Node 4: close C4's code-deposit half by running the pinned init images under Ξ

Eip8282.lean

@@ -15,6 +15,7 @@ import Eip8282.Audit.Guarantees.PControl1.Gate
 import Eip8282.Audit.Guarantees.PControl1.Excess
 import Eip8282.Audit.Guarantees.PControl1.Count
 import Eip8282.Audit.Guarantees.PControl1.Ctor
+import Eip8282.Audit.Guarantees.PControl1.CtorXi
 import Eip8282.Audit.AllGuarantees
 import Eip8282.Audit.Trust
 import Eip8282.Tests.Mutants

Eip8282/Audit/Guarantees/PControl1.lean

@@ -5,6 +5,7 @@ import Eip8282.Audit.Guarantees.PControl1.Gate
 import Eip8282.Audit.Guarantees.PControl1.Excess
 import Eip8282.Audit.Guarantees.PControl1.Count
 import Eip8282.Audit.Guarantees.PControl1.Ctor
+import Eip8282.Audit.Guarantees.PControl1.CtorXi
 
 namespace Eip8282.Audit.Guarantees.PControl1
 
@@ -700,11 +701,22 @@ def pcontrol1_c3_count_forall :=
     (@Count.system_count_reset)
 
 /-- C4: exit init stores `INHIBITOR` at slot 0 then returns runtime;
-deposit init does not `SSTORE`. Closes `initial_gating` on bytes. -/
+deposit init does not `SSTORE`. Closes `initial_gating` on bytes.
+
+The trailing conjunct is the code-deposit half. `Ctor`'s three facts are
+`rfl` on the first `++` chunk of each init hex — 32 of 638 bytes for
+deposit, 64 of 503 for exit — and never run the image.
+`CtorXi.pcontrol1_ctor_xi_parent` executes the *full* pinned init images
+under `EvmYul.EVM.Ξ` and pins the buffer each one returns to be
+`depositRuntime` / `exitRuntime` byte for byte, which is the `code` that
+`Λ`'s step (115) installs. That is the only thing in this repository
+connecting `pinned/bytecode/*/ctor.hex` to `pinned/bytecode/*/main.hex`;
+`audit/artifacts.lock.json` hashes them independently. -/
 def pcontrol1_c4_ctor_forall :=
   And.intro Ctor.initial_gating_bytes <|
-  And.intro (@Ctor.exit_ctor_stores_inhibitor)
-    (@Ctor.deposit_ctor_storage_zero)
+  And.intro (@Ctor.exit_ctor_stores_inhibitor) <|
+  And.intro (@Ctor.deposit_ctor_storage_zero)
+    CtorXi.pcontrol1_ctor_xi_parent
 
 /--
 **P-CONTROL-1 parent.** CFG-level `∀` under `WellFormed` / `CallHyp`
@@ -730,9 +742,19 @@ The leading conjunct pins what the CFG layer stepped against: the jumpdest
 tables the C1/C2/C3 runtime lemmas step against are the tables
 `EvmYul.EVM.Ξ` itself derives from the pinned runtime image, kernel-checked by
 `decide +kernel` (EVMYulLean 0ff72b2), not hand-written arrays that happen to
-look right. C4 is a no-jump init preamble and steps against no table, so the
-two init-image equalities in that conjunct stand on their own; they do not
-transport into or constrain `pcontrol1_c4_ctor_forall`.
+look right. C4's CFG half is a no-jump init preamble and steps against no
+table, so the two init-image equalities in that conjunct stand on their own;
+they do not transport into or constrain `pcontrol1_c4_ctor_forall`.
+
+C4's code-deposit conjunct is cut separately, on the **init** images rather
+than the runtimes: `Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent`
+flips the deposit `CODECOPY` source operand at ctor byte 5 (`0x0a` → `0x0b`)
+and the exit `SSTORE` at ctor byte 34 (`0x55` → `0x50`), and shows
+`CtorXi.ctorXiFacts` is `false` on each. Those bytes are unreachable from
+every runtime trace — `ctor_mutants_leave_runtime_guarantees_intact` proves
+`controlFacts` and `PSubmit1.submitFacts` stay true on the pinned runtimes
+under both cuts — so the code-deposit conjunct is load-bearing on bytes
+nothing else in this repository constrains.
 -/
 def pcontrol1_forall_conj :=
   And.intro Eip8282.Audit.Step.validJumps_are_Xi_tables <|

Eip8282/Audit/Guarantees/PControl1/CtorXi.lean

@@ -0,0 +1,140 @@
+import Eip8282.Audit.EvmRunner
+
+/-!
+C4, code-deposit half: the pinned **init** images run under `EvmYul.EVM.Ξ`.
+
+`Ctor.lean` closes C4 on a CFG prefix. Its own note is explicit about the
+gap: `fromHex` of the full init blobs times out in the kernel, so the
+opcode facts there are `rfl` on the *first* `++` chunk of `depositInitHex`
+and the first two chunks of `exitInitHex`. That reads the first 32 / 64
+bytes of a 638 / 503-byte image and never runs it. Three things were
+therefore unchecked:
+
+* that the init image reaches its `RETURN` at all;
+* that the buffer it returns is the pinned runtime **byte for byte**
+  rather than merely "a copy starting at the right offset";
+* that the exit ctor's `SSTORE` lands, as opposed to being present as an
+  opcode 34 bytes in.
+
+This module closes all three by executing the full pinned init images and
+comparing the returned buffer against the pinned runtime images.
+
+## What this is, and what it is not
+
+`Λ` (`EvmYul.EVM.Semantics.Lambda`, EVMYulLean `0ff72b2`) is `Ξ` on the
+init code followed by the code-deposit step (115): on success it writes
+`code := returnedData` into the new account. `initDeploys` below is
+exactly that `Ξ` half, plus the equality step (115) would use, stated
+against the pinned runtime image.
+
+It is deliberately **not** `Lambda` itself. `Lambda` derives its target
+address as `KEC(RLP(sender, nonce))`, and the EIP-8282 contracts are
+genesis predeploys at `0x0000bFF4…` / `0x000064D6…`, not `CREATE`
+outputs. Driving `Lambda` here would pin an address that is provably not
+the predeploy address, and would pull the `opaque @[extern]` keccak FFI
+into the trusted base for no gain. The bytes an init image actually
+*executes* are its preamble — 10 bytes for deposit, 45 for exit;
+everything after that is the runtime carried as `CODECOPY` data — and
+neither preamble contains a `SHA3`, `CREATE`, call or precompile-dispatch
+opcode, so running them under `Ξ` leaves the `A-NATIVE-DECIDE` disclosure
+exactly as `Ctor` and Wave-1 state it.
+
+This does **not** discharge `A-PINNED-SOURCE`. It links `ctor.hex` to
+`main.hex` inside the pin; it observes nothing on chain. The residual
+open part is the deployed-address / deployed-codehash observation — see
+`audit/assumptions.yaml`.
+-/
+
+namespace Eip8282.Audit.Guarantees.PControl1.CtorXi
+
+open EvmYul
+open EvmYul.EVM
+open Eip8282.Audit.Bytecode
+open Eip8282.Audit.EvmRunner
+
+/-- The init images halt in far fewer steps than a runtime call: each
+preamble is a `CODECOPY` and a `RETURN`. -/
+def CTOR_FUEL : Nat := 20000
+
+/-- Account that deploys the predeploy. Its identity is irrelevant to the
+init programs — neither image reads `CALLER` before returning. -/
+def deployer : Nat := 0x1234
+
+/-- `Ξ` on an init image, with the account being created holding no code.
+
+`Ξ` is entered with `executionEnv.code := initCode`, which is what
+`CODESIZE` / `CODECOPY` read during creation, while the account being
+created still has none. `EvmRunner.run` would additionally install
+`initCode` as that account's code; the pinned preambles never read their
+own account code, but leaving it empty is the faithful creation world. -/
+def runInit (fuel : Nat) (target : AccountAddress) (initCode : ByteArray)
+    : RunResult :=
+  let σ : AccountMap .EVM :=
+    (default : AccountMap .EVM)
+      |>.insert target (mkAccount ByteArray.empty)
+      |>.insert (toAddress deployer) (mkAccount ByteArray.empty oneEth)
+  Ξ fuel default default default σ σ defaultGas default
+    (callEnv target initCode (toAddress deployer) ZERO_U256 ByteArray.empty)
+
+/-- Return buffer of a successful `Ξ`; empty on revert or interpreter error. -/
+def returnBuffer (r : RunResult) : ByteArray :=
+  match r with
+  | .ok (.success _ o) => o
+  | _ => ByteArray.empty
+
+/-- The code-deposit step (115) of `Λ`, on bytes: running `initCode`
+succeeds, and the buffer it returns is exactly `runtime` — the value
+`Λ` would install as the new account's `code`. -/
+def initDeploys (target : AccountAddress) (initCode runtime : ByteArray) : Bool :=
+  let r := runInit CTOR_FUEL target initCode
+  isSuccess r && bytesEq (returnBuffer r) runtime
+
+/-- Deposit ctor: deploys `depositRuntime` and writes no storage. -/
+def depositCtorFact (initCode : ByteArray) : Bool :=
+  initDeploys depositAddr initCode depositRuntime
+    && slots0to3Are (runInit CTOR_FUEL depositAddr initCode) depositAddr 0 0 0 0
+
+/-- Exit ctor: deploys `exitRuntime` and leaves slot 0 = `INHIBITOR` with
+slots 1–3 untouched. -/
+def exitCtorFact (initCode : ByteArray) : Bool :=
+  initDeploys exitAddr initCode exitRuntime
+    && slots0to3Are (runInit CTOR_FUEL exitAddr initCode) exitAddr
+        ((2 ^ 256) - 1) 0 0 0
+
+/-- Both ctor facts, parameterised by the two init images so that a
+one-byte init mutant can be fed to exactly the statement the parent is
+registered against. -/
+def ctorXiFacts (depInit exitInit : ByteArray) : Bool :=
+  depositCtorFact depInit && exitCtorFact exitInit
+
+/--
+**C4 code-deposit trace, on pinned init bytecode.**
+
+`Ξ` on the full pinned 638-byte deposit init and 503-byte exit init
+images. Each returned buffer is the pinned `depositRuntime` /
+`exitRuntime` byte for byte — the `code` that `Λ`'s step (115) would
+install. The exit ctor additionally leaves slot 0 at `INHIBITOR` with
+slots 1–3 zero; the deposit ctor writes nothing.
+
+This is what ties `pinned/bytecode/*/ctor.hex` to
+`pinned/bytecode/*/main.hex`. `audit/artifacts.lock.json` hashes the two
+files independently, so until this theorem nothing in the repo ruled out
+a ctor that deploys something other than the runtime every other
+guarantee is proved about.
+
+Kill-line: `Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent`
+flips one byte of each init image — the deposit `CODECOPY` source offset
+at 5 (`0x0a` → `0x0b`) and the exit `SSTORE` at 34 (`0x55` → `0x50`,
+`POP`) — and shows `ctorXiFacts` is `false` on each.
+
+Discharged by `native_decide` for cost, on the same terms as the Wave-1
+traces: each image executes only its preamble before `RETURN`, and
+neither preamble contains a `SHA3`, `CREATE`, call or precompile-dispatch
+opcode, so no `opaque @[extern]` FFI constant and no `partial` RLP
+decoder is reached. See `A-NATIVE-DECIDE`.
+-/
+theorem pcontrol1_ctor_xi_parent :
+    ctorXiFacts depositInit exitInit = true := by
+  native_decide
+
+end Eip8282.Audit.Guarantees.PControl1.CtorXi

Eip8282/Audit/Trust.lean

@@ -171,3 +171,11 @@ only on the kept trace theorems.
 #print axioms Eip8282.Tests.PControl1Mutant.wave5_target_shifts_nonempty_excess
 #print axioms Eip8282.Tests.PControl1Mutant.wave5_mutants_leave_psubmit1_intact
 #print axioms Eip8282.Tests.PControl1Mutant.nonempty_is_not_empty
+
+-- C4 code-deposit half: Ξ on the full pinned init images (Node 4).
+#print axioms Eip8282.Audit.Guarantees.PControl1.CtorXi.pcontrol1_ctor_xi_parent
+#print axioms Eip8282.Tests.PControl1Mutant.pinned_ctor_bytes
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutants_differ_in_one_byte
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutants_are_independent
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutants_leave_runtime_guarantees_intact

Eip8282/Tests/PControl1Mutant.lean

@@ -270,4 +270,73 @@ theorem fold_equating_mutants_leave_psubmit1_intact :
     ∧ Eip8282.Audit.Guarantees.PSubmit1.submitFacts depositRuntime foldEquatingExit = true := by
   native_decide
 
+/-! ## Kill-line for the C4 code-deposit conjunct
+
+`CtorXi.ctorXiFacts` is cut on the **init** images, one byte each. These
+are bytes no runtime trace can reach: the init code is not the deployed
+code, so neither `controlFacts` nor `submitFacts` nor `drainFacts`
+constrains them. Before `pcontrol1_ctor_xi_parent` nothing in this
+repository did.
+-/
+
+open Eip8282.Audit.Guarantees.PControl1.CtorXi
+
+/-- Source offset of the runtime copy in the deposit ctor
+(`PUSH2 0x0274; DUP1; PUSH1 0x0a; PUSH0; CODECOPY`): the `0x0a` operand. -/
+def depositCtorSrcIdx : Nat := 5
+
+/-- The `SSTORE` of the exit ctor's `PUSH32 INHIBITOR; PUSH0; SSTORE`. -/
+def exitCtorSstoreIdx : Nat := 34
+
+/-- Sanity: the pinned init bytes really are what the mutations claim to cut. -/
+theorem pinned_ctor_bytes :
+    depositInit.size = 638
+    ∧ exitInit.size = 503
+    ∧ depositInit.get! depositCtorSrcIdx = 0x0a
+    ∧ exitInit.get! exitCtorSstoreIdx = 0x55 := by
+  native_decide
+
+/-- `CODECOPY` source `10` → `11`. The ctor still returns 628 bytes and
+still succeeds, but the buffer is the runtime shifted one byte, so the
+code deposited is not the code every other guarantee is proved about. -/
+def ctorSrcMutatedDeposit : ByteArray := depositInit.set! depositCtorSrcIdx 0x0b
+
+/-- `SSTORE` → `POP`. The exit ctor still deploys the right runtime, but
+slot 0 is left at 0 instead of `INHIBITOR`, so the exit contract starts
+un-inhibited — the exact failure C4 exists to exclude. -/
+def sstoreMutatedExit : ByteArray := exitInit.set! exitCtorSstoreIdx 0x50
+
+theorem ctor_mutants_differ_in_one_byte :
+    ctorSrcMutatedDeposit.size = depositInit.size
+    ∧ ctorSrcMutatedDeposit.get! depositCtorSrcIdx = 0x0b
+    ∧ sstoreMutatedExit.size = exitInit.size
+    ∧ sstoreMutatedExit.get! exitCtorSstoreIdx = 0x50 := by
+  native_decide
+
+/-- **The C4 code-deposit kill-line.** `ctorXiFacts` is the conjunct
+`pcontrol1_c4_ctor_forall` carries, so each cut also makes the registered
+`pcontrol1_forall_parent` false of the mutated init image. -/
+theorem ctor_mutant_refutes_parent :
+    ctorXiFacts ctorSrcMutatedDeposit exitInit = false
+    ∧ ctorXiFacts depositInit sstoreMutatedExit = false := by
+  native_decide
+
+/-- The two cuts are independent: the shifted-copy mutant leaves the exit
+ctor alone and the lost-`SSTORE` mutant leaves the deposit ctor alone. -/
+theorem ctor_mutants_are_independent :
+    depositCtorFact ctorSrcMutatedDeposit = false
+    ∧ exitCtorFact exitInit = true
+    ∧ depositCtorFact depositInit = true
+    ∧ exitCtorFact sstoreMutatedExit = false := by
+  native_decide
+
+/-- The init cuts leave every runtime guarantee intact: the deployed code
+is a different byte string from the init code, so no runtime trace can
+see these bytes. This is what makes the C4 code-deposit conjunct
+load-bearing rather than a restatement. -/
+theorem ctor_mutants_leave_runtime_guarantees_intact :
+    controlFacts depositRuntime exitRuntime = true
+    ∧ Eip8282.Audit.Guarantees.PSubmit1.submitFacts depositRuntime exitRuntime = true := by
+  native_decide
+
 end Eip8282.Tests.PControl1Mutant

README.md

@@ -162,8 +162,22 @@ Two disclosed costs, both in `audit/assumptions.yaml`:
   parents are under `WellFormed` / `CallHyp`. `A-ABSTRACT-TX` stays: F4
   did not prove `Ξ ↔ Model`.
 
-Deployment provenance is out of the current claim. P-CONTROL-1's C4 lemmas
-are CFG prefixes of the pinned init bytecode, not `Ξ` CREATE traces.
+Deployment provenance is still out of the current claim, but C4 no longer
+stops at a CFG prefix. `PControl1.CtorXi.pcontrol1_ctor_xi_parent` runs the
+full pinned 638-byte deposit and 503-byte exit init images under
+`EvmYul.EVM.Ξ` and pins the buffer each returns to be `depositRuntime` /
+`exitRuntime` byte for byte — the `code` that `Λ`'s step (115) installs —
+with the exit ctor leaving slot 0 at `INHIBITOR`. That is what ties
+`pinned/bytecode/*/ctor.hex` to `pinned/bytecode/*/main.hex`;
+`audit/artifacts.lock.json` hashes the two files independently.
+
+It is deliberately not `Λ` itself. `Λ` derives its address as
+`KEC(RLP(sender, nonce))`, and the EIP-8282 contracts are genesis
+predeploys, not `CREATE` outputs — so driving `Λ` would pin an address
+that is provably not the predeploy address. No address derivation is
+claimed, and `A-PINNED-SOURCE` stays **open**: nothing here observes chain
+state. What remains is a single observation — the live codehash at
+`0x0000bFF4…` / `0x000064D6…` against keccak of the pinned `main.hex`.
 
 The three IDs are the smallest coherent audit surface:
 

audit/assumptions.yaml

@@ -59,12 +59,12 @@
     {
       "id": "A-PINNED-SOURCE",
       "accepted": true,
-      "risk": "Assembly and EIP text are pinned snapshots, not live-deployed bytecode.",
-      "justification": "sys-asm@83f9801 and EIPs PR #12120 head b759aae8 are the working references.",
+      "risk": "Assembly and EIP text are pinned snapshots, not live-deployed bytecode. STILL OPEN. Node 4 closed the ctor-to-runtime half only: nothing here observes chain state, and no deployed codehash is claimed.",
+      "justification": "sys-asm@83f9801 and EIPs PR #12120 head b759aae8 are the working references. Within the pin, the two bytecode files are no longer independent: Eip8282.Audit.Guarantees.PControl1.CtorXi.pcontrol1_ctor_xi_parent runs the full pinned ctor.hex images under EvmYul.EVM.Ξ and shows each returns main.hex byte for byte, which is the code Λ step (115) installs. So keccak(deployed code) is determined by ctor.hex given the pin. What remains assumed is that these files are the images actually at 0x0000bFF46984e3725691FA540a8C7589300D8282 and 0x000064D678505ad48F8cCb093BC65613800E8282.",
       "severity": "HIGH",
-      "violation_impact": "A later sys-asm or EIP revision can invalidate the model.",
-      "validation": "audit/artifacts.lock.json sha256 of pinned files.",
-      "removal_path": "Add deployed-bytecode observation and keccak identity."
+      "violation_impact": "A later sys-asm or EIP revision can invalidate the model. Because the predeploys are genesis-installed rather than CREATE outputs, no address derivation is proved either: Λ's KEC(RLP(sender,nonce)) address is not the predeploy address, so CtorXi deliberately does not invoke Lambda and the deployed-address binding is untouched.",
+      "validation": "audit/artifacts.lock.json sha256 of pinned files, plus PControl1.CtorXi.pcontrol1_ctor_xi_parent tying ctor.hex to main.hex inside the pin. Kill-line: Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent.",
+      "removal_path": "Observe the live codehash at the two predeploy addresses and check it against keccak of the pinned main.hex. The ctor-to-runtime link is now proved, so that single observation would close this assumption."
     }
   ]
 }