Update SORRY_REDUCTION_PLAN.md: 4 → 3 sorries (93% reduction)

- Record sorry #4 elimination (setMappingPackedWord singleton)
- Record TYPESIG_SORRY reduction progress
- Update remaining sorry line numbers and analysis
- Add TYPESIG_SORRY status table

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: claude

docs/SORRY_REDUCTION_PLAN.md

@@ -1,9 +1,9 @@
 # Sorry Reduction Plan — Pass 5
 
-## Current State (as of commit 08b717e3)
+## Current State (as of commit 8a589c04)
 
-**Active `sorry`**: 4 (all in `GenericInduction.lean`)
-**TYPESIG_SORRY blocks**: ~57 commented-out theorems with broken type signatures
+**Active `sorry`**: 3 (all in `GenericInduction.lean`)
+**TYPESIG_SORRY blocks**: ~20 commented-out theorems with broken type signatures
 **Build status**: Green (compiles with warnings only)
 
 ## Progress (Pass 5)
@@ -22,33 +22,33 @@
 | `66236a18` | 6 | Add keccak axiom `solidityMappingSlot_add_wordOffset_lt_evmModulus` + prove 4 mapping slot wordOffset≠0 sorries (−4) |
 | `7dee40c3` | 5 | Prove aliasSlots TYPESIG_SORRY chain: 3 theorems uncommented (−1) |
 | `08b717e3` | 4 | Add ExprCompileCore bitwise constructors, prove exprCompileCore_of_exprTouchesUnsupportedContractSurface (−1) |
+| `faaf81e5` | 4 | Remove 7 dead-code TYPESIG_SORRY blocks, uncomment 2 setStorage blocks, uncomment 2 exceptMappingWrites blocks (TYPESIG reduction only) |
+| `8a589c04` | 3 | Prove compiledStmtStep_setMappingPackedWord compileOk + eliminate sorry #4 (singleton) (−1) |
 
-## Remaining 4 Sorries — Architecturally Blocked
+## Remaining 3 Sorries — Architecturally Blocked
 
 Every remaining sorry depends on fundamental design issues that cannot be resolved
 by proof work alone. They require either upstream code changes, new axioms, or
 substantial proof infrastructure.
 
-### 1. Identifier shapes (line 5982)
+### 1. Identifier shapes (line 5993)
 **Theorem**: `validateIdentifierShapes_fieldName_avoidReservedCompilerPrefix`
 **Blocker**: Claims no field name starts with `"__"`, but `__immutable_*` fields are
 explicitly allowed by the validation pipeline.
 **Fix**: Thread stronger field-shape classification that distinguishes mutable vs
 immutable fields through the generic induction scope invariant.
 
-### 2. setMappingPackedWord (line 7467)
+### 2. setMappingPackedWord preserves (line 7604)
 **Theorem**: `compiledStmtStep_setMappingPackedWord_singleSlot_of_slotSafety_preserves`
 **Blocker**: Requires proving a 5-statement IR block body executes correctly, plus a
 bitwise identity (`storedIR = packedWordWrite`) bridging IR-level Nat operations with
 Uint256-level `packedWordWrite`. Three proof attempts were made:
-- **Attempt 1**: Explicit state chain with raw `Nat.land`/`Nat.xor` — 6 errors including
-  notation mismatches (`&&&` vs `Nat.land`) and getVar/setVar resolution failures.
-- **Attempt 2**: Restructured with fuel decomposition (`obtain ⟨ef, rfl⟩`) and concrete
-  `Nat.succ` fuel — timed out at 200k heartbeats on `simpa [compiledIR] using hslack`,
-  `simp [YulStmt.block.sizeOf_spec]`, and `set state1 := ...`.
-- **Attempt 3**: Considered increased heartbeats (800k) and early `by_cases` on
-  `wordOffset == 0` to avoid conditional terms, but fundamental timeout on term-level
-  `sizeOf` computation with abstract subexpressions remains.
+- **Attempt 1**: Explicit state chain with raw `Nat.land`/`Nat.xor` — notation mismatches
+  and getVar/setVar resolution failures.
+- **Attempt 2**: Fuel decomposition with concrete `Nat.succ` — timed out at 200k heartbeats
+  on `sizeOf` computation with abstract subexpressions.
+- **Attempt 3**: Increased heartbeats + `by_cases` on `wordOffset == 0` — fundamental
+  timeout on term-level sizeOf with conditionals remains.
 **Root causes**:
   1. `execIRStmts` requires `Nat.succ` fuel at each cons, needing explicit fuel
      decomposition that triggers `sizeOf` computation timeouts.
@@ -60,18 +60,24 @@ Uint256-level `packedWordWrite`. Three proof attempts were made:
 packed word block body execution with its own `maxHeartbeats` budget. This isolates
 the expensive term reduction. The bitwise identity also needs a separate lemma.
 
-### 3. setStorageAddr — Address modulus (line 9944)
+### 3. setStorageAddr — Address modulus (line 10000)
 **Theorem**: `stmtListGenericCore_singleton_setStorageAddr_singleSlot`
 **Blocker**: Depends on `compiledStmtStep_setStorageAddr_singleSlot_preserves` (TYPESIG_SORRY
-at line 6134). That theorem needs `runtimeStateMatchesIR_writeAddressSlot` which requires
+at line 6150). That theorem needs `runtimeStateMatchesIR_writeAddressSlot` which requires
 `value < Address.modulus` (2^160), but `evalExpr` only gives `< evmModulus` (2^256).
 Source semantics truncates to 160 bits via `wordToAddress` but IR stores full 256 bits.
 **Fix**: Either add a truncation step in the IR compilation of address storage, or
 add a hypothesis that the value is already within address range.
 
-### 4. setMappingPackedWord singleton (line 10548)
-**Theorem**: `stmtListGenericCore_singleton_setMappingPackedWordSingle_of_slotSafety`
-**Blocker**: Depends on #2 being resolved first (the `_preserves` theorem it wraps).
+## TYPESIG_SORRY Status
+
+| Group | Lines | Status | Blocker |
+|-------|-------|--------|---------|
+| mstore/tstore scope | 2838, 3860 | Blocked | Need `StmtListScopeCore` constructors |
+| setStorageAddr | 6150, 6196 | Blocked | Address.modulus (sorry #3) |
+| validateIdentifierShapes chain | 9289, 9345 | Blocked | sorry #1 |
+| ExceptMappingWrites chain | 11560, 11593, 11615, 11656 | Blocked | `SupportedStmtListMappingWriteSlotSafety` structure commented out (line 10159) |
+| Catalog assembly | 14830+ (9 blocks) | Dead code | Commented-out catalog infrastructure |
 
 ## Root Causes Summary
 
@@ -80,16 +86,17 @@ add a hypothesis that the value is already within address range.
 | ~~Keccak FFI opaque output bounds~~ | ~~#3, #5, #6, #7~~ | ~~RESOLVED: added axiom~~ |
 | ~~TYPESIG_SORRY dependency (aliasSlots)~~ | ~~#8~~ | ~~RESOLVED: proved chain~~ |
 | ~~ExprCompileCore missing constructors~~ | ~~#1~~ | ~~RESOLVED: added constructors~~ |
-| `execIRStmts` 5-stmt block + bitwise identity | #2, #4 | Dedicated helper theorem + bitwise lemma |
+| ~~setMappingPackedWord singleton~~ | ~~#4~~ | ~~RESOLVED: proved compileOk + chained~~ |
+| `execIRStmts` 5-stmt block + bitwise identity | #2 | Dedicated helper theorem + bitwise lemma |
 | `__immutable_*` field prefix | #1 | Validation pipeline change |
 | Address modulus semantic mismatch | #3 | IR compilation change or hypothesis |
 
 ## Conclusion
 
-The sorry count has been reduced from 44 to 4 (91% reduction). The remaining 4 sorries
+The sorry count has been reduced from 44 to 3 (93% reduction). The remaining 3 sorries
 fall into three categories:
 
-1. **Proof infrastructure needed** (#2, #4): The `setMappingPackedWord` proof requires a
+1. **Proof infrastructure needed** (#2): The `setMappingPackedWord_preserves` proof requires a
    dedicated helper theorem for the 5-statement block body execution (to isolate the
    expensive `sizeOf`/fuel computation within its own heartbeat budget) plus a bitwise
    identity lemma bridging IR and Uint256 operations. This is the most tractable remaining