tptsto_agree is not sound in the simple_pred model

[gmalecha-at-skylabs]

This is a model-level issue, not a logic-level issue.

Clients only see these predicates if they work below the level of primR (which is rare). A greater degree of sealing would further insulate clients from this sort of issue.

Problem
The issue is the overlap between raw and non-raw values for byte-sized types.

Several potential fixes:

1. Weaken tptsto_agree to only hold on precise types, i.e. those that do not admit raw.
2. Remove tptsto entirely and replace it with tptsto_fuzzy. This weakens the = to a val_related ty.