feat(transform): Add optional SSA transformation for Strata Core

[sagjoshi]

Introduce a Static Single Assignment (SSA) transformation that converts
procedure bodies so every variable is assigned exactly once via init.
Mutations (set, havoc) become fresh init declarations. At if-then-else
join points, conditional init expressions merge divergent variable versions.

Uses the standard CoreTransformM monad with CoreGenState.gen for fresh
name generation (ssa_ prefix), aligning with transform API conventions.

Integration:

• Available as `--pass ssa` in the transform CLI command
• Available as `TransformPass.ssa` in the SimpleAPI
• Not part of the default verification pipeline (opt-in)

Files:

• `Strata/Transform/SSA.lean`: transformation implementation
• `StrataTest/Transform/SSA.lean`: 16 tests
• `Strata/SimpleAPI.lean`: TransformPass.ssa + applyPass wiring
• `StrataMain.lean`: ssa added to valid transform passes

[tautschnig]

Bug 1 — output parameters lose their final assignment

In transformCmd, the .set r … case generates var ssa_r_N : int := … instead of preserving the write to the output parameter r. After SSA, the declared output is never assigned.

Minimal repro:

procedure inc(x : int, out y : int)
spec { ensures (y == x + 1); }
{ y := x + 1; };

Before SSA: inc_ensures_0 : ✅ pass. After [.ssa]: body becomes var ssa_y_0 : int := x + 1; — y is never written — and inc_ensures_0 : ❌ fail.

See the inline comment on transformCmd. The fix is probably to emit a final r := ssa_r_N for every output whose env ident diverged from its original ident, at the end of each procedure body (and similarly for inout parameters).

Bug 2 — phi merges can reference out-of-scope or undefined names

Strata Core blocks introduce lexical scope (see Translate.lean:1332 — translateBlock does not propagate boundVars out of the block). emitJoinMerges emits phi inits at the join point that reference the branches' in-block SSA names, which are no longer in scope after the ITE. And when a variable is declared only in one branch (and wasn't in preEnv), the other branch's getIdOr falls back to ⟨origName, ()⟩ — the raw pre-SSA name, which may never have been declared at all.

Minimal repro:

procedure f(c : bool, out r : int) {
  if (c) { var x : int := 42; }
  r := 0;
};

SSA output:

  var ssa_$ssa_cond_0 : bool := c;
  if (ssa_$ssa_cond_0) { var ssa_x_1 : int := 42; }
  var ssa_phi_x_2 : int := if ssa_$ssa_cond_0 then ssa_x_1 else x;
  var ssa_r_3 : int := 0;

Both ssa_x_1 (declared inside the then-block) and x (never declared) appear in the outer scope. Strata's current type checker happens to accept this (that's probably its own bug), but it's clearly wrong. The logic should either skip join-merges for variables that weren't in preEnv, or lift the declarations themselves out of their branches to procedure scope before emitting the phi.

See the inline comment on emitJoinMerges / getIdOr.

Pipeline validation is wrong

Given Bug 1, the .modelPreserving annotation on ssaPipelinePhase is false: there exist programs where SSA changes verification outcomes from pass to fail. Until Bug 1 is fixed, this phase shouldn't claim model preservation. Consider .unchecked or a new .transformModels validation with explicit documentation — or .notImplemented while the transform is still experimental / opt-in.

Test coverage is too weak to catch either bug

All 16 tests use one of three weak oracles — see inline on StrataTest/Transform/SSA.lean. A single VC-outcome round-trip test would have caught Bug 1; a simple "no undefined identifiers" check on the output would have caught Bug 2.

Refactoring notes

• getIdOr's fallback to ⟨origName, ()⟩ silently produces potentially-undefined references. It should either be removed (in favor of throwing a diagnostic at the call site) or, if a fallback really is needed, asserted unreachable via a panic!-replacement that reports the bug.
• genSSAIdent "$ssa_cond" yields ssa_$ssa_cond_N, a double-ssa_ / double-$ name that is ugly to read in traces. Pick "cond" (→ ssa_cond_N) or bypass the ssa_ prefix for these internal names.
• initEnvFromProcedure seeds the env for outputs identically to inputs — document that outputs require a final re-assignment (once Bug 1 is fixed) so a future reader doesn't try to "simplify" the initialization.
• collectAllKeys : List Env → List String is only ever called with a 3-element list; either specialize it or keep it general and add a 0/1/2/empty test.
• rewriteExpr shortcircuits on env.isEmpty, but substFvars with an empty map is already a no-op; the check is harmless but redundant.
• The rewriteExpr/rewriteExprOrNondet split plus getIdOr/getTyOr/varChanged makes emitJoinMerges hard to follow — consider extracting a phiEntry : String → Env → Env → Env → Option (Ident × Ident × Ty) that returns none for vars that don't need a phi and handles the scoping / lookup concerns in one place.

Theorems / tests worth locking in

All of these would either prevent re-occurrence of the two bugs or push the transform toward the .modelPreserving guarantee:

1. Single-assignment: for all p : Program, every procedure body produced by ssaTransform has distinct init identifiers (modulo nested blocks). This is the defining invariant of SSA form.
2. Scoping: for all p : Program, every free-variable reference in the body produced by ssaTransform p resolves to a init-declared identifier in an enclosing scope. (Would have failed for Bug 2.)
3. Output preservation: for all p : Program and every procedure P with output o, the final value of o under the transformed body equals the final value of o under the original body. (Would have failed for Bug 1.)
4. VC-outcome preservation: a property-test (plausible / random Core procedures) that verify p and verify (runTransforms p [.ssa]) produce identical VC outcomes per label.
5. Well-typedness preservation: a simpler prerequisite to #4 — if the original type-checks, so does the SSA output.

#1 and #2 should be tractable as pencil-and-paper proofs over the structure of transformStmt / transformCmd. #3 and #4 are harder but the payoff is high: they would justify the .modelPreserving claim that currently isn't true.

[tautschnig]

Remaining soundness bug: flattened ITE loses the path-condition guard for branch-specific asserts.

Reproducer I ran locally on this branch:

procedure check_branch_assert(x : int) {
  if (x > 0) {
    assert [pos]: (x > 0);
  }
};

Original: verifies (path condition for the assert is x > 0 from the branch guard — trivially entails the assert).

After --pass ssa, the program becomes (copied verbatim from the output):

procedure check_branch_assert (x : int)
{
  var ssa_cond_0 : bool := x > 0;
  assert [pos]: x > 0;
};

SSA'd: fails — x is an input, the assert is now unconditional, and x = -5 is a counterexample the solver picks up. The if (x > 0) { … } wrapper has been flattened away, and the assert no longer has ssa_cond_0 → … as its guard.

This falsifies the .modelPreserving claim (SSA.lean:256): the SSA'd program produces a counterexample (x = -5) that is not a counterexample in the original (where x = -5 simply skips the then-branch). So an SSA run in deductive mode reports false-alarm failures, and an SSA run in bug-finding mode reports spurious counterexamples. Both are the kind of unsoundness .modelPreserving is meant to rule out.

The .ite .det arm at :186-198 flattens both branches inline:

return (mergedEnv, [condInit] ++ thenStmts' ++ elseStmts' ++ merges)

The standard fix in SSA is either (a) guard each branch-local assert with an implication ssa_cond_0 → assert_expr before flattening, or (b) keep the .ite intact and only add phi inits at the join (no flattening). Details inline on transformStmt. Worst-case, route this under .modelToValidate until the fix lands.

Other observations (all smaller):

• ssaTransform always reports changed = true (:241) even when no procedures were transformed (e.g., a program of only axioms/types). Pipeline consumers treat changed as "something changed"; reporting true unconditionally makes downstream fixpoint loops non-terminating.
• emitOutputAssignments reintroduces set into the output program (:173). This breaks the SSA invariant ("every variable assigned exactly once") for output parameters specifically — the output gets var ssa_y_N := … followed by set y := ssa_y_N. Worth a docstring note that this exception is intentional to preserve the procedure contract, so a reader doesn't misread "SSA" as literally meaning every variable is init-once.
• emitOutputAssignments skips outputs whose final SSA id equals the original. Fine for the common case, but for an output parameter that a procedure never assigns, we skip — which is correct. Worth a comment saying so.
• Duplicated .ite .det / .ite .nondet arms (:186-205) differ only in the RHS of condInit (.det condExpr' vs .nondet). Extract a helper buildIteLocal (condInitRhs : ExprOrNondet Expression) that emits condVar + branches + merges. Not blocking.
• rewriteExpr's substFvars handles bound variables correctly (standard capture-avoiding), but there's no test that exercises SSA inside a quantifier (the only LExpr binders in the asserts that might appear in procedure bodies). Worth a fixture: assert [q]: ∀ i : int. x > i — verify SSA renames x but leaves i alone.

Test-coverage gaps:

• The new SSACorrectnessTests section (:324-423) adds 3 round-trip fixtures; none of them exercise branch-specific asserts, so the soundness bug above is invisible to the test suite. Adding my check_branch_assert reproducer would catch it.
• 14 of the 16 tests use the oracle toString fmt result != toString fmt pgm (unchanged since thread T14). Those tests only check that the transform did something; they pass if a transform deletes every procedure, or if it emits spurious counterexamples. I'd like to see at least one of them replaced with a structural #guard_msgs check on the expected output shape.

Proof suggestions:

Three theorems would formalize the SSA invariants and (importantly) would fail to prove today because of the soundness bug — making the bug provable-as-a-lemma, which is the right place for it:

/-- Single-assignment invariant: after `ssaTransform`, no variable is assigned more than once. -/
theorem ssaTransform_single_assignment
    (p : Program) (p' : Program) (h : Core.Transform.run p (Core.SSA.ssaTransform · |>.map (·.2)) = .ok p') :
    ∀ proc ∈ p'.decls.filterMap (·.getProc?),
      (∀ name, (Core.SSA.countInits name proc.body) + (Core.SSA.countSets name proc.body) ≤ 1)

(The output-writeback set is the one documented exception — the statement would need an explicit carve-out for procedure output parameters.)

/-- Scoping invariant: every fvar referenced in `ssaTransform p` is either an input,
    an output, or introduced by an SSA-generated init earlier in the same scope. -/
theorem ssaTransform_closed_fvars (p p') : …

/-- Model-preservation: if the SSA'd program has a counterexample for obligation Q,
    the original program has one too.  Fails under the current `.ite` flattening
    — proving this is the right gate for flipping back from `.modelToValidate`. -/
theorem ssaTransform_preserves_model (p p' : Program) (Q : ProofObligation Expression) (m : Model) :
    Core.Transform.run p (Core.SSA.ssaTransform · |>.map (·.2)) = .ok p' →
    Q ∈ obligationsOf p' → isModel Q m → ∃ Q', Q' ∈ obligationsOf p ∧ isModel Q' m

Filing these even as sorry-terminated stubs would make the soundness story visible at the type level and would prevent silent regressions when a future edit touches the .ite arm.

[tautschnig]

Soundness bug: branch-specific asserts lose their path-condition guard. I reproduced this on the current branch:

procedure check_branch_assert(x : int) {
  if (x > 0) { assert [pos]: (x > 0); }
};

Original: verifies. After --pass ssa:

procedure check_branch_assert (x : int)
{
  var ssa_cond_0 : bool := x > 0;
  assert [pos]: x > 0;
};

SSA'd: fails (x = -5 is a spurious counterexample). The if is flattened away but the assert isn't guarded by ssa_cond_0, so the verifier checks x > 0 unconditionally.

Two standard fixes:

1. Guard branch asserts at flattening time. In transformBlock (called with the branch env), whenever an assert is encountered inside a then/else branch, rewrite it as assert (condVar → original_assert). This preserves VC semantics while still flattening.
2. Don't flatten — keep the .ite intact and only add phi inits at the join. Emit the ITE as .ite cond' (thenStmts' ++ localPhis) (elseStmts' ++ localPhis) md ++ outerPhis. The phis for variables changed in only one branch use the preEnv value on the other side, which is what phiEntry already computes. This is the standard SSA-with-control-flow representation.

Option (2) is less invasive — the flattening was the source of the bug. Option (1) is simpler to implement on top of the current code.

Until one of these lands, please downgrade .modelPreserving at line 256 to .modelToValidate so the solver validates models it produces — see inline comment there.

Also add the reproducer to SSACorrectnessTests:

def SSABranchAssertRoundTrip :=
#strata
program Core;
procedure check_branch_assert(x : int) {
  if (x > 0) { assert [pos]: (x > 0); }
};
#end

/-- info: true -/
#guard_msgs in
#eval show IO Bool from do
  let pgm := translate SSABranchAssertRoundTrip
  let origResults ← … -- verify, should pass
  let .ok ssaPgm := Core.runTransforms pgm [.ssa] | return false
  let ssaResults ← … -- verify ssaPgm, should ALSO pass (currently fails)
  return origPass && ssaPass

[tautschnig]

Nit: return (true, { decls := decls }) always reports changed = true, even when p.decls contains no procedures (or every procedure had an empty body, short-circuited at :228). Downstream consumers that run passes to a fixpoint will loop forever on SSA applied to an axiom-only program.

Suggested change

	return (true, { decls := decls })
	-- Track whether any procedure was actually transformed. An empty / proc-less
	-- program is a no-op; reporting `changed = true` would force fixpoint loops
	-- in the transform driver to iterate indefinitely.
	let mut anyChanged := false
	let decls ← p.decls.mapM fun d =>
	match d with
	| .proc proc md =>
	if proc.body.isEmpty then pure (.proc proc md)
	else do
	anyChanged := true
	return .proc (← transformProcedure proc) md
	| other => return other
	return (anyChanged, { decls := decls })

[tautschnig]

Worth documenting the intentional SSA-invariant exception here: after emitOutputAssignments, the output parameter gets assigned via set outId := ssa_y_N in addition to its var ssa_y_N : int := … init. That is a genuine double-assignment on outId — once implicitly at the procedure boundary (when we seed it in initEnvFromProcedure), once here.

A reader checking "does every variable have exactly one init?" would find this confusing.

Suggested change

	/-- Emit final `set` statements to write SSA-renamed values back to the
	original output/inout parameter identifiers. This preserves the
	procedure's contract semantics. -/
	def emitOutputAssignments (proc : Procedure) (finalEnv : Env)
	(md : Imperative.MetaData Expression) : List Statement :=
	(proc.header.outputs : List _).filterMap fun (outId, _) =>
	match finalEnv.get? outId.name with
	| some info =>
	if info.ident != outId then
	some (Statement.set outId (createFvar info.ident) md)
	else none
	| none => none
	/-- Emit final `set` statements to write SSA-renamed values back to the
	original output/inout parameter identifiers. This preserves the
	procedure's contract semantics.
	Note (SSA-invariant exception): the output parameter's original name is
	reassigned here via `set` even though SSA nominally permits exactly one
	assignment per name. This is deliberate: the procedure contract references
	outputs by their declared name, so the SSA form has to write the final
	SSA value back before returning. All *local* variables remain strictly
	single-assignment. -/
	def emitOutputAssignments (proc : Procedure) (finalEnv : Env)
	(md : Imperative.MetaData Expression) : List Statement :=
	(proc.header.outputs : List _).filterMap fun (outId, _) =>
	match finalEnv.get? outId.name with
	| some info =>
	-- Skip when the output was never assigned in the body (its SSA id
	-- equals the original seed from `initEnvFromProcedure`).
	if info.ident != outId then
	some (Statement.set outId (createFvar info.ident) md)
	else none
	| none => none

[tautschnig]

Downgrade to .modelToValidate until the branch-assert soundness bug is fixed. Per the inline on :184-198 and the top-level body: the current .ite flattening produces spurious counterexamples (verified on this branch: the check_branch_assert reproducer fails in SSA form where it passes in original). .modelPreserving means "sat results are sound" — which is exactly what this flattening breaks.

Suggested change

	phase.getValidation _ := .modelPreserving
	/-- SSA pipeline phase: converts procedure bodies to SSA form.
	Correctness status (NOT YET `.modelPreserving`): the current `.ite`
	handling flattens branches without guarding branch-specific asserts by
	the branch condition. This introduces spurious counterexamples for
	programs like `if c then assert b`, where the SSA form checks `b`
	unconditionally even though the original only reaches the assert on
	the `c = true` path. See the TODO on `transformStmt`'s `.ite` arm.
	Until the guard-or-preserve fix lands, models must be validated — a
	counterexample reported by the solver after SSA may be spurious.
	TODO: once the fix lands, flip back to `.modelPreserving` and file a
	formal proof of model-preservation. -/
	def ssaPipelinePhase : PipelinePhase where
	transform := ssaTransform
	phase.name := "SSA"
	phase.getValidation _ := .modelToValidate (fun _ => false)

(The concrete validator fun _ => false conservatively rejects every model — safe default. A sharper validator that re-runs the original program on the candidate counterexample is the follow-up work.)

[tautschnig]

Two gaps in the correctness suite:

1. Branch-specific asserts. Add the reproducer from my review body — if c then assert b-shaped procedures — so the soundness bug on SSA.lean:184-198 is caught by the test suite:

def SSABranchAssertRoundTrip :=
#strata
program Core;
procedure check_branch_assert(x : int) {
  if (x > 0) { assert [pos]: (x > 0); }
};
#end

/-- info: true -/
#guard_msgs in
#eval show IO Bool from do
  let pgm := translate SSABranchAssertRoundTrip
  let origResults ← …  (as SSAIncRoundTrip)
  let origPass := origResults.all Core.VCResult.isSuccess
  let .ok ssaPgm := Core.runTransforms pgm [.ssa] | return false
  let ssaResults ← …
  let ssaPass := ssaResults.all Core.VCResult.isSuccess
  return origPass && ssaPass  -- fails today; passes once SSA guards branch asserts

2. Structural / snapshot tests. The 14 SSA tests at :43-322 use the oracle toString fmt result != toString fmt pgm — they only check that something changed. A transform that deletes every procedure passes all 14; so does a transform that emits the empty program with one global var. Consider replacing at least one of these (e.g. SSATest1) with a #guard_msgs snapshot of the expected SSA output, so a regression in the shape of the produced program surfaces directly rather than only via a downstream verification failure.