verification(A3.1 step-4): proof-phase foundation (execList_append + setVar frame) + record the N-mask gate finding

Proof-phase foundations (advisor: "frame lemmas first"):
- execList_append: running xs ++ ys runs xs then (only if it didn't halt) ys —
  the structural lemma behind every phase split, halt short-circuit threaded.
- setVar_get_eq / setVar_get_ne: binding-frame lemmas so a phase can carry a
  computed binding (e.g. digest) past later statements touching other vars.

FINDING (surfaced by the refinement, documented in A3_1_CLOSURE_PATH.md §8): the
deployed Yul rejects non-N-masked pkSeed/pkRoot (L58-65), but verifyYulModel =
verifyRefined does `take 16` with NO N-mask gate (confirmed Refined.lean:143). So
execC10Asm = verifyYulModel is not literally true; the faithful, STRONGER target
is execC10Asm = nMaskedB pkSeed && nMaskedB pkRoot && verifyYulModel — folding the
input-gate (currently a separate Halmos check) into one kernel statement. It is a
precision win, not a bug: the bytecode is strictly more restrictive (safety
direction holds), DeployedBytecode is opaque (nothing provably-false), and the
divergence is unreachable via the factory/addOwner (which N-mask). The phase
proofs are UNAFFECTED (they prove the both-N-masked branch computes verifyYulModel).
The only consequence is a step-6, USER-GATED reconciliation that threads the
already-modeled Factory.nMasked invariant through theft_free's liveness use of the
A3.1 axiom — old axiom kept in place until then.

verify-build green, verify-interp 396/396, theft_free closure unchanged.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: Nicola-Ceornea

contracts/verification/docs/A3_1_CLOSURE_PATH.md

@@ -369,7 +369,41 @@ with the climb lemmas as the loop-refinement engine.
   6. Replace `solidityVerifier_compiles_correctly` with the narrow
      `DeployedBytecode.SPHINCsC10Asm_verify = execC10Asm` transcription axiom
      (empirically backed by step 3 / `make verify-interp`) + re-derive the old
-     statement as a theorem.
+     statement as a theorem. **See the N-mask finding below — this step touches
+     `theft_free` and is USER-GATED.**
+
+### FINDING (2026-06-17, surfaced by the refinement) — N-mask gate: bytecode strict, model lenient
+
+The deployed Yul (`SPHINCsC10Asm.sol` L58–65) rejects (`return false`) any
+`pkSeed`/`pkRoot` not in N-mask shape (`and(key, N_MASK) != key`). The Lean model
+`verifyYulModel = Verifier.Refined.verifyRefined` (confirmed at `Refined.lean:143`)
+takes `ByteVec 32` keys and does `pkSeed.take 16` — **silently discarding the
+bottom 16 bytes, with NO N-mask check.** So `execC10Asm = verifyYulModel` is **not
+literally true**: on a non-N-masked key, `execC10Asm = false` (gate) while
+`verifyYulModel` uses the top 16 and can be `true`. (Deductively certain;
+`verify-interp` 396/396 is consistent because every KAT/bulk key is N-masked.)
+
+- **It is a precision WIN, not a bug.** The bytecode is strictly *more* restrictive
+  (`bytecode true → model true` always; divergence only at `bytecode false, model
+  true`, reachable only by inputs the factory/`addOwner` never produce — they
+  N-mask). `DeployedBytecode` is opaque, so the old axiom is unfaithful-to-reality,
+  NOT provably-false (no soundness fire). The project already covers the gate via
+  **Halmos input-gates, separately** from the Lean equiv; the interpreter folds
+  *core + gate* into ONE kernel statement, subsuming the Halmos check.
+- **True target theorem (step 5/6 end-state):**
+  `execC10Asm pkS pkR m sig = nMaskedB pkS && nMaskedB pkR && verifyYulModel pkS pkR m sig`,
+  with `nMaskedB key := (wordOf key) &&& N_MASK == wordOf key` (Bool, matching the
+  bytecode) + a small lemma to `Wallet.Factory.nMasked` (Prop). The phase proofs
+  (H_msg→FORS→WOTS→hypertree) are UNAFFECTED — they prove the both-N-masked branch
+  computes `verifyYulModel`; the gate is the top-level `ifnz` wrapper.
+- **`theft_free` interaction (step 6, USER-GATED):** `theft_free` (Theorems.lean
+  :350-352) uses the A3.1 axiom in the LIVENESS direction (`rw [hbridge]; exact
+  hverify`: `verifyYulModel true → DeployedBytecode true`). Under the faithful
+  characterization that needs the stored keys N-masked — modeled
+  (`Factory.nMasked`/`Storage.hasNMaskLayout`) and enforced by the factory/addOwner,
+  so threadable, but it edits `theft_free`. **KEEP the old axiom in place for now;
+  bring the swap (transcription axiom + characterization + threading the N-mask
+  invariant) to the user at step 6, with the characterization already proven.**
 
 - **(historical) the original executable-first NEXT list (now steps 1–3 done):**
   1. **`Interpreter/Yul.lean`** — the C10 opcode-subset AST (`Expr`:

contracts/verification/lean/SphincsCVerify/Interpreter/Yul.lean

@@ -181,6 +181,43 @@ mutual
         | (vm', some h) => (vm', some h)
 end
 
+/-! ## Composition + binding-frame lemmas (proof-phase foundation)
+
+These are the workhorses the phase-wise refinement consumes (`docs/A3_1_CLOSURE_PATH.md`
+§8 step 4): `execList_append` splits the program at phase boundaries (with the
+halt short-circuit threaded), and the `setVar` frame lemmas let a phase carry a
+computed binding (e.g. `digest`) past later statements that touch other vars. -/
+
+/-- Reading the just-bound variable returns the bound value. -/
+@[simp] theorem setVar_get_eq (env : VarEnv) (x : String) (v : Nat) :
+    setVar env x v x = v := by
+  unfold setVar; rw [if_pos rfl]
+
+/-- Reading a *different* variable is unaffected by a binding. -/
+@[simp] theorem setVar_get_ne (env : VarEnv) (x y : String) (v : Nat) (h : y ≠ x) :
+    setVar env x v y = env y := by
+  unfold setVar; rw [if_neg h]
+
+/-- **Phase composition.** Running `xs ++ ys` runs `xs`, and — only if `xs` did
+    not halt — continues with `ys` from the resulting state; a halt in `xs`
+    short-circuits. The structural lemma behind every phase split. -/
+theorem execList_append {n : Nat} (sha : List UInt8 → Spec.ByteVec 32) (sig : Spec.ByteVec n)
+    (xs ys : List Stmt) (vm : VM) :
+    execList sha sig (xs ++ ys) vm
+      = match execList sha sig xs vm with
+        | (vm', none)   => execList sha sig ys vm'
+        | (vm', some h) => (vm', some h) := by
+  induction xs generalizing vm with
+  | nil => simp only [List.nil_append, execList]
+  | cons s rest ih =>
+      show execList sha sig (s :: (rest ++ ys)) vm = _
+      rw [execList]
+      cases hs : execStmt sha sig s vm with
+      | mk vm' o =>
+        cases o with
+        | none => rw [execList, hs]; exact ih vm'
+        | some h => rw [execList, hs]
+
 /-! ## Top-level program execution -/
 
 /-- Run a program from a caller-supplied initial memory (`mem0` lets the caller