feat(prove): prove properties of a script for every initial balance

[ascandone]

What

numscript prove <file.num|file.ir> checks boolean properties of a script for every initial balance, and numscript ir <file.num> dumps the compiled textual IR. Both are experimental commands (hidden unless NUMSCRIPT_EXPERIMENTAL_CLI is set). Full write-up in prove.md.

$ numscript prove internal/prove/testdata/cases/simple-send.num

simple-send.num: touches @dest, @src in USD/2; success reachable: yes; failure reachable: yes

  ✓ enough_means_success         valid          10ms
  ✓ dest_credited                valid          8ms
  × src_never_negative           counterexample 8ms
  ...
× src_never_negative: after(@src, USD/2) >= 0
  initial balances:
    | Account | Asset | Balance |
    | src     | USD/2 | -1      |
  outcome: fails at instruction 20 `check_enough_funds($r9, $r2)`: missing funds

Properties are written in a small language (prop name: formula in a .props file, or --prop "..."):

prop enough_means_success: before(@src, USD/2) >= 100 => success
prop dest_credited: success => after(@dest, USD/2) == before(@dest, USD/2) + 100
prop exact_a: success => sent(@a, USD/2) == min(30, max(0, before(@a, USD/2)))

Atoms: before, after, sent, received, moved(@a, @b, X), delta, success/fails; and or not => <=>, comparisons, linear arithmetic with Euclidean / and %, min/max. A failed run applies nothing (after == before, all totals 0), so properties about the committed run carry an explicit success =>.

How

• The compiled IR (forward jumps only, so text order is execution order) is encoded in one pass into an SMT-LIB2 model: every initial balance is a free Int, every state write is a define-fun named after the register or balance and the instruction index, branches clone the state and labels merge with ite chains. The funds queue is one slot per pull_account, drained in order by send_to_account; oneof marks repay the slots pulled inside the region; failing instructions are guarded flags and every output is masked by fails. Portions are rational linear forms over Int, so portion_to_int is an integer div and the whole problem stays in QF_LIA.
• The property's negation is asserted and z3 -in (or cvc5, or any SMT-LIB2 solver via --solver) decides it. unsat is valid.
• Every sat model is replayed on the real VM (vm.Exec with a static store) and compared output by output; a disagreement is reported as tool-bug, never as a finding.
• v1 rejects vars, metadata reads, colors, scopes and non-constant strings reaching an account/asset with an UnsupportedError naming the instruction.

Tests

• internal/prove/encode: a differential sweep that evaluates the model at concrete balances without a solver and compares with vm.Exec: 166 of the spec-corpus scripts encode and all 172 of their cases agree; hand-written IR for shapes the compiler never emits (capped send smaller than the queue, negative cap, uncapped overdraft, asset switch between pull and send, undrained queue, kept, save, division by zero, oneof, rewind after a join).
• internal/prove/testdata/cases: .num/.ir + .props + .expected fixtures (simple send, capped source, allotment, @world, oneof, save, kept, send-all, a vacuous script, negative amount, hand IR, a vars script expected unsupported). Counterexample models are not pinned (solver-dependent); each must replay-confirm, and every valid gets a 64-trial random VM cross-check.
• internal/prove/prop: parser/typecheck/eval/lower tables and FuzzParse.
• Solver-backed tests skip without z3 unless NUMSCRIPT_REQUIRE_Z3=1; a new Prove CI job installs z3 and sets it. flake.nix gains z3.

Not in this PR

Script vars (binding load_var to constants is the first step and unlocks the generator sweep, which today encodes almost nothing because generated scripts use vars), metadata, colors, scopes, forall/sum over accounts (finite expansion; syntax reserved). See the extension path in prove.md.

[NumaryBot]

🟠 [major] Give repeated rewind balance writes distinct names

A valid hand-written IR region containing mark_push, two capped pull_account instructions for the same account/asset, and mark_rewind reaches this assignment twice with the same bal(account,asset)@pos name. With symbolic initial balances, both refund expressions are non-leaf terms, so smt.Script.Define calls bind twice and panics (name bound twice). The prover crashes before querying the solver instead of modelling this supported funds-queue shape. Existing rewind fixtures only pull distinct accounts and miss this case.

Suggestion: Aggregate rewind refunds by Key and define each balance once, as send does, or include the slot position in each intermediate balance name. Add a same-account, two-pull rewind regression that compares the encoded outcome with Replay.

[NumaryBot]

🟡 [minor] Run the solver gate through the shared race-enabled tooling

The new Prove job installs an unpinned distro z3 and invokes plain go test, while the Nix shell now supplies z3 and Justfile's tests recipe enables -race. Consequently solver-backed paths exercised by this gate are not race-checked, and this gate uses a different solver environment from local/shared CI testing. This contradicts RFC-0015's shared Nix/Just and race-enabled testing requirements.

Suggestion: Run the required-solver gate using nix develop --impure --command just with a shared recipe that sets NUMSCRIPT_REQUIRE_Z3=1 and retains race checking (or use the existing tests recipe with that environment variable). Remove the separate apt/setup-go test environment.