[audit] test-coverage: 22/36 SupportedStmtFragment constructors lack concrete instantiation witnesses

[Th0rgal]

Finding

The master preservation theorem compile_supported_stmt_fragments_semantics (TypedIRCompilerCorrectness.lean:4797) generically proves correctness for all 36 SupportedStmtFragment constructors. However, only 14 of 36 constructors have concrete contract-function instantiation witnesses (lines 4859–5369).

The 22 constructors without concrete witnesses are:

#	Constructor	Category
1–17	Pure literal, branching, storage read/write, return patterns	Basic building blocks
18–22	Arithmetic rebinding patterns (addRebind, subRebind, mulRebind, divRebind, modRebind)	Arithmetic
30	returnMappingCaller	Mapping access

Constructors WITH witnesses (14)

• Counter: docs: add verification status documentation #23 (increment), chore: consolidate property extraction and infrastructure improvements #24 (decrement), Add Unlink Privacy Protocol with formal verification #25 (getCount)
• SimpleStorage: docs: roadmap to completion (Layer 3 + production-ready) #26 (retrieve)
• Owned: fix: make create_layer3_issues.sh idempotent #27 (getOwner)
• OwnedCounter: docs: roadmap to completion (Layer 3 + production-ready) #26, fix: make create_layer3_issues.sh idempotent #27, [Layer 3] Prove variable assignment statement equivalence #28, [Layer 3] Prove storage load statement equivalence #29
• ERC20: Add Unlink Privacy Protocol with formal verification #25, [Layer 3] Prove mapping load statement equivalence #31, [Layer 3] Prove mapping store statement equivalence #32, [Layer 3] Prove conditional (if) statement equivalence #33, [Layer 3] Prove return statement equivalence #34
• ERC721: [Layer 3] Prove revert statement equivalence #35, [Compiler Enhancement] External function linking for production cryptographic libraries #36

Risk

The 22 untested constructors are generically proved correct, so there is no soundness gap. However, the lack of concrete witnesses means:

1. No instantiation smoke test: if a constructor's hypotheses are accidentally unsatisfiable, no test would catch it.
2. No downstream contract exercise: patterns like addRebind are presumably used via the macro but no contract exercises them in the witness list.

Recommendation

Add concrete instantiation witnesses for the 22 missing constructors, or document that they are covered transitively by the macro-generated contract witnesses (if that can be shown).

Discovered by automated audit (Priority 5: test coverage).