docs(plans): refine model-property-checking surface

[scarmuega]

Refines the model-property-checking.md plan merged in #33, after a design review pass. Docs-only.

What changed (the property / trix prove surface):

• Forward-compatible by construction (new decision 8). The verified subject is always a transaction; a rule is a projection of it, never a top-level subject — so widening rule→tx→protocol only adds clauses, never reinterprets existing ones.
• invokes / accepted are explicit predicates under assume/assert, not binder magic. The assume-vs-assert position of accepted is exactly the soundness (V ⊆ Safe) vs completeness (Honest ⊆ V) distinction. This makes "which input runs which spend rule" expressible.
• tx-relative namespaced access (new decision 9). Inputs/outputs under tx.inputs.<name> / tx.outputs.<name>; inputs are records projected explicitly (.value / .datum / .redeemer), removing the value-vs-datum overload. Mint redeemer at tx.mints.<Policy>.redeemer.
• ASCII proof-keyword surface (new decision 10). Block keyword check → property; one binding per for (no comma-lists); equivalent dropped (it's assert a == b); quantifier-neutral binder with assert (∀) / satisfiable (∃) as duals; no Unicode glyphs.

Scope unchanged: prove the Tx3 model, not the generated enforcement layer. Branch is based on the post-#33 main; clean delta.

🤖 Generated with Claude Code