audit/DIRECT-CLOSURE.md

1 # Direct closure of the three agreed guarantees2 3 Implementation of Thomas's approved 9 September 2026 plan. This document is an4 evidence map, not a replacement for the structured sandboxed.sh task ledger.5 The only public IDs remain P-SUBMIT-1, P-DRAIN-1 and P-CONTROL-1.6 7 ## Current local candidate: ordinary transaction block incorporation8 9 `ReferenceFullFeeBlockTotal.verified` takes the same fee-finalized ordinary10 source journal that `ReferenceFullFeeTotal.verified` produces and incorporates11 it into the source block. One actual computation supplies the three12 conditional claims, the exact frame receipt, full logs/rollback/meter, ordered13 fee credits and the checked sender nonce. The final journal has a finite,14 duplicate-free account write enumeration over sender, contract and beneficiary15 and a finite storage write enumeration over the contract; code hashes are16 unchanged and the code write overlay stays empty.17 18 Account BAL updates precede storage BAL updates and both compare against the19 unmerged block parent. The U32 index is preserved, the sender nonce converts20 through the checked U64 path, every other nonce is unchanged, cumulative21 account/storage reads are merged, and the returned transaction journal is22 fresh. Post-incorporation account reads agree with the settled journal;23 contract storage reads agree with the receipt and foreign storage is untouched.24 25 Two initial conditions are explicit additions to the balance-only fee domain:26 the source sender nonce read equals the admitted old sender nonce, and the27 initial account/code write overlays are fresh. Final support, conversions,28 successful merge and the fresh reset are conclusions, not premises.29 30 Source `f2ab5eb37c8a436c4cf2e74059dd71520e0ad73a` passes frozen `make check`31 (3608 jobs, `check ok`), 28 production axiom checks and eight targeted32 nonce/merge-order/alias mutations. Only `propext`, `Classical.choice` and33 `Quot.sound` occur. See the34 [bundle](receipts/direct-ordinary-block-bundle-20260911.json),35 [build](receipts/direct-ordinary-block-build-20260911.json),36 [axioms](receipts/direct-ordinary-block-axioms-20260911.json) and37 [rechecked complete source provenance](receipts/direct-ordinary-block-sources-20260911.json).38 The SYSTEM block pair `cb65536`, SYSTEM success `a612bbb` and ordinary fee39 settlement `eec2142` remain included without changing their proved domains.40 41 | Original clause family | Current composed consumer | Domain and material limit | Source commit |42 | --- | --- | --- | --- |43 | P-SUBMIT-1 admission, authentic record/log and local failure | `ReferenceFullFeeBlockTotal.verified`; SYSTEM exclusion also in `ReferenceCheckedSystemBlock.verified` | Represented nonblob ordinary transaction admission, initialized History and explicit initial nonce correspondence; full local logs/fees and block incorporation, not canonical ancestry | `f2ab5eb`, `cb65536` |44 | P-DRAIN-1 SYSTEM FIFO/caps/output/storage and user exclusion | `ReferenceCheckedSystemBlock.verified` plus `ReferenceFullFeeBlockTotal.verified` | Mandatory empty-data SYSTEM pair succeeds within source grants with derived block-parent composition. Complete canonical block applicability remains open | `cb65536`, `f2ab5eb` |45 | P-CONTROL-1 quote/append updates and SYSTEM empty-data update/unlock | Same two consumers | Exact ordered word operations and existing mathematical agreement domain. Nonempty SYSTEM/inhibition clauses retain earlier conditional evidence; no schedule or policy adoption | `cb65536`, `f2ab5eb` |46 47 The source functions are audited functional transcriptions with complete48 archived bodies rehashed at this commit: transaction-state journals and49 incorporation order, nonce validation and check, sender-state update and fee50 finalization order, and the BAL balance/nonce/code/storage update rules. No51 Python exception-state rollback, whole-container insertion-order/serialization52 refinement, whole-block BAL size/read admission or final block validation is53 claimed. Nonce fixtures in the mutation module are injected projection54 witnesses, not canonical counterexamples.55 56 Canonical Ethereum production of the initialized funded History, the57 next-transaction History after this incorporation, complete admission,58 deployment, SYSTEM authorization, inhibition and upgrade applicability remain59 open. Synthetic replay gas is never source gas; there is no 256-iteration60 ceiling; the tariff agreement domain (numerator ≤2892) and the 2893 divergence61 remain explicit. The structured task ledger is the only roadmap.62 63 Independent exact review on the ordinary block candidate is now CLEAN:64 [report](reviews/spark-review-f2ab5eb.md) covers `a612bbb`, `5cd0fe5`,65 `cb65536` and `f2ab5eb` together (fresh-context reviewer, not the author),66 with zero blocking and zero advisory findings. The earlier67 [review-status receipt](receipts/direct-ordinary-block-review-status-20260911.json)68 recorded the quota outage that preceded this review. Local promotion is69 recorded here only; PR20 remains `c3f3c1d`, and prepared documentation70 `7e2ef006` stays unpushed. No external message or normative policy has been71 promoted.72 73 ## Preserved SYSTEM candidate: ordered checked SYSTEM block pair74 75 `ReferenceCheckedSystemBlock.verified` composes the two successful mandatory76 SYSTEM drains with their actual storage incorporation. Deposit's returned77 journal becomes Exit's source parent. The same intermediate replay world78 supplies Exit's three predicates; global storage reads at every address agree79 with that world and then with the final world. Both protected invariants at80 these boundaries are derived from the initial history.81 82 The source BAL update compares final writes against the **unmerged** parent,83 checks key length before big-endian conversion, and retains the incoming U3284 index. Its enumeration contains every actual write, no extra write and no85 repeated key. Complete account/code write journals are proved empty, cumulative86 account/storage reads are merged, and the transaction journals are cleared.87 Source events, meters, terminal, logs, output, account reads and final warmth88 remain tied to the same checked trace and receipt.89 90 The intermediate parent/world relation, Exit invariant, finite write support,91 key-conversion success, empty account/code writes and trace-consistent warmth92 are conclusions. No independent intermediate equality, successful endpoint,93 final meter, final journal or new funded History at Exit entry is assumed.94 95 Source `cb655365674ef9173e1e4587ee89ad4291024163` passes frozen `make check`96 (session 95447, collected exit 0), 35 production axiom checks and six targeted97 mutations. Only `propext`, `Classical.choice` and `Quot.sound` occur. See the98 [bundle](receipts/direct-system-block-bundle-20260911.json),99 [build](receipts/direct-system-block-build-20260911.json),100 [axioms](receipts/direct-system-block-axioms-20260911.json) and101 [rechecked complete source provenance](receipts/direct-system-block-sources-20260911.json).102 The preceding same-evaluator SYSTEM success `a612bbb` and ordinary fee103 settlement `eec2142` remain included without changing their proved domains.104 105 | Original clause family | Current composed consumer | Domain and material limit | Source commit |106 | --- | --- | --- | --- |107 | P-SUBMIT-1 admission, authentic record/log and local failure | `ReferenceFullFeeTotal.verified`; SYSTEM exclusion also in `ReferenceCheckedSystemBlock.verified` | Represented nonblob ordinary transaction admission and initialized History; full local logs/fees, not canonical ancestry | `eec2142`, `cb65536` |108 | P-DRAIN-1 SYSTEM FIFO/caps/output/storage and user exclusion | `ReferenceCheckedSystemBlock.verified` plus `ReferenceFullFeeTotal.verified` | Mandatory empty-data SYSTEM pair succeeds within source grants; actual storage/receipt/block-parent composition is derived. Complete canonical block applicability remains open | `cb65536`, `eec2142` |109 | P-CONTROL-1 quote/append updates and SYSTEM empty-data update/unlock | Same two consumers | Exact ordered word operations and existing mathematical agreement domain. Nonempty SYSTEM/inhibition clauses retain earlier conditional evidence; no schedule or policy adoption | `cb65536`, `eec2142` |110 111 The initial domain is the existing initialized `ReleaseCandidate.History`112 before this pair, the represented initial storage world, successful fresh113 source code loads for both pinned runtimes, and source account/code parents,114 cumulative read sets and a BAL builder with U32 index. History's constructor,115 financing, credit-count and block-slot conditions remain explicit; their116 canonical Ethereum production has not been established.117 118 At the audited EL pin, these adjacent calls occur in119 `process_general_purpose_requests`, after the withdrawal/consolidation request120 calls. The earlier `apply_body` step sets the post-execution index to checked121 `U32(transaction_count+1)`. The theorem starts at the pair entry and preserves122 its input index; it does not derive that preceding block execution or the123 final whole-block BAL size/admission checks.124 125 The source functions are audited functional transcriptions, with complete126 archived bodies and checked hashes. Mechanical Python/bytes/dictionary127 refinement, insertion-order/BAL serialization and full account/code payload128 correspondence remain trust boundaries. The failure marker in the successful129 BAL projection does not model partial Python builder mutations on exceptions;130 derived valid keys exclude that branch in this consumer.131 132 The original guarantees, author draft, tariff divergences and earlier133 conditional results remain in `audit/release/`. The mathematical tariff is134 not silently replaced: the agreement domain (numerator ≤2892) and the 2893 divergence135 remain explicit. There is no 256-iteration ceiling. Synthetic replay gas is136 never source gas, and local returned effects are not ancestor commitment.137 Canonical funded histories, complete call-tree occurrence accounting/global138 gas, deployment, SYSTEM authorization, inhibition and upgrade applicability139 remain open. The structured task ledger is the only roadmap.140 141 Independent exact review on the SYSTEM block pair is now CLEAN as part of the142 same [combined report](reviews/spark-review-f2ab5eb.md) noted above (fresh143 context, not the author). The earlier144 [review-status receipt](receipts/direct-system-block-review-status-20260911.json)145 records the prior quota outage. PR20 remains `c3f3c1d`, and prepared146 documentation `7e2ef006` remains unpushed. No unreviewed extension,147 external message or normative policy has been promoted.148 149 ## Preserved ordinary-call candidate: same-frame guarantees, gas and fee balances150 151 `ReferenceFullFeeTotal.verified` preserves the exhaustive three-guarantee,152 full-log and source-gas certificate and derives ordered fee disbursement from153 that same settled receipt. The initial history and fee debit fund both credits;154 no final balance budget, overflow guard or disbursement success is assumed.155 All account balance changes are exact natural amounts, including equal payer156 and beneficiary. Queue/control storage is identical to the settled receipt.157 Refund, tip and calculated base-fee burn partition the upfront execution fee.158 159 Source `eec2142d7bbc97b4d03fff5d912bb8953a485b5c` passes frozen `make check`,160 15 production axiom checks and four ordered-credit/zero/overflow mutations.161 The first source `54d884e` failed the aggregate import-order check; the fix and162 new successful check are recorded explicitly. See the163 [bundle](receipts/direct-source-fee-finalization-bundle-20260910.json),164 [build](receipts/direct-source-fee-finalization-build-20260910.json),165 [axioms](receipts/direct-source-fee-finalization-axioms-20260910.json) and166 [source excerpts](receipts/direct-source-fee-finalization-sources-20260910.json).167 Prior full-gas `20783d3` and full-log `9e79b3f` evidence remains included.168 169 The domain is unchanged from FullGasTotal: represented nonblob ordinary calls,170 selected source admission conditions and before-transaction history/source171 correspondences, plus a fresh storage overlay/read/created journal. The parent172 chain storage may be nonempty. These conditions are not canonical Ethereum173 reachability. The exact EVM-word tariff and mathematical agreement domain are174 unchanged, with no 256-iteration ceiling. Synthetic replay and source gas remain175 separate; frame log eligibility is distinct from ancestor commitment.176 177 Full Python/dictionary/byte/hash refinement, source block incorporation and178 next-transaction history, complete call-tree commitment, deployment, SYSTEM,179 inhibition and upgrade applicability remain open. Fee balance observations do180 not assert equality of full source account payloads with old replay worlds.181 182 Independent exact review is now CLEAN on both `20783d3` (full gas settlement)183 and `eec2142` (source fee finalization): fresh-context reviewer, not the184 author; zero blocking findings; one advisory documenting an additive185 re-export in `ReferenceOutcomeGas.lean` at the later commit `5cd0fe5` that is186 semantically neutral. See [report](reviews/spark-review-20783d3.md). Earlier187 [review-status receipts](receipts/direct-source-fee-finalization-review-status-20260910.json)188 retain the pre-review evidence chain. PR20 remains `c3f3c1d`; prepared189 documentation `7e2ef006` remains unpushed. Checked SYSTEM execution,190 successful source payment, the ordered SYSTEM block-parent/world composition191 and ordinary transaction block incorporation are now composed above.192 Next-transaction history remains open. The existing structured task ledger193 remains the sole roadmap.194 195 The following sections identify earlier theorem layers and their original196 verification domains. Their remaining gaps are evaluated against the current197 candidate above, not treated as new parallel work.198 199 ## Exhaustive computed allocated-call certificate — candidate200 201 `ReferenceAllocatedTotal.verified` no longer assumes an evaluator endpoint.202 From the same explicit allocated-entry domain, it constructs sufficient203 computational fuel and an actual supported result. Terminal/EOF supply the204 same three-predicate receipt and source settled balances; exceptional failure205 supplies the same complete local rollback receipt. The conclusion excludes206 unsupported/unfinished cases using reached pinned-runtime sites and actual207 evaluator extraction. Computational completion is distinct from EVM success.208 209 `Started` and `Result` name conclusions, never additional input premises.210 The earlier arbitrary finite outcome-specific theorems remain unchanged.211 Source gas and synthetic replay gas, local frame effects and ancestor commitment,212 and source transcriptions and canonical Python/Ethereum applicability remain213 distinct. This earlier API exposes protected-owner logs only; the current214 full-frame transport is composed above, while Python extraction remains open.215 216 Source `245e02bcee5bf0c205562ba3f1e793758345d29f` passes frozen `make check`,217 nine production axiom checks and two mutations; see the218 [build](receipts/direct-allocated-total-build-20260910.json) and219 [bundle](receipts/direct-allocated-total-bundle-20260910.json).220 Independent exact review is unavailable and there is no promotion.221 222 ## Computed source dispatch and allocated meter — candidate223 224 `ReferenceAllocatedGuarantees.terminal/eof` and `ReferenceAllocatedFailure.settled`225 start the same checked evaluator from the computed dispatch/value-entry journal226 and source split allocation. Actual pinned code reads derive the ready dispatch227 branch and exact accumulated account reads. Selected source nonce/fee/floor228 checks plus explicit sender presence derive funding admission and calldata fit.229 The computed call intrinsic and its two explicit admission checks derive pool230 conservation and executable potential at most16777216; a free30000000 bound is231 no longer an input to these APIs.232 233 This domain is represented nonblob ordinary calls without authorizations, with234 before-transaction initialized history and source observations as before.235 Charged/delegated preparation continuations remain separate prefix results;236 full Python construction/extraction, canonical validation/history and complete237 source logs are not established. Prior APIs remain unchanged. See the238 [bundle](receipts/direct-dispatch-allocation-bundle-20260910.json).239 Source `b8de01363430e093ef3211b162e11cec7d5adb85` passes frozen `make check`,240 thirteen production axiom checks and four mutations; see the241 [build](receipts/direct-dispatch-allocation-build-20260910.json).242 Independent exact review is unavailable; no promotion.243 244 ## Constructed initial access sets and jump destinations — candidate245 246 `ReferenceInitializedGuarantees.terminal/eof` and247 `ReferenceInitializedFailure.settled` consume storage warmth constructed from the248 represented transaction access list and destinations scanned from the same249 pinned code. `WarmRelated` and `DestinationContext` are derived. Transfer mode250 is specialized to source top-level `True`; the previous APIs remain unchanged.251 This is not a proof of complete `create_evm` preparation or Python extraction.252 Source meter, calldata fit and the earlier before-journal/history/admission253 conditions remain explicit. Protected-owner logs remain distinct from source254 transfer logs at SYSTEM_ADDRESS.255 256 Source `c9a8066a1455d88f046d41b881113b95c00dfeed` passes frozen `make check`,257 seven production axiom checks and four mutations. See the258 [build](receipts/direct-initial-access-build-20260910.json) and259 [bundle](receipts/direct-initial-access-bundle-20260910.json).260 Independent review remains unavailable; this contribution is not promoted.261 The next consumer connection is actual dispatch preparation and allocated gas.262 263 ## Source prepayment from the before-transaction journal — candidate264 265 [The prepayment candidate](receipts/direct-source-prepayment-bundle-20260910.json)266 adds `ReferencePrepaidGuarantees.terminal/eof` and267 `ReferencePrepaidFailure.settled`. Its input journal is now before gas268 prepayment: the ordered source operation derives successful prepayment and269 all checkpoint code, slot and balance bindings. The same complete receipt still270 carries all three predicates and source settled balances. A failed call restores271 the computed post-prepayment snapshot, retaining fee debit and nonce increment.272 273 This stronger connection has an explicit additional domain: represented274 legacy/access/dynamic transactions, excluding blobs. Their source and old blob275 charges are both zero; the differing blob tariff formulas are not identified.276 The earlier checkpoint APIs remain unchanged. Source type4, full constructor/277 preparation/gas/warm binding and canonical admission/history remain open.278 279 Source `eb373cd2654dc018c685cd55d882dd4c451d172d` passes frozen `make check`,280 fifteen production axiom checks and four mutations; see281 [build](receipts/direct-source-prepayment-build-20260910.json).282 Independent review is unavailable; no promotion or PR update is made. The283 mutations cover nonce-before-fee ordering and retained nonce effects on fee284 underflow, using explicitly injected finite journals rather than canonical285 reachability claims. Every new helper is consumed by these complete-call APIs.286 287 ## Before-transaction history at the actual checkpoint — candidate288 289 The [checkpoint composition](receipts/direct-checkpoint-bundle-20260910.json)290 adds `ReferenceCheckpointGuarantees.terminal/eof` and291 `ReferenceCheckpointFailure.settled`. They derive the selected call's invariant,292 work bound, code and funding from history **before the transaction** and its293 explicit admission. They no longer require a separate history after prepayment294 or an independently funded call. The same replay receipt still carries all295 three guarantees and settled source balance observations.296 297 Call rollback restores the snapshot after gas prepayment and nonce increment,298 before transferring call value. It does not refund all transaction fees. A299 mutation with30001wei initially,30000wei prepaid and1wei call value detects300 substituting the before-transaction world for the actual selected checkpoint.301 This injected fixture is not a canonical transaction/history certificate.302 303 Source `be85ecff8e639fe9bbfb1cc888ec081ce3ffaa0e` passes frozen `make check`,304 eleven production axiom checks and two mutations; see305 [build](receipts/direct-checkpoint-build-20260910.json). Independent exact306 review is unavailable and there is no promotion. Source checkpoint representation is307 still an input to those APIs; the nonblob prepayment extension above derives it.308 The old admission interface does not establish Amsterdam blob tariff equality,309 source frame/gas identity or type4 semantics. These boundaries are unchanged.310 311 ## Same-receipt source balances candidate — not promoted312 313 The current proof workspace strengthens the source-funding candidate with314 [16 balance/composition exports](receipts/direct-source-balance-bundle-20260910.json).315 `ReferenceSourceBalancedGuarantees.terminal/eof` compose the three predicates316 with balance observations of the **same settled receipt world**. The source317 transfer, finite checked execution, old pinned runtime balance preservation318 and frame rollback supply the connection. No post-balance equality is assumed.319 `ReferenceSourceBalancedFailure.settled` recovers the original balances alongside320 the same failed-frame storage/write/log/output/meter receipt.321 322 These stronger terminal/EOF results additionally require ordinary transfer mode323 (`shouldTransfer = true`) or zero actual value. Previous funded APIs are unchanged.324 Initial balance/code/slot representation and caller funding remain explicit;325 canonical source-frame/admission/history producers remain open. This does not326 identify source gas with replay resources, prove optional-account identity,327 or turn local success into ancestor commitment.328 329 Source `8cea382d101eebb3b54f8e357fb306dac6c57edd` passes frozen `make check`,330 16 production axiom checks and the two new balance mutations; see331 [build](receipts/direct-source-balance-build-20260910.json).332 [Independent exact review is unavailable](receipts/direct-source-balance-review-status-20260910.json);333 this candidate has not entered the reviewed branch or PR.334 The publication PR is still #20 at `c3f3c1d644d9e641585dfc5143100123729fd0e4`.335 A separate refresh at `7e2ef006c0e3bfafaf98f40eb9768560ad03fe16` contains only the336 reviewed snapshot `12806f9` and current publication documents. Its 433 proof/build337 inputs match the prior verified source; exact document review is unavailable338 because the existing reviewer exhausted quota. It has not been pushed.339 340 ## Funded source entry candidate — final review pending341 342 Source `8e92a8bc783862fec9ef602151743fff66eb43a6` on the separate343 `codex/source-funding-candidate-20260910` branch adds344 [the source funding candidate](receipts/direct-source-funding-bundle-20260910.json).345 The reviewed source branch remains at `12806f9`; the timed release is unchanged.346 `ReferenceSourceTransferFunding.after_history` derives successful checked347 source transfer from initial balance observations and caller funding, with the348 wealth bound supplied by the initialized ledger. It handles self-transfers and349 zero-balance account cleanup without asserting account-object identity.350 351 `ReferenceSourceFundedEntry.prepared` supplies entry admission and runtime352 slots to both all-three terminal/EOF consumers and the failed-frame consumer.353 An independent `entered` premise and independent post-transfer slot binding354 are removed from these new public APIs. A concrete account-field image proves355 the balance relation for represented replay; actual Python PreState/frame356 correspondence and canonical sender admission remain open.357 358 Ten production exports and two added funding mutations pass target compilation.359 Full frozen `make check` passes, including standard-only axioms for all ten new360 exports and the source funding mutations; see [build](receipts/direct-source-funding-build-20260910.json).361 Component source review was clean, but the362 existing reviewer exhausted its quota before final exact-commit review; see363 [review status](receipts/direct-source-funding-review-status-20260910.json).364 This candidate is not promoted to the independently reviewed release. Work on365 independent proof obligations continues without new worker jobs or spending.366 367 ## Guarded source transfer and pre-transfer rollback368 369 Proof commit `f9c7953771129f05c4b1b4c72f12f5dbc588c425` adds370 [the source transfer bundle](receipts/direct-source-transfer-bundle-20260910.json).371 `ReferenceSourceValueTransfer` preserves exact checked debit/credit order,372 empty-account cleanup, self-transfers, source transfer guard and partial errors.373 It represents the endpoint of each `modify_state`: its temporary updated-account374 write and repeated emptiness-check read collapse to the final overlay/read set.375 It does not assert an account-write event trace.376 For a nonempty code hash, the protected code and storage survive. Its read377 preservation lets the consumer reuse the actual fetch before transfer without378 inventing a second read effect.379 380 `ReferenceTransferredFailure.settled` consumes pre-transfer code and slots,381 derives the runtime entry relations and fault classification, and restores the382 same pre-transfer journal. Account/storage/code/transient writes return to that383 snapshot; live account/storage reads and created metadata remain. The new384 kernel mutation rejects unconditional storage preservation for empty-code385 self-transfers. The older `ReferenceValueTransfer` account-map parity proofs386 remain byte-for-byte unchanged.387 388 The 14 production and two mutation exports pass targeted compilation. Frozen389 full verification and exact independent review PASS; evidence is recorded in390 [build](receipts/direct-source-transfer-build-20260910.json) and391 [review](receipts/direct-source-transfer-review-20260910.json).392 Source transfer success, actual account payload/world representation,393 code-address/current-target/should-transfer construction, source LOG3/context394 binding, full Python frame identity and canonical admission are still open.395 These additions are outside the unchanged timed release.396 397 ## Derived source failure classification398 399 Proof commit `af027e8bdfefe1f0bea92737dd3b0862c35dd3d1` adds the400 [derived failure bundle](receipts/direct-derived-failure-bundle-20260910.json).401 The same failed account-aware evaluation now derives its final calldata/PC402 conversion bounds and excludes the owner assertion using its nonempty code403 fetch. `ReferenceHistoryFailure.settled` obtains the old replay owner from the404 initialized history, then proves projected storage rollback, zero parent logs,405 empty exceptional output and the ordered meter settlement. No independent406 `caught` classification or old `HasOwner` is supplied by this history consumer.407 408 All 14 new exports compile with standard Lean axioms; the exact isolated409 `make check` passes, including existing mutation checks. Evidence:410 [build](receipts/direct-derived-failure-build-20260910.json) and411 [review](receipts/direct-derived-failure-review-20260910.json).412 Actual source entry construction, code-address/current-target identity,413 account/value-transfer state and full saved snapshot binding remain open.414 In particular, source `process_call` transfers value before opcodes and may415 emit a SYSTEM-address LOG3; `modify_state` may delete a newly empty account.416 The opcode projection does not silently discard or justify these source effects.417 The frozen timed release under `audit/release/` is unchanged.418 419 ## Post-release source account composition420 421 The frozen release remains `58c2a60` (proofs `d46fa07`). Work continues on422 `codex/source-account-composition-20260910` toward Ethereum applicability.423 The [account bundle](receipts/direct-account-bundle-20260910.json) adds literal424 optional-account lookup, post-charge SSTORE account reads and a complete425 account-aware checked evaluator. Every finite evaluation projects to the same426 checked result, including computational exhaustion and exceptional outcomes;427 completed outcomes preserve account writes. Its terminal/EOF outputs now feed428 the same three history-derived guarantees without an independent owner Bool.429 430 Source dictionary/current-target identity, account payload/value-transfer and431 full frame/ancestor snapshot restoration remain open. This is a local source432 projection, not a canonical source-world or gas equivalence theorem. Fourteen433 exports pass target checks with standard axioms; isolated full check and434 independent exact-commit review pass at `f5f7a36`435 ([build](receipts/direct-account-build-20260910.json),436 [review](receipts/direct-account-source-review-20260910.json)). No released claim or EIP/protocol policy is changed.437 438 ## Scoped release of 10 September 2026439 440 The user authorized revised audit claims on a precise domain, without EIP or441 protocol-policy changes. [Release claims](release/CLAIMS.md) and the442 [clause map](release/CLAUSE-MAP.md) compose actual factory/history invariants443 into the next complete call, sufficient-resource getter/submission and a real444 inhibition cycle. The [release report](release/REPORT.md) records full compilation,16 new445 standard-axiom exports, mutation checks and independent review PASS at d46fa07. Ethereum applicability remains open; this conditional release does not446 close that broader roadmap. Earlier snapshots below are historical evidence.447 448 ## Current snapshot449 450 The registered direct parents for all three IDs are checked under explicit451 local input domains; all six required mutations refute those same predicates.452 Protocol coverage remains PARTIAL/OPEN. Correctness parents and the new453 supporting proofs use standard Lean axioms only; five historical finite mutant454 witnesses retain their disclosed native receipts.455 456 The [checked outcome bundle](receipts/direct-checked-outcomes-bundle-20260910.json)457 adds six modules and 31 exports. Genuine EOF is connected to the same pinned458 execution only after deriving the absent code byte; source PC is unchanged.459 Caught exceptional failures and REVERT have distinct projected storage, meter,460 output and log effects. Builtin conversion and owner-assertion faults remain461 explicitly uncaught at the pinned source boundary.462 463 All evaluated outcomes preserve the same baseline and committed spill. Literal464 child initialization now supplies the failed-child incorporation assertions,465 including after a partially executed failing opcode. The log context carries a466 fixed incoming prefix; the checked trace and terminal produce the new suffix,467 which alone may be forwarded. Failed/reverted frames retain internal logs for468 executed-effect accounting but contribute no logs to their parent.469 470 These are exact local source projections. Actual full account/code/transient471 snapshot restoration, source initial log/value-transfer bindings, parent/frame472 identity, complete retained occurrence coverage and canonical funded histories473 remain open. Component checks, full frozen check and exact-commit review pass at474 `fe81dc501fad4fee657a44935c5648855c51a1d0`; see475 [build](receipts/direct-checked-outcomes-build-20260910.json) and476 [review](receipts/direct-checked-outcomes-review-20260910.json). No protocol decision was adopted.477 478 Source `778f2d5` adds the [computed evaluator bundle](receipts/direct-checked-evaluator-bundle-20260910.json)479 adds six modules and 24 exports. The dispatcher computes a handler from current480 code/PC, using the complete pinned 153-tag Ops table. Invalid opcode, EOF and a481 valid unsupported opcode have distinct outcomes. The evaluator produces its482 own checked prefix and exact last result. Initial potential plus one is a483 sufficient computation budget from bounded stack/aligned entry; no fixed loop484 ceiling is imposed and failure remains separate from success.485 486 The computed terminal result now produces actual pinned bytecode evaluation487 with the same environment, storage, logs, stack, memory and output. Numerical488 nested transaction location derives the replay resource cap. Actual source489 frame/world bindings, complete occurrence identity, source journal restoration,490 canonical funded history and unresolved protocol decisions remain open. Genuine491 EOF is retained; REVERT observations are internal. Component builds and reciprocal492 reviews pass, together with [full frozen validation](receipts/direct-checked-evaluator-build-20260910.json)493 and [exact-commit review](receipts/direct-checked-evaluator-review-20260910.json).494 495 The newly fetched Hermes FeeQuoteLoop helper is [reviewed here](receipts/direct-hermes-feequote-loop-review-20260910.json).496 Its dependencies are identical to the integrated originals; existing quote497 consumers already use their facts. No alias-only refactor was introduced. One498 misleading vacuous zero-budget lemma name remains a review objection.499 500 Source `da1c6f7` adds the [checked runtime bundle](receipts/direct-checked-runtime-bundle-20260910.json)501 adds 11 modules and 37 exports. All 41 protected nonterminal handler variants502 now produce actions, exact ordered prices, payment and stack bounds from their503 literal checked result. One finite trace threads these same states and meters;504 alignment and all intermediate bounds are derived from empty entry. Deposit505 and Exit append consumers use that trace and the existing nested allocation506 bound. STOP, RETURN and REVERT have literal terminal handlers with distinct507 revert and out-of-gas outcomes. Source STOP advances PC; replay STOP does not,508 so no equality of those terminal PCs is claimed.509 510 The decoder supplies complete PUSH immediates from the same code/PC. Its finite511 byte-table proof is not an iteration limit. Paid running length is bounded by512 the same resource potential for arbitrary finite traces. Actual source dispatch513 (including invalid opcode versus EOF), frame initialization, owner lookup,514 outer rollback, complete occurrence identity and protocol histories remain515 open. Component builds and reciprocal independent reviews pass, together with516 [full frozen validation](receipts/direct-checked-runtime-build-20260910.json)517 and [exact-commit review](receipts/direct-checked-runtime-review-20260910.json).518 519 Source `823f37b` adds the [context-producer bundle](receipts/direct-context-producers-bundle-20260910.json):520 checked binary handlers, a transaction-derived potential bound at nested521 CALL/CREATE entries, and concrete paid-append consumers. Parent storage read522 equivalence preserves original/current values and exact actions/prices across523 pending block-write overlays. Ten component targets and reciprocal independent524 reviews pass, with 69 standard-or-less exports, together with [full frozen validation](receipts/direct-context-producers-build-20260910.json)525 and [independent exact-commit review](receipts/direct-context-producers-review-20260910.json).526 527 Retrieved Hermes sources now supply explicit SYSTEM dispatcher fields and the528 ordered pair, represented admission checks, and accepted-slot/withdrawal guards.529 The admission interface was corrected after independent review: the old blob530 tariff differs from Amsterdam, so old-consumer compatibility is separately531 required. It is not silently inferred from source admission. The new inherited532 withdrawal-stage producer derives both previous guard inputs. The cache producer533 starts at exact Gloas upgrade initialization and retains expected withdrawals534 on empty parents, counting every payload list without assuming each computed535 list is used at most once.536 537 [Adapter findings and the pending cryptographic proposal](receipts/direct-protocol-adapter-findings-20260910.md)538 record the exact remaining source/engine/canonical history bindings. Eleven539 complete CL files have been verified against the immutable Git tree. No fork,540 inhibition, upgrade or cryptographic proposal has been adopted automatically.541 The actual source occurrence coverage, full source handler/interpreter binding,542 canonical funded histories and final three-guarantee closure remain open.543 544 Source `7fe5e3d` adds the [source-completion bundle](receipts/direct-source-completion-bundle-20260910.json)545 reconstructs an entire finite protected execution from the same ordered546 source-shaped actions and prices. Memory capacity and host bounds are derived547 from those actions and cumulative costs. Entry starts with empty stack/memory;548 synthetic gas and fuel are constructed, preserving the call's world and context.549 STOP, RETURN and REVERT produce actual evaluator outcomes and exact terminal550 gas debits. REVERT's terminal storage/log observations remain internal.551 552 The same completed source event list now derives the mandatory append costs553 (1419 Exit, 2647 Deposit) and produces the existing paid append resource leaf.554 Old execution success, an old trace, per-step memory caps and an instruction555 count are no longer supplied to this leaf producer. Its work bound comes from556 the same literal paid resource run and the frame's initial execution potential.557 Seven component targets and independent component reviews pass, with 22558 standard-or-less exports, together with [full frozen validation](receipts/direct-source-completion-build-20260910.json)559 and [independent exact-commit review](receipts/direct-source-completion-review-20260910.json).560 561 Actual source execution/price/context extraction, the protocol-derived initial562 frame potential, source occurrence identity and all-survivor coverage, outer563 failure/rollback, canonical funding/deployment/block context and pending policy564 decisions remain open. The finite action history and its halt are still inputs565 from source extraction; unconditional source termination is not established here.566 567 Source `b7c927d` adds the [protected-replay bundle](receipts/direct-protected-replay-bundle-20260910.json)568 constructs an actually admitted pinned EVM step from the same successful569 source-shaped action. It covers every nonterminal instruction of both fixed570 runtimes, with stack, memory, storage, logs, environment and PC related. Stack571 underflow, DUP/SWAP depth, jump validity and static-mode guards are derived.572 The source-produced output stack bound remains explicit.573 574 Memory and opcode charges yield a conservative synthetic budget of 222 times575 the same source event's execution cost, plus a 2301 reserve for the SSTORE576 sentry. This budget is used for effect replay; actual source gas remains the577 resource ledger's measure. The proof handles the actual charge order and has578 no fee-loop iteration ceiling. All sixteen component targets and independent579 component reviews pass, together with [full frozen validation](receipts/direct-protected-replay-build-20260910.json)580 and [independent exact-commit review](receipts/direct-protected-replay-review-20260910.json).581 582 This closes local reverse effects and guarded single-step construction.583 Actual source instruction/price extraction, memory bounds from the source584 ledger, whole finite trace and terminal replay, source occurrence coverage,585 canonical funding/deployment/block context and policy decisions remain open.586 Unchecked actions alone do not justify stack admission; the injected stack587 counterexample is preserved and is not presented as a reachable contract bug.588 589 Source `f11f001` adds the [execution-work bundle](receipts/direct-execution-work-bundle-20260910.json), which590 derives mandatory append costs from the same actual completed user trace:591 Exit costs at least 1419 execution gas; Deposit at least 2647. The last store592 is counted after LOG0, so this is a completed-append bound, not a bound inferred593 from an arbitrary executed log. Actual entry and fee-loop inversion, ordered594 instruction markers, terminal trace uniqueness and source-priced prefix595 splitting remove the supplied structural-count premise.596 597 The finite recursive resource ledger tracks execution plus outstanding and598 committed state spill. State credits and rollback preserve this potential;599 exceptional forfeiture decreases it. CALL overhead subtracts its stipend once;600 CREATE's opcode overhead is paid separately. Selected actual completed leaf601 payments derive the transaction count bound from source allocation and calldata602 floor without requiring global nonnegative net state use. Eleven targets and603 43 standard-or-less axiom exports pass, with component reviews,604 [full frozen validation](receipts/direct-execution-work-build-20260910.json) and605 [independent exact-commit review](receipts/direct-execution-work-review-20260910.json).606 607 This selection is explicitly a subset. Resource threading does not prove608 source occurrence identity or coverage. Actual source frame/payment/journal609 extraction, inclusion of every retained append, same-transaction settlement,610 canonical deployment/funding/block context and policy decisions remain open.611 The complete pinned 49-file gas audit is archived; it establishes the source612 mutation inventory, not Python execution or canonical reachability.613 614 Source `d85afb0` adds the [CALL boundary bundle](receipts/direct-call-boundary-bundle-20260910.json), which615 constructs literal child gas grants after CALL precharges, keeps the value616 stipend explicit, and derives failed-child meter guards from its actual paid617 protected-runtime run. Parent incorporation and the failed new-account refund618 stay tied to that same split and child result. Executed LOG0 costs remain bounded619 by parent pool loss; cancelled logs are not treated as retained records.620 Actual source early checks, state predicates, caller/child journal extraction,621 other state-credit paths and recursive transaction/block composition remain622 open. Three targets, ten standard-or-less axiom exports and component reviews623 pass, together with [full frozen validation](receipts/direct-call-boundary-build-20260910.json)624 and [independent exact-commit review](receipts/direct-call-boundary-review-20260910.json).625 626 Source `949d49d` adds the [state accounting bundle](receipts/direct-state-accounting-bundle-20260910.json), which627 derives source state-gas credits from the same actual storage actions, first628 per slot and then across the full EVM address/key space using a symbolic finite629 sum. Successful literal meter payments telescope to exact execution costs and630 state-potential change. The same actual receipt retains all three guarantees631 and a bound on executed LOG0 costs, with the initial credit potential retained632 for nested frames. These logs are not identified with retained queue records.633 Full-meter rollback preserves earlier committed charges, cancels this frame's634 state balance at its baseline and leaves executed work paid. Actual source635 child/outer journal pairing, grants, final refunds/block accounting and canonical636 protocol context remain open. Nine component targets, 28 standard-or-less637 axiom exports and component reviews pass, together with638 [full frozen validation](receipts/direct-state-accounting-build-20260910.json) and639 [independent exact-commit review](receipts/direct-state-accounting-review-20260910.json).640 641 Source `e9be8e9` adds the [source admission bundle](receipts/direct-source-admission-bundle-20260910.json)642 uses Amsterdam's own calldata floor to derive the size premise of the actual643 transaction-history consumer. It does not infer the different pinned intrinsic644 admission gate; the [divergence dossier](receipts/direct-reference-divergences-20260910.md)645 records an unsigned local counterexample to that floor-only implication.646 Source allocation and ordered reservoir-first spill now pay the same actual647 runtime event list through STOP/RETURN/REVERT under sufficient cap/total-gas648 inequalities. The same full receipt retains all three guarantee observations.649 These quantified allocations are not yet bound to actual transaction or child650 call grants. Settlement arithmetic is proved with explicit frame-input guards;651 canonical admission, returned pools/refunds, source execution and block-history652 extraction remain open. Eight component targets and 19 standard-or-less axiom653 exports pass, together with [frozen full validation](receipts/direct-source-admission-build-20260910.json)654 and [independent exact-commit review](receipts/direct-source-admission-review-20260910.json).655 656 Source `e79530b` adds the [admission and ordered SYSTEM bundle](receipts/direct-admission-system-bundle-20260910.json)657 derives root calldata fit from actual intrinsic-gas admission and connects it658 to the existing transaction-history and committed-effect consumers. It also659 constructs empty Deposit then Exit SYSTEM calls in the same actual history.660 Both entry invariants and the work/funding bounds come from the two real factory661 deployments and the linked history/ledger/block inputs. Each call retains its662 three guarantee observations. Canonical validation/dispatch extraction and663 acceptance of this schedule remain open. Four targets, nine standard-axiom664 exports and component reviews pass, along with665 [full frozen validation](receipts/direct-admission-system-build-20260910.json) and666 [independent exact-commit review](receipts/direct-admission-system-review-20260910.json).667 668 Source `e720558` adds the [runtime resource bundle](receipts/direct-runtime-resource-bundle-20260910.json)669 adds closed source readings and COPY/LOG0 prices to the same actual user or670 SYSTEM trace. Its complete success/REVERT certificates include terminal payment,671 with memory charged once across the trace and a state reserve based on executed672 SSTORE occurrences. All three guarantees consume the same receipt together673 with these certificates. The resource statement is deliberately conditional:674 its sufficient initial grants still need a protocol producer. It does not675 assert admitted user progress or source exceptional replay. Six targets and676 21 standard-axiom exports pass with component reviews,677 [isolated full validation](receipts/direct-runtime-resource-build-20260910.json), and678 [independent exact-commit review](receipts/direct-runtime-resource-review-20260910.json).679 680 Source `f17ab237` adds the [runtime receipt bundle](receipts/direct-runtime-receipt-bundle-20260910.json)681 now derives source-shaped actions for every actual completed user or SYSTEM682 execution, including LOG0, COPY, STOP, RETURN and REVERT. Memory capacities683 follow from an invariant on gas plus memory cost and an explicit initial684 resource/host threshold. The same actual Theta receipt feeds all three685 registered guarantee predicates and these runtime observations. Successful686 terminal owner preservation discharges the empty-world fallback; failed calls687 restore the whole pre-transfer journal and distinguish REVERT from exceptional688 failure. No post-state capacity, global write permission, or 256-iteration cap689 is assumed. The twelve component targets and reviews pass, as do the690 [isolated full check](receipts/direct-runtime-receipt-build-20260910.json) and691 [independent exact-commit review](receipts/direct-runtime-receipt-review-20260910.json). Initial source bindings, source user and692 outer-frame payment, canonical history extraction and protocol choices remain693 open; this bundle does not establish executable reference-interpreter parity.694 695 Source `90f02e9` adds the [source-reading payment bundle](receipts/direct-source-payment-bundle-20260910.json)696 removes the arbitrary storage-reading function from both SYSTEM constructors.697 Each actual priced edge now carries its evolving source view, independent698 warm-access set, source original/current/new values, and exact memory-cost699 difference. The same event list pays through RETURN and retains post-RETURN700 warmth, output and the three actual receipt guarantees. The initial source701 storage/access/context binding and historical invariant remain explicit inputs;702 executable reference interpretation is still open. CALLDATACOPY also has a703 complete local effect adapter at arbitrary source offsets, including zero704 length; user-path resources and full instruction/rollback composition remain.705 All eight targets, 24 standard-axiom exports and component reviews pass, as do706 [isolated full validation](receipts/direct-source-payment-build-20260910.json) and707 [independent exact-commit review](receipts/direct-source-payment-review-20260910.json).708 Exact lock-selected numeric sources show gas is nonnegative unbounded Uint,709 so a fixed-width gas upper-bound obligation would be spurious. U256 operand710 checks, nonnegative meter subtraction and initial source typing remain distinct.711 712 Source `2f0c142` adds the [SYSTEM view composition bundle](receipts/direct-system-views-bundle-20260910.json)713 constructs every source-shaped instruction action along the actual SYSTEM714 trace, including RETURN and its extended-memory output slice. Accepted stack715 operands, fixed-image decoder agreement, natural PC bounds, intermediate owner716 and memory-capacity facts are derived from that execution. Deposit and Exit717 entry constructors produce one witness carrying both these views and the718 sequential source-meter payment. Its exact full Xi endpoint and Theta commit719 then feed all three guarantee parents and SYSTEM invariant preservation in720 `ReferenceSystemGuarantees.system`. No independent receipt is supplied.721 All 19 targets, 61 new standard-axiom Trust exports, component reviews,722 [isolated full validation](receipts/direct-system-views-build-20260910.json) and723 [independent exact-commit review](receipts/direct-system-views-review-20260910.json)724 pass. Initial storage/context bindings and725 the historical invariant remain inputs to this adapter. Arbitrary storage-gas726 readings are not yet coupled to the source views, and a source-shaped Lean727 action is not an executable reference-interpreter trace. Canonical deployment,728 admission, scheduling, fork and inhibition decisions remain open. The linked729 producer inventory records these dependencies; the structured ledger remains730 the only roadmap.731 732 Source `64eddfb` adds the [SYSTEM resource bundle](receipts/direct-system-resources-bundle-20260910.json)733 with sixteen modules and 100 Trust exports. Its [isolated full validation](receipts/direct-system-resources-build-20260910.json)734 and [independent exact-commit review](receipts/direct-system-resources-review-20260910.json)735 passed, including all 100 Trust exports and existing kill lines. Both736 actual SYSTEM executions now retain their complete trace, terminal RETURN,737 operation count, at most four SSTOREs and intermediate memory bounds. Word-fit738 for memory expansion is derived from operand types, without a no-wrap premise.739 The source memory-cost sum is constructed from those same actual states for an740 arbitrary finite trace, including the terminal operation. Sequential source-meter741 payment is then derived from initial resources, with every sentry and payment742 condition proved and no reliance on future refunds. Under the proposed 30M743 execution/16*97920 reservoir grant, conservative execution envelopes are744 17,902,012 for Deposit and 1,730,623 for Exit, with 391,680 state gas each.745 746 `SystemMeterResources.deposit/exit` retain the same actual successful evaluator747 result and priced events. They do not establish execution by the proposed748 reference interpreter: its instruction/state/checked-type adapter, mandatory749 SYSTEM scheduling and canonical history remain open. Local control/stack,750 arbitrary-offset CALLDATALOAD and charged memory-operation adapters also gained751 proofs. The [producer inventory](receipts/direct-system-resources-bundle-20260910.json)752 identifies each consumer, dependency and owner; the structured task ledger753 remains the sole roadmap. No protocol variant or inhibition policy is adopted.754 755 The preceding frozen source `8173c79` passed isolated `make check` and independent exact-commit review. Supporting756 results now include universal remaining-gas bounds, recursive and whole-Υ757 funding conservation under independent admission, linked funding histories,758 all-outcome local event extraction, actual recursive error adapters, structural759 occurrence uniqueness and child-charge transport through steps and wrappers.760 761 Source `8173c79` adds ten modules and 52 Trust exports for reference operation762 transport. Full account entry lookup, apparent/actual value and synthetic-log763 guards, source-shaped storage layers and SSTORE charging, and five-image764 PUSH/jump decoding are checked. Actual sparse memory writes compose with eager765 reference slice replacement, deriving post-memory coherence, rounded capacity766 and RETURN bytes. [Full validation](receipts/direct-reference-operations-build-20260910.json)767 and [exact-commit review](receipts/direct-reference-operations-review-20260910.json)768 passed. The [producer inventory](receipts/direct-reference-operations-bundle-20260910.json)769 keeps source interpretation, full reference traces, bounds, gas accounting and770 canonical protocol inputs open. The [divergence analysis](receipts/direct-reference-divergences-20260910.md)771 records truncated-PUSH foreign-code mismatch, sparse memory and refund/state772 boundaries. The tighter physical-store capacities give costs 1372/107; the new complete773 trace producer conservatively uses 400/40 words and costs 1512/123. Reference774 execution transport remains required. This is not Ethereum context closure.775 776 Source `7f55526` derives both initial invariants from two linked actual factory777 transactions. Exact salt/initializer copying, selected-child fuel, CREATE2 gas778 settlement, constructor code deposit, the factory return, Θ value transfer and779 Υ finalization are composed on the same worlds. The second deployment preserves780 the first contract’s code/storage/control invariant. `FactoryHistoryGuarantees.from_genesis_both`781 uses this committed seed for all three guarantees and the same retained queue/log782 effects at every later receipt position; it does not assume an initialized seed.783 The literal genesis/credit ledger derives the numerical funds bound. All 18784 modules and 74 Trust exports passed [full validation](receipts/direct-factory-history-build-20260910.json)785 and [exact-commit review](receipts/direct-factory-history-review-20260910.json).786 [Finite factory regressions](receipts/direct-factory-deployment-regressions-20260910.json)787 cover both deployments, admissible prefunding, collision retries and gas-failure788 rollback, with complete traces and explicitly injected Prague setup.789 790 The remaining protocol inputs are explicit in the791 [producer inventory](receipts/direct-factory-history-bundle-20260910.json): canonical792 factory installation and deployment admission/hash/collision state; the actual793 prior genesis-to-deployment funding trace; canonical credit-ledger/count and794 block/slot extraction; reference EVM opcode/rollback/gas and mandatory SYSTEM795 scheduling/resources; and Thomas’s fork, inhibition and upgrade decisions.796 The 30M pinned SYSTEM counterpart and synthetic SYSTEM-emitter log projection797 are proved, but do not establish the reference dispatcher’s dual-pool liveness.798 These conditional results do not close or adopt an Ethereum protocol context.799 800 Source `d71706d` composes journal preservation over the complete actual recursive801 evaluator, including failed wrappers and ancestor rollback. Every nested call's802 input invariant is derived from the initial journal and real preceding steps;803 its three local observations bind to the same actual receipt. A constructive804 `5 * (request.gas + 1)` evaluator-fuel bound discharges all-node fuel exhaustion,805 including caught creation children. This is separate from EVM gas success and806 reference Ethereum semantic transport. All ten modules passed807 [isolated full validation](receipts/direct-recursive-journal-build-20260910.json)808 and [independent exact-commit review](receipts/direct-recursive-journal-review-20260910.json).809 Actual transaction settlement, initialized linked histories, external-credit810 provenance, committed-record/log survival and protocol obligations remain open.811 812 Source `40b6095` adds actual Υ checkpoint/provisional/settlement composition,813 including failed status, refunds and cleanup. A linked history of the same814 transaction receipts, either canonical SYSTEM runtime and literal credits815 derives intermediate invariants and funding from one seed. The exact ordered816 receipt list feeds the admitted block work envelope. Chosen physical queues817 are unique and actual local append couples the queue extension to authentic818 LOG0; a false-status call restores its checkpoint. These five modules passed819 [isolated full validation](receipts/direct-actual-history-build-20260910.json)820 and [independent exact-commit review](receipts/direct-actual-history-review-20260910.json).821 Seed deployment/funding, protocol extraction, external-credit provenance and822 bounds, plus occurrence identity and survival through ancestor rollback remain823 required consumers. Local queue uniqueness does not identify equal-byte submissions.824 825 Source `7cc3d0a` derives the actual prehistory at every transaction list826 position, then uses its seed-derived funding/invariant for all three nested827 observations. Protected-address log frames preserve all topics/payloads and828 actual order through ordinary other-owner instructions and Υ finalization.829 A literal credit ledger supplies a symbolic funding envelope; the numerical830 specialization remains conditional on protocol-derived PoW/withdrawal counts,831 migration coverage and genesis correspondence. All three modules passed832 [isolated full validation](receipts/direct-history-observations-build-20260910.json)833 and [independent exact-commit review](receipts/direct-history-observations-review-20260910.json).834 These results do not yet prove complete committed occurrence/log survival or835 reference protocol/deployment coverage.836 837 Source `baf38a4` ties actual transaction/history queue replay to extracted838 protected-call world paths and proves record-source provenance. It separately839 specifies a unique ordered list of calls surviving the literal wrapper guards;840 the exact list-to-path bridge and final log equation are the next consumers.841 Literal conserving transfers now enter the funding and execution histories,842 and sequential full-balance sweeps derive their receiver arithmetic bound.843 A source-verified minimum-difficulty/terminal-parent calculation supplies the844 PoW count arithmetic, with canonical-chain and reward linkage still explicit.845 All supporting targets passed [isolated full validation](receipts/direct-queue-provenance-build-20260910.json)846 and [independent exact-commit review](receipts/direct-queue-provenance-review-20260910.json).847 The three [nested rollback regressions](receipts/direct-nested-rollback-regressions-20260910.json)848 separate executed append work from committed records/logs, including a caught849 inner out-of-gas. They use an injected Prague state, not protocol reachability.850 851 Source `22a886b` closes the pinned-evaluator composition of actual surviving852 call IDs, final queue replay and final protected-emitter logs. The same canonical853 list has no duplicate invocation IDs; the final log count equals the surviving854 successful nonempty non-SYSTEM submission count, bounded by actual executed855 marked work and reported transaction gas. It is not the final queue length.856 `HistoryCommittedGuarantees.composed` derives the physical prequeue from the857 actual initialized prefix and combines these committed effects with all three858 local observations at every transaction position, including nested calls later859 rolled back. Its genesis-ledger specialization discharges the numeric initial860 funding bound using the complete constructed genesis world. Literal withdrawal861 dispatch counts every list item, including Gloas builders, and typed accepted862 payload lists at distinct beacon slots derive the withdrawal count bound.863 All eleven modules passed [isolated full validation](receipts/direct-committed-effects-build-20260910.json)864 and [independent exact-commit review](receipts/direct-committed-effects-review-20260910.json).865 866 This is still conditional Ethereum coverage. The [transitive producer inventory](receipts/direct-committed-effects-bundle-20260910.json)867 keeps exact factory/deployment/parent-commit initialization, canonical genesis868 and credit classification/chronology, reference semantics and resource pools,869 transaction admission, block/slot and SYSTEM dispatch/progress, inhibition and870 upgrades open. The supplied ledger matches genesis, final world and credit871 total; step-by-step correspondence with the actual reference history is a872 separate obligation. No protocol variant has been silently accepted.873 874 The new modules derive full nested-event extraction, tree uniqueness875 and aggregate gas for every finite evaluator fuel and every outcome. Descendants876 remain counted after errors or ancestor rollback. A successful audited append877 is tied to a local event in the same certificate. The actual Υ child selection878 and capped refund now derive `tree.count ≤ usedGas` without a supplied aggregate879 charge. Exact initializer success is also derived with code-deposit resources.880 All additions passed frozen full validation, including the existing mutation881 targets; the [build receipt](receipts/direct-nested-event-composition-build-20260909.json)882 records exact sources and dependencies. This is modular evidence, not closure883 of the three guarantees over protocol histories.884 885 Sources `39b3e02` and `413176a` add the complete set of actual locally successful append886 frames. `XiAt.identity` proves that each structural path denotes unique full887 inputs and result; `NestedAppendCount.mem_frames_iff` proves the finite set888 omits no qualifying invocation. Its count is bounded by actual Υ reported gas,889 including reverted descendants. All nine new modules passed isolated full validation and independent source890 reviews; the [build receipt](receipts/direct-append-history-bridge-build-20260910.json)891 and [exact-commit review](receipts/direct-append-history-bridge-review-20260910.json)892 identify the validated sources. Runtime893 clones and delegated execution of the pinned bytes are conservatively included.894 The opcode tables and actual dynamic execution scope now prove that both895 runtimes have no child invocations. Ordinary instructions executed at another896 owner preserve existing protected account code/storage, including SELFDESTRUCT897 with that account as beneficiary. Nested subtree counts and actual transaction898 receipts feed the typed block budget; protocol gas admission remains explicit.899 A kernel-certified CREATE/zero-evaluation-fuel prefix erases the temporary world900 and ultimately errors. This diagnoses a proof-evaluator boundary, not a901 successful Ethereum transaction or a security exploit.902 903 Source `b341047` additionally derives funding ceilings at every actual nested904 Theta transfer from the linked funding history, including reverted ancestors.905 Typed CREATE encoding is total; Lambda errors are classified as evaluator906 OutOfFuel. Exact creation/message/ordinary/finalization code and storage frames907 compose with the protected call's queue/control invariant on the same receipt.908 The full pinned genesis input has 8893 allocations whose sum and constructed909 account-map bound are kernel checked. These 16 modules and their Trust exports910 passed [full validation](receipts/direct-funding-journal-build-20260910.json)911 and [independent exact-commit review](receipts/direct-funding-journal-review-20260910.json).912 The genesis input is not yet bound to the reference loader or admitted protocol913 history. The legacy initializer consumer exposes target absence; the newer914 prefunding-compatible producer is now connected to the journal invariant. Complete call-owner/code915 coherence, selfdestruct exclusion and adequate evaluator fuel remain open.916 917 Source `bd62a07` composes all three local runtime observations on the same918 actual protected Theta receipt. Its public queue/control domains are derived919 from one journal invariant; the actual selected code and value are bound to920 that receipt. Chronological executed-event intervals and the append weight921 use the same nested certificate. Prefunded initialization, nested calldata922 width, recursive step world/set projections, and runtime/precompile deletion923 frames are now connected consumers. Ten modules passed [full validation](receipts/direct-protected-journal-build-20260910.json)924 and [exact independent review](receipts/direct-protected-journal-review-20260910.json).925 This establishes the atomic step needed by the global journal induction. It926 still consumes the input invariant and does not establish protocol history927 reachability or sufficient SYSTEM resources. The runtime control component is928 not misrepresented as the full initialization-and-progress PControl conjunction.929 930 The next missing composition is **committed storage and intermediate journals**.931 Locally successful appends are a work metric, not a persistent-record count.932 Valid protocol-history extraction, external credit provenance, every933 intermediate domain, deployment, block accounting and scheduling remain to justify. Final normative version/inhibition remains an934 explicit report decision. No intermediate supporting result closes these935 obligations by itself. The sections below retain the evidence chronology.936 937 The resumed closure review expands the public transitive premises into 46938 explicit obligations, attached to the four existing structured tasks (5 fee,939 11 queue/event, 27 protocol/initialization, 3 global-composition obligations).940 The [premise inventory](receipts/direct-public-premises-20260909.json) and941 [task-write receipt](receipts/direct-premises-roadmap-20260909.json) are review942 snapshots, not another roadmap or acceptance of those obligations.943 Seven additional reference-interpreter adequacy obligations are attached to944 the existing protocol task in the [structured progress receipt](receipts/direct-structured-progress-20260910.json).945 The [semantic inventory](receipts/direct-semantics-adequacy-20260910.md) and946 [focused adapter proposal](receipts/direct-runtime-adapter-interface-20260910.md)947 identify dual gas pools, transaction type 4, transfer LOG3, code protection and948 sufficient evaluator fuel as concrete remaining bindings. They do not claim949 that the pinned evaluator already implements the proposed Amsterdam reference.950 The [current-version review](receipts/direct-protocol-current-20260909.md)951 checks byte identity, deployment preimages and report provenance; its proposed952 protocol choices and authors draft remain unadopted and unsent. In particular,953 canonical deployment still needs the actual factory transaction and ancestor954 commit, beyond the new local initialization-success theorem, and the runtime domain must be derived955 at nested intermediate states as well as committed transaction boundaries.956 957 ## Target and acceptance958 959 The initial implementation base is `f14791d482690c64b71c17f63024d78459d15939`.960 Bytecode, EIP and EVMYulLean pins remain those in `artifacts.lock.json` and961 `lake-manifest.json`. Current EIP wording must not silently change this target.962 963 The live objective is a theorem about each complete pinned EVM call and its964 committed effects. Global equality with the old natural-number Model is no965 longer a prerequisite. That historical target is not proved, and the arithmetic966 counterexamples remain valid; changing the objective does not close it.967 968 The agreed mathematical excess and fee clauses remain obligations on a969 justified domain. Additional monotonicity and super-linear-growth properties970 are separate findings, not additional conditions for closing the three IDs.971 Word-exact semantics alone does not establish the agreed mathematical clauses.972 973 An intermediate dossier is not completion. No existing public parent is974 reclassified solely because a new definition, helper or local theorem builds.975 976 ## Architecture977 978 * **Execution:** reuse EntryReach/SymExec and pinned EVMYulLean. Do not build979   another interpreter. Keep exact memory, storage, logs and failure behavior.980 * **Small specifications:** FIFO as a list, independent record encoding,981   precise word control operations and an untruncated natural fee recurrence.982 * **Arithmetic:** separate successful completion, word fit and EVM gas. No983   256-iteration constant in the new fee semantics. No arbitrary no-wrap or984   funding bound presented as a derived protocol invariant.985 * **Message calls:** `Ξ` begins after value transfer. `Θ` performs transfer and986   settlement. REVERT/exception restores the pre-call world and substate;987   interpreter OutOfFuel propagates. This does not refund transaction fees.988 * **Histories:** bind both worlds to actual `Θ` results. A history parameterised989   by an initial world is not yet evidence about the exact constructor or about990   valid Ethereum blocks.991 992 ## Implementation evidence and limits993 994 All names in this section identify source obligations; compilation and review995 receipts are required before accepting the corresponding evidence.996 997 | Module | Result to validate | What it does not establish |998 |---|---|---|999 | `EntryReach/FeeQuote` | Completed word quote, stability and uniqueness for arbitrary finite budgets; candidate originated at `ee7c3f869052bf52259b59d664422631f67949ea` | Success of an EVM call, sufficient gas, or the natural tariff |1000 | `EntryReach/FeeQuotePath` | Completed quote to the actual deposit fee-loop exit at PC 127; source `34c319eb9890d1bf56221df4310c14b52b21be8d` | Full getter result or successful-call inversion |1001 | `Integrator/MathFee` | Natural recurrence terminates for every numerator and defines a unique price; arbitrary finite-prefix correspondence under explicit intermediate bounds | Word-loop termination or that arithmetic bounds hold on protocol histories |1002 | `Integrator/ControlSpec` | Word control operations, relation to entry operands and bounded natural formulas | Committed control state for a whole call |1003 | `Integrator/EndpointState` | Whole `Ξ` success payload from execution witnesses; getter account-map/log preservation | Inversion of every possible successful call, append/drain content postconditions, or `Θ` settlement |1004 | `Integrator/AppendSpec` | Independent deposit receipt authenticity, anonymous-log cardinality, other-account preservation | Authentic queue storage or exit address/pubkey byte identification |1005 | `Integrator/MessageCall` | Actual `Θ` settlement, including rollback, value-transfer order and OutOfFuel propagation | Authorization, sufficient funds, transaction gas accounting or a predeploy path |1006 | `Integrator/ReachableCalls` | Calls link actual pre/post worlds; failed calls cannot select a new world; OutOfFuel cannot extend the history | Exact initialization, protocol reachability, slot integrity or economic bounds |1007 | `Integrator/CallBridge` | Pinned code frame uses actual transferred world and correct Θ/Ξ/X fuel offsets; endpoint settlement | A new execution-path or independent storage specification |1008 | `Integrator/RejectionSpec` | Inhibited paths compose with actual Θ rollback, under explicit resources | A complete arbitrary-gas rejection partition |1009 | `Integrator/SystemSpec` | Actual successful Ξ world satisfies independent excess/count/head/tail formulas; every record slot ≥4 preserved; owner remains present | Natural queue length on malformed pointers, FIFO bytes, or a derived protocol invariant |1010 | `Integrator/WorldNonempty` | An existing account disproves the actual empty-world BEq test without a LawfulBEq Account assumption | Owner existence without an execution/initial-state proof |1011 | `Integrator/CommittedSystem` | SYSTEM storage specification and actual return bytes committed by Θ; derives absence of empty-world fallback | FIFO byte identification, actual gas scheduling, or justified protocol histories |1012 1013 ### Further direct evidence (continuation, 9 September)1014 1015 The following additional sources passed standalone Lean compilation and the1016 full `make check` at `5e9f63f`; the exact source bindings and independent reviews1017 are recorded in `direct-continuation-build-20260909.json` and1018 `direct-continuation-reviews-20260909.md`. The older build receipt does not cover1019 these additions. Subsequent components listed below require their own receipt.1020 1021 * `EntryReach/FeeQuoteGetter`, cherry-picked from remote `d191d4f` as1022   `0ccf3d3`, carries a completed deposit quote through its getter endpoint with1023   explicit remaining gas and fuel. The pinned main branch remains `f14791d`.1024 * `Integrator/GetterCall` proves both actual Θ getters return the exact quoted1025   32-byte word, preserving all account lookups, logs and created accounts.1026   It proves zero-value transfer neutrality and handles both empty-world1027   settlement branches. Quote completion and sufficient resources remain premises.1028 * `Integrator/AppendStorage` proves both actual Ξ append outcomes have the1029   independent calldata/caller record words, count and tail increments, unchanged1030   head/excess and preservation outside the write set. Record-window and counter1031   bounds are explicit assumptions, not established protocol invariants.1032 * `Integrator/ExitRecord` identifies the actual exit LOG0 payload as the1033   immediate caller's twenty bytes followed by exactly forty-eight calldata bytes.1034 * `Integrator/ExitDrain` proves every iteration of the actual exit memory writer,1035   then composes with Θ: returned bytes are exactly the independent concatenation1036   of the oldest capped, word-indexed records. It accounts for the overlapping1037   MSTORE writes and excludes the final sixteen-byte overhang. The 160-bit width1038   of stored source addresses is a premise; ordinary queue arithmetic and its1039   preservation from initialization still require proof.1040 1041 Further components passed `make check` at `8b9e562`; source hashes and reviews1042 are in `direct-data-build-20260909.json` and `direct-data-reviews-20260909.md`:1043 1044 * `CommittedAppend` joins storage and receipt witnesses by equality of the1045   actual Ξ result, then commits both in one Θ result. Owner existence excludes1046   the empty-world fallback. Other accounts are compared to the transferred1047   entry world, so balance transfer is not silently erased.1048 * `SubmissionCall` binds apparent CALLVALUE to actual transferred value and1049   replaces payment word comparisons with fee-plus-stake inequalities over1050   naturals. The actual uint64 amount extraction proves the stake product cannot1051   wrap; it is not an assumed arithmetic bound. Quote completion and local1052   storage-window bounds remain premises.1053 * `QueueArithmetic` proves the cap is `min(TAIL-HEAD,64/16)` in naturals and1054   commits full reset/partial advance with all stale slots unchanged, assuming1055   entry `HEAD≤TAIL`. It does not assume post-pointer equations.1056 * `DepositDrain` identifies the entire actual Θ return as the word-indexed FIFO,1057   including exact reversal of amount bytes 80–87 and exclusion of the final1058   eight-byte memory overhang. No record-encoding agreement is assumed.1059 * `RejectionCases` exhausts every invalid input branch after a completed quote1060   and proves actual Θ rollback of the pre-transfer world and log journal.1061   Its word-level input predicate and sufficient resource bounds remain visible.1062 1063 Additional results passed isolated `make check` at `018cd2d`; exact source1064 hashes and reviews are in `direct-inversion-build-20260909.json` and1065 `direct-inversion-reviews-20260909.md`:1066 1067 * `SuccessInversion` derives actual steps, exact fee-loop cycles and quote1068   completion from a successful user Ξ call, at arbitrary gas and fuel. Inhibition1069   is ruled out by inverting the actual REVERT branch. `CallSuccess` and1070   `SuccessfulQuote` lift this necessity to actual Θ success and derive positive1071   evaluator fuel. No completed-quote premise or fixed iteration cutoff remains1072   in these necessity theorems. The further admission/return results below1073   extend this evidence.1074 * `Initialization` executes both pinned init byte strings universally, returns1075   their exact runtimes, and proves their storage effects. Initial control values1076   follow from explicit zero-control inputs. CREATE/code installation and1077   protocol activation are not established by returned bytes alone.1078 * `QueueInvariant` supplies the small FIFO abstraction: append extends the list,1079   drain returns its capped prefix and retains its suffix, tied to actual Θ1080   results. Source-width preservation for exits follows from the caller's1081   inherent address width and list append/drop. Local capacity bounds remain1082   explicit; initialized protocol-history preservation remains open.1083 * `ResourceBounds` proves the finite-slot/gas arithmetic implication to fewer1084   than 2^128 appends and hence capacity/control fit given an explicit accounting1085   bridge. Actual gas/refund accounting and actual-state bounds are not assumed1086   proved. See `PROTOCOL-BOUNDARY.md` for immutable references and open bindings.1087 * `Tests/DirectMutations` reuses six existing finite mutant receipts to refute1088   the very same direct storage/log predicates. It adds no native evaluation and1089   has no impossible mutant-code pin premise. Its dependencies retain exactly1090   the disclosed legacy native receipt axioms; the new universal proofs do not.1091 1092 Further sources passed isolated `make check` at `f52112e`; exact bindings are1093 in `direct-admission-build-20260909.json` and independent source reviews in1094 `direct-admission-reviews-20260909.md`:1095 1096 * `CreationSettlement` unfolds actual Lambda creation settlement, retaining1097   address encoding, collision behavior, all code-deposit checks and remaining1098   gas. Both pinned constructors are connected to installed runtime/storage in1099   an actual successful creation. Canonical deployment identity, transaction1100   validity and sufficient resources for creation remain separate obligations.1101 * `TransferFrame` proves that actual Θ credit/debit preserves every storage read1102   and code observation, including self-calls and initially missing accounts. An1103   existing pre-call owner survives transfer; unchanged balances are not claimed.1104 * `AdmissionInversion` and `SuccessfulUser` derive inhibition exclusion, a1105   completed operational quote, and the exact getter/submission input partition1106   from actual success at arbitrary gas/fuel. Natural calldata lengths require1107   the explicit size bound `<2^256`; ordinary calls bind apparent to actual value.1108   The actual getter output is the same quoted price, encoded in 32 bytes.1109 * `GetterInversion` derives zero value and preservation of every pre-call account1110   lookup, logs and created accounts from actual successful empty-calldata user Θ1111   calls. Neither quote completion nor sufficient gas is a premise.1112 * `UniversalGate` proves every completed inhibited user Θ call has failure flag1113   and restores the entire pre-call world, substate and created-account journal.1114   Evaluator OutOfFuel remains an error, not a completed call result.1115 * `FeeSafeDomain` universally proves word/natural agreement for every numerator1116   ≤2892. A kernel-checked trajectory at the upper bound plus monotonicity proves1117   all intermediate products fit and all smaller trajectories complete. The 4621118   steps are a certificate witness, not a cutoff in the fee definition. Any1119   completed word budget yields the same mathematical tariff.1120 * `SuccessfulUser.*_getter_math` binds that tariff to actual Θ return bytes using1121   the independent PRE-CALL natural numerator `excess+max(0,count-TARGET)≤2892`.1122   This bound remains external until initialized protocol/funding preservation1123   is established.1124 * `FeeBoundary` proves the untruncated word and natural fees differ at numerator1125   2893, and the word fee decreases relative to 2892. These are exact terminating1126   computations plus uniqueness, not observations at an arbitrary cutoff. It1127   does not prove that a funded protocol history reaches that numerator.1128 1129 Further sources passed isolated `make check` at `cc78419`; exact source1130 bindings are in `direct-append-build-20260909.json`, and reviews in1131 `direct-append-reviews-20260909.md`:1132 1133 * `AppendInversion` follows every actual SSTORE/memory/LOG0/STOP step in both1134   successful append suffixes. It derives the concrete state and empty return1135   from actual successful user Ξ execution, without resource/completion premises.1136 * `SuccessfulAppend` transports the independent storage and authentic single1137   receipt to the same actual Θ result. Its paid variants also derive the same1138   completed operational quote and natural payment checks. Owner existence and1139   local record/counter fit remain explicit; gas, permission and fee completion1140   are derived from success rather than assumed.1141 * `UniversalRejection` proves arbitrary-resource failure plus whole-journal1142   rollback for malformed lengths, paid getters, the deposit amount floor and1143   underpayment. A known-price underpayment witness may use any completed word1144   quote of the pre-transfer input; uniqueness identifies the executed price.1145 * `AccountedState` maintains HEAD≤TAIL≤budget, count≤budget and, when enabled,1146   excess+count≤budget across the independently proved append/SYSTEM slot maps.1147   It derives AppendFits from an independent budget<2^128 BEFORE using the1148   append postcondition. Monotone budgets can cover restored older journals;1149   actual event extraction and gas accounting remain open.1150 * `FundedDomain` proves the safe numerator ≤2892 is preserved by paid appends1151   below an explicit funding ceiling (the fee at 2892), and by all SYSTEM1152   latch/unlock/fold cases. It composes with the existing sufficient-resource1153   Θ results. Neither the ceiling nor initialized-history preservation is1154   asserted to be a derived protocol fact.1155 1156 One-step user invariant modules passed isolated `make check` at `f1e2c57`;1157 exact bindings and reviews are in `direct-user-invariants-build-20260909.json`1158 and `direct-user-invariants-reviews-20260909.md`:1159 1160 * `UserStateInvariant` handles every actual completed ordinary user Θ result.1161   Failure/getter preserves bounds; successful nonempty input contributes exactly1162   one event and preserves the structural budget and funded safe fee domain.1163   AppendFits is derived from the pre-call budget before using the actual receipt.1164   No sufficient resources, quote completion or post-state agreement is assumed.1165 * `UserQueueInvariant` proves the actual user post-world represents either the1166   same list or that list extended by exactly the authentic input record. The1167   choice depends only on actual success and calldata emptiness. Thus the prior1168   FIFO is a prefix of the resulting FIFO, and exit source width is preserved.1169   This needs the independent structural budget, without any fee-domain or1170   funding ceiling premise.1171 1172 The next modules passed isolated `make check` at `ebfe8af`; source bindings1173 and reviews are in `direct-system-inversion-build-20260909.json` and1174 `direct-system-inversion-reviews-20260909.md`:1175 1176 * `InitializedInvariant` derives installed runtime, Bounded0, EnabledSafe and1177   an empty represented FIFO from actual successful Lambda creation at an1178   independently absent target. Deposit starts enabled; exit starts inhibited.1179   Canonical deployment identity and transaction validity remain separate.1180 * `SystemInversion` derives both entire SYSTEM Ξ outcomes from actual success,1181   including capped loops, memory, full/partial pointers, latch/unlock/fold and1182   both final stores/RETURN. No gas/fuel/permission premise is needed. The1183   independent all-slot specification additionally requires an input owner.1184 * `ActualAppendGas` extracts real memory/opcode debits from accepted Z/step,1185   proves the actual LOG0 charges (919 exit; 1847 deposit), and telescopes real1186   supported traces through the gas returned by Θ. The whole-call debit theorem1187   requires an actual `LogPath` witness, discharged by `AppendGasPath` below.1188   It does not assume a desired final gas value.1189 1190 The following complete-call/history modules passed isolated `make check` at1191 `586bb1c`; source bindings and reviews are in `direct-history-build-20260909.json`1192 and `direct-history-reviews-20260909.md`:1193 1194 * `SuccessfulSystem` transports both arbitrary-resource SYSTEM success results1195   to actual Θ storage and output, deriving owner survival/nonempty settlement.1196 * `SystemStateInvariant` covers actual completed SYSTEM results: success returns1197   exactly the capped FIFO prefix and keeps its suffix; failure preserves the1198   queue and makes no return-byte claim. Structural budget and enabled fee safety1199   are preserved in both cases, with exit source width retained. Scalar-only1200   wrappers need no logical queue witness.1201 * `ConcreteHistory` links real full pre/post worlds through actual Θ transitions1202   and counts events from success, caller and input. Its policy contains only1203   calldata-size and user-funding constraints. An independent total-event bound1204   supplies all prefix bounds; no invariant or AppendFits is a history-constructor1205   premise. Actual successful creation supplies the initial invariant, with1206   canonical address equality explicit. The conclusion preserves budget, fee1207   safety and an existential represented FIFO (including exit source width).1208   It does not extract arbitrary transactions/ancestor rollbacks, connect gas1209   totals, or impose inter-call header/originalWorld/substate coherence.1210 1211 The following gas modules passed isolated `make check` at `749a1c0`; exact1212 bindings and reviews are in `direct-gas-build-20260909.json` and1213 `direct-gas-reviews-20260909.md`:1214 1215 * `AppendGasPath` extracts the genuine supported trace from every actual1216   successful append and discharges `ActualAppendGas.LogPath`. The resulting Θ1217   theorems prove returnedGas+919≤inputGas for exits and +1847 for deposits.1218   No path witness, gas bound, fee completion, owner or storage fit is supplied.1219   These are lower bounds on internal execution cost, not total transaction gas.1220 * `RefundAccounting` projects actual Υ transaction execution/finalization onto1221   its true provisional Θ/Lambda result and exact refund expression. It derives1222   all word-fit conditions from remaining≤limit and proves count≤reported net1223   gas when the independently counted events satisfy 919*count≤gross gas. It1224   includes failed transactions. The aggregate charge and valid remaining-gas1225   inputs still need a real, nonduplicated call-tree accounting proof.1226 1227 These results advance the coverage rows below without closing any of the three1228 public IDs. Extraction of initialized protocol histories, execution-event1229 accounting and the justified mathematical tariff domain1230 remain. Existing and reused direct-spec mutation checks remain finite corroboration;1231 final public-parent strength and sibling independence must still be reviewed.1232 1233 `MessageCall` retains the upstream empty-account-map fallback on successful1234 settlement. A consumer claiming direct identity with the `Ξ` post-world must1235 prove the surviving world is nonempty; it must not drop the fallback silently.1236 1237 The legacy Model and its existing theorems remain reproducible. The new direct1238 parents must not depend logically on the legacy 256-fuel price. Merely importing1239 an existing module which also defines `Model.Kind` is not a fee dependency.1240 1241 ## Clause coverage required before public closure1242 1243 | ID | Clause | Required complete-call evidence |1244 |---|---|---|1245 | P-SUBMIT-1 | Only allowed users submit | Caller/inhibitor gate, every rejection, and no effects on failure |1246 | P-SUBMIT-1 | Paid and well-formed | Actual completed fee, exact calldata size, minimum deposit and fee plus stake checks |1247 | P-SUBMIT-1 | One authentic record | Exact append window, count/tail updates, preservation outside the write set |1248 | P-SUBMIT-1 | One anonymous receipt | Existing log series plus exactly one log at the predeploy, no topics, authentic payload |1249 | P-DRAIN-1 | Only SYSTEM consumes | Complete caller partition and user/getter pointer preservation |1250 | P-DRAIN-1 | Oldest capped records | Content and length of the real return memory, cap 64/16, FIFO order |1251 | P-DRAIN-1 | Encoding | Deposit amount LE conversion; exit source address followed by pubkey |1252 | P-DRAIN-1 | Pointers and stale slots | Full reset versus partial head advance; all old slots from 4 preserved |1253 | P-CONTROL-1 | Dispatch and inhibition | CALLER alone; inhibited users rejected; SYSTEM still operates; pinned reversible semantics |1254 | P-CONTROL-1 | Getter and append | Getter fee/readonly effects; accepted append increments count and preserves excess |1255 | P-CONTROL-1 | SYSTEM updates | Drain first, nonempty latch/empty unlock or excess fold, count reset |1256 | P-CONTROL-1 | Constructors | Exact initializer execution and installed runtime/storage; deployment identity separate |1257 | P-CONTROL-1 | Mathematical formulas | Correct fee numerator versus next excess; untruncated tariff agreement on justified domain |1258 1259 Endpoint observations and fragment proofs are supporting evidence. They do not1260 alone close the rows involving committed records, logs or storage.1261 1262 ### Present coverage of the agreed clauses1263 1264 | Agreed clause | Implemented evidence | Remaining limitation |1265 |---|---|---|1266 | Inhibited users cannot commit effects | `UniversalGate` derives failure and whole-journal rollback from any actual completed Θ result | Evaluator OutOfFuel is not a completed result; deployment/code pin remains explicit |1267 | Paid, well-formed submission | `SuccessfulUser.*_admission` derives actual quote, exact length/payment and getter output from arbitrary-resource Θ success | Ordinary CALLVALUE equality and calldata size fit are explicit; mathematical tariff domain remains separate |1268 | Authentic record and one LOG0 | `AppendSpec.deposit_submission_receipt` proves the actual Ξ log is exactly the 184-byte calldata; both append helpers have one anonymous log | `AppendStorage` now covers record storage under local bounds; `ExitRecord` identifies exit bytes. `CommittedAppend` now joins storage/logs at Θ; `SuccessfulAppend` now derives those effects from arbitrary-resource success; history-derived bounds remain |1269 | Only SYSTEM consumes | `UserQueueInvariant` derives preservation/one-record extension for every actual completed user call; prior FIFO remains a prefix | Input queue representation and independent budget bound must be derived from initialized protocol histories |1270 | Oldest capped records and encoding | `SystemStateInvariant` identifies actual returned bytes and dropped suffix from arbitrary-resource Θ success | Input FIFO/source-width follows local concrete-history induction; valid protocol history extraction remains |1271 | Full/partial pointers and old record slots | `SystemSpec` and `CommittedSystem` prove exact word pointer updates and every slot ≥4 unchanged | `QueueArithmetic` supplies natural length/pointers under HEAD≤TAIL; derivation of that entry invariant remains |1272 | Caller dispatch and inhibition | User/SYSTEM inversion covers both actual caller classes; UniversalGate proves inhibited user rollback | Conditional direct parent implemented; protocol authorization/scheduling and mutation-based registration remain |1273 | Getter read-only; append count/excess | `GetterInversion` proves Θ getter preservation from actual success without resources/completion premises | `SuccessfulAppend` proves independent append controls from arbitrary-resource success under local fit; history-derived fit remains |1274 | SYSTEM count reset, latch/unlock/fold | `SuccessfulSystem` derives all word controls from actual Θ success; Bounded gives the natural sum bound | Budget accounting must be justified by valid protocol executions; natural calldata nonemptiness also needs size-word fit |1275 | Constructors | `InitializedInvariant` derives installed runtime, exact gating and initial empty FIFO/bounds from actual successful Lambda creation at an absent target | Explicit creation resource conditions; canonical deployment identity and valid protocol-history binding remain |1276 | Correct mathematical fee numerator/tariff | `SuccessfulUser.*_getter_math` proves actual Θ price agreement for independent pre-call numerator ≤2892; `MathFee` is untruncated | Protocol/funding justification of the domain remains; `FeeBoundary` refutes unrestricted agreement at 2893 |1277 1278 ## Direct specification and accounting continuation1279 1280 The frozen candidate at `5c3da89` adds code-independent data specifications and1281 actual CALL accounting. Isolated `make check` passed; exact source bindings and1282 reviews are in `direct-specs-build-20260909.json` and1283 `direct-specs-reviews-20260909.md`.1284 1285 * `DirectAdmission` derives the untruncated mathematical price and the checks1286   paid by the same successful user call. Its predicate contains no original-code1287   pin; only the correctness proof does. The pre-call enabled-safe domain remains1288   explicit. Deposit admission includes the actual minimum amount of 10^9 gwei.1289 * `AppendDataSpec` factors authentic record words, exact storage overlay, natural1290   controls and one anonymous receipt into pure data specifications. Correspondence1291   theorems recover the existing append specifications without weakening them.1292 * `SystemDataSpec` derives a code-independent four-slot overlay from actual Θ1293   success, then separates natural control and drain/stale-slot projections using1294   independent input bounds. These predicates can also be tested against mutants.1295 * `CallGasAccounting` and `CallDispatchGas` bind actual accepted CALL dispatch to1296   its literal child Θ invocation and returned gas. The natural debit includes1297   overhead minus stipend plus memory expansion; denied calls have no child event.1298   Child remaining-gas monotonicity and a nonduplicated full execution tree remain1299   separate obligations. CALLCODE/DELEGATECALL/STATICCALL/CREATE are not covered here.1300 * `FundingBounds` proves conditional external-credit envelopes below 2^163 (161301   withdrawals per payload) or 2^223 (a looser list bound), both below the certified1302   fee ceiling. The input lists, genesis bound, actual admission and conservation1303   are not established as protocol facts by this arithmetic theorem.1304 1305 The reviewed next steps are archived in1306 `direct-parent-packaging-next-20260909.md` and1307 `direct-funding-domain-next-20260909.md`. In particular, final mutation refutations1308 must satisfy independent domains and execute actual Θ; the existing Ξ mutant1309 receipts alone do not refute the complete-call parents. The three public IDs1310 remain open. Versioned funding references are supporting research, not changes1311 to the normative pins or a certified mainnet genesis state.1312 1313 ## Composed conditional direct guarantees1314 1315 The frozen candidate at `6fde5fc` passed isolated `make check`; bindings and1316 reviews are in `direct-parents-build-20260909.json` and1317 `direct-parents-reviews-20260909.md`. `DirectGuarantees` supplies exactly three parameter-code1318 predicates and pinned universal instances for both contract kinds:1319 1320 * `psubmit1_direct`: actual nonempty user success implies the enabled, paid1321   mathematical admission and the same authentic record/storage/log result.1322   Getters are read-only. SYSTEM adds no log and preserves every record slot.1323   Actual failure restores the journal. No signature check is claimed.1324 * `pdrain1_direct`: actual SYSTEM success returns the encoded oldest capped1325   prefix and leaves the represented suffix, with exact natural pointers and1326   stale-slot preservation. User calls preserve HEAD and either keep the queue1327   or append exactly one independently specified record; failures consume none.1328 * `pcontrol1_direct`: actual caller partitions control effects, with inhibition,1329   natural getter fee, count/excess updates and natural SYSTEM latch/unlock/fold.1330   It includes the separately quantified initializer and a SYSTEM progress clause:1331   owner presence, write permission, 2.5M gas and fuel≥8503 suffice for success on1332   either runtime, with **no enabled-storage premise**. Arbitrary-resource safety1333   remains separate from this sufficient-resource success clause.1334 1335 The input domains are pre-call owner/value/size observations, independent budget1336 and safe-fee invariants; drain also takes a represented queue and exit source1337 width. No original-code constraint occurs inside those domains. The standalone1338 call predicates do not require an external funding ceiling. `ConcreteHistory`1339 still requires funding and event bounds to preserve their preconditions.1340 1341 `DirectInitialization`, `DirectSubmit`, `DirectAppend`, `DirectControl`,1342 `DirectDrain` and `SystemFrame` compose existing execution proofs into these1343 observations. Getter preservation concerns created accounts, account lookups,1344 logs and zero value; access bookkeeping may change, as recorded in the archived1345 getter erratum. No full-substate getter equality is claimed.1346 1347 `AuditedChildGas` now derives a successful audited child's 919/1847 charge and1348 includes it once in the actual parent CALL debit without a supplied child-gas1349 bound or path. `TransferFunding` observes the real finite AccountMap balance1350 sum and proves that actual funded Θ entry transfer cannot increase it, including1351 alias and absent-account cases. General execution conservation, transaction1352 admission, nonduplicated event accounting and block/history extraction remain.1353 1354 The three new predicates are **conditional direct candidates**, not yet replacements1355 for the public Registry/YAML parents. Same-predicate actual-Θ mutation witnesses,1356 reviewed registration and protocol-domain justification remain acceptance gates.1357 1358 ## Same-predicate Θ control mutations and ordinary gas1359 1360 The frozen candidate at `0469f9c` passed isolated `make check`; exact source1361 bindings and reviews are in `direct-theta-control-build-20260909.json` and1362 `direct-theta-control-reviews-20260909.md`. `DirectThetaMutations` refutes **the exact new `PControl` predicate**1363 for both the caller-dispatch and TARGET mutations, with parameter-code domains1364 proved independently (budget 105), actual installed mutant code and actual1365 successful Θ results. A zero-value adapter proves exact equality with the old Ξ1366 runner inputs and derives the account witness that excludes empty settlement.1367 There is no new native execution evaluation: each finite refutation retains only1368 its corresponding historical native receipt axiom. The new universal parents1369 remain dependent only on standard Lean axioms. The other four Θ mutation1370 transports remain open, so public registration is still pending.1371 1372 `OrdinaryGas` covers exact accepted-step debit for every opcode except the six1373 recursive CALL/CREATE-family instructions, including GAS and SELFDESTRUCT.1374 INVALID is excluded by actual Z acceptance, not by trusting raw fallback behavior.1375 Actual ordinary prefixes and final successful halts are accounted; recursive1376 frames and full extraction/aggregation remain separate.1377 1378 ## Five actual-Θ mutation refutations and CALL-family accounting1379 1380 The frozen candidate at `778f4f5` passed isolated `make check`; bindings and1381 reviews are in `direct-theta-drain-build-20260909.json` and1382 `direct-theta-drain-reviews-20260909.md`. `DirectThetaDrainMutations` adds the exact new `PDrain` refutations for1383 both cap mutations and the stale-slot overwrite. Physical pre-queues and domains1384 are proved independently for arbitrary code; exit source width covers all 171385 entries, including the remaining one. Actual zero-value Θ calls reuse their old1386 Ξ receipts after exact entry/environment transport. Only the corresponding old1387 native receipt axiom remains in each finite refutation.1388 1389 Together with the two control refutations, five of the six required same-predicate1390 Θ mutants are implemented. The funded LOG0 witness remains open: an attempted1391 monolithic kernel evaluation of a zero-excess actual Θ fixture was killed with1392 exit 137 and produced no certificate. Its untracked draft is excluded from the1393 frozen validation candidate; work continues on smaller kernel-checked fragments.1394 No new native execution axiom is introduced to close it.1395 1396 `CallFamilyGas` extends real dispatch/child/gas/denied-branch accounting to1397 CALLCODE, DELEGATECALL and STATICCALL with their distinct stack layouts, source,1398 storage recipient, code target, real/apparent value and permissions. The local1399 child remaining-gas bound remains explicit for permitted calls. `CallFunding`1400 derives sufficient real transfer funds from those actual call gates, and binds1401 the entry budget to the exact child invocation extracted from StepOk. Neither1402 lemma assumes conservation of the world returned after child code execution.1403 1404 ## Universal remaining gas and ordinary funding1405 1406 The frozen candidate `d7de3a0` passed isolated `make check`; exact source hashes1407 and reviews are in `direct-recursive-gas-build-20260909.json` and1408 `direct-recursive-gas-reviews-20260909.md`.1409 `ReturnedGas` proves, by mutual strong induction on arbitrary evaluator fuel,1410 that completed X, Ξ, Θ and Λ results and every accepted actual step return no1411 more gas than they receive. This includes REVERT, both Θ/Λ statuses, the ten1412 precompiles, all six recursive instructions and CREATE's actual caught-error1413 branch. No child-gas bound, code pin or finite iteration cutoff remains in the1414 universal theorem's premises. Interpreter errors have no invented endpoint.1415 `CreationGas` supplies literal CREATE/CREATE2 dispatch and code-deposit debits.1416 1417 `TransactionGas` now derives the real Υ provisional remaining-gas bound and its1418 exact natural capped-refund/net-gas formula from execution. Its count-to-net-gas1419 corollary still requires an independently established aggregate append charge;1420 it does not manufacture event counting or protocol transaction validation.1421 1422 `StorageFunding`, `SelfdestructFunding` and `OrdinaryFunding` prove that actual1423 accepted nonrecursive instructions cannot increase the finite AccountMap sum1424 of balances. Persistent/transient writes preserve it; SELFDESTRUCT handles both1425 same-address policies, absent accounts and possible modular-credit loss. There1426 is no assumed supply ceiling or predicted post-state. Recursive funding,1427 transaction escrow/settlement, external credits and protocol history remain.1428 1429 ## Registered conditional direct parents and six Θ refutations1430 1431 The frozen registration source `9d44bcf` passed isolated `make check`. Its1432 exact source hashes and log are in `direct-registration-build-20260909.json`;1433 independent metadata and mutation reviews are recorded alongside it. The public1434 YAML now selects exactly `DirectGuarantees.psubmit1_direct`, `pdrain1_direct`1435 and `pcontrol1_direct`, for both contract kinds. Scope is explicitly1436 `THETA_CONDITIONAL_FORALL`: the local theorem is checked and overall protocol1437 closure stays PARTIAL/OPEN. AllGuarantees checks these exact predicate instances.1438 No finite receipt is conjoined into a universal correctness parent. Original1439 CFG/model parents, kill-lines and metadata remain in Lean and `audit/history`.1440 The earlier sections saying registration is pending describe prior snapshots.1441 1442 `DirectThetaSubmitMutation` certifies all 158 actual instruction steps of a1443 zero-excess funded LOG0 mutant, then the same Ξ and settled Θ result.1444 `DirectThetaSubmitCounterexample` independently proves its budget-0 domain,1445 real sender funding and two-ETH pre-world total, and refutes exactly PSubmit.1446 The complete wrapper now compiles; the earlier monolithic/normalization memory1447 failures produced no accepted result and were replaced by small proved steps1448 and finite-map funding identities. No new native evaluation axiom is used.1449 `DirectThetaKills` gathers the six exact predicate negations for metadata only.1450 1451 The five control/drain witnesses keep their disclosed historical native receipt1452 axioms. Their sibling Boolean regression checks do not establish universal1453 independence. The new guarantees deliberately overlap: SYSTEM stale-slot1454 corruption contradicts both drain preservation and the PSubmit record frame.1455 No clause was weakened to manufacture a disjoint test matrix. The independent1456 registration review records the conservative cross-impact matrix; only the six1457 named same-predicate refutations are advertised as compiled test conclusions.1458 1459 Protocol-domain coverage, actual nested-event aggregation and initialized valid1460 history extraction remain separate obligations. Registering this stronger1461 conditional evidence does not complete the agreed audit.1462 1463 ## Actual recursive execution and transaction funding1464 1465 The frozen funding source `c92e0f8` passed isolated `make check`. Exact hashes1466 and the successful log are in `direct-recursive-funding-build-20260909.json`;1467 independent reviews are in `direct-recursive-funding-reviews-20260909.md`.1468 1469 `CallWorld` and `CreationWorld` extract the literal child invocation and returned1470 world from actual accepted recursive steps, including denied calls and CREATE's1471 caught-error/empty-world branch. `CreationFunding` handles nonce changes and1472 code installation. It treats sender/creation-address aliasing separately:1473 Λ's intermediate debit/credit can increase the map sum in that case, but the1474 actual nonzero nonce selects INVALID code and the completed creation restores1475 the input world. No hash-injectivity assumption hides this case.1476 1477 `ExecutionFunding` proves by mutual strong induction on arbitrary evaluator1478 fuel that completed execution cannot increase the finite sum of balances.1479 X/Ξ cover successful states; Θ and Λ cover both statuses and the actual rollback1480 rules, with funded input transfer and, for Λ, an existing nonzero sender nonce.1481 Accepted steps derive child funding and nonce facts from their actual gates.1482 The proof includes every recursive opcode and all ten precompiles; no child1483 conservation result or predicted post-world bound is an input hypothesis.1484 1485 `FinalizationFunding` proves actual modular credits, account deletion folds1486 and transient-storage cleanup bounds. `TransactionFunding` then proves an exact1487 Υ settlement equation and nonincrease of the whole transaction's world funds.1488 Its independent admission conditions require the existing sender, sufficient1489 natural balance for upfront gas/blob fees plus value, bounded pre-increment1490 nonce, and priority price no greater than effective price. They are not yet1491 extracted from a protocol validation implementation. The proof uses the actual1492 provisional execution, refund cap, beneficiary credit and cleanup, for either1493 returned status. No new native execution receipt or project axiom is used.1494 1495 These endpoint results do not themselves establish every intermediate call's1496 budget, nested append counting, external issuance/withdrawal accounting, or a1497 valid initialized protocol history. Those obligations remain open.1498 1499 ## Linked funding history and all-outcome local events1500 1501 The frozen source `c0c6bea` passed isolated `make check`. The exact-source1502 receipt is `direct-local-events-build-20260909.json`; independent reviews are1503 in `direct-local-events-reviews-20260909.md`. New proofs use only standard1504 Lean axioms.1505 1506 `FundingHistory` links actual Υ transactions, zero-value SYSTEM Θ calls and1507 literal AccountMap credits. Its constructors assume independent input admission1508 and actual execution receipts, never a post-world funding bound. The proof1509 derives each resulting world's budget from initial funds plus accumulated1510 explicit credits. It also bounds every actual XRuns prefix, including prefixes1511 whose later execution reverts or errors. Protocol provenance of those credits1512 and transactions and a bound on the initial-plus-credit sum remain required.1513 1514 `FrameEvents` extracts certificates from every actual X outcome: successful1515 halt, REVERT, guard rejection, failed step and OutOfFuel. Its marked events are1516 actually completed LOG0 instructions with actual length at least 68 bytes.1517 The proof derives `residual + 919 * localEventCount <= entryGas`; an error has1518 accounting residual zero, without inventing an actual error gas field. The1519 local list is unique and has no duplicate occurrences even through PC loops.1520 Existing XRuns prefixes embed in that same certificate. `AppendEvents` binds1521 both successful audited append paths to occurrences in this unique list.1522 1523 This is frame-local accounting: recursive instructions are actual opaque steps1524 and their descendant events are not counted yet. Fuel labels distinguish local1525 occurrences only; they cannot serve as globally unique call-tree IDs. Full1526 nested counting needs actual child/error extraction and disjoint structural1527 paths, including events before a child or ancestor error. The implementation1528 proposal in `audit/receipts/direct-event-accounting-design-20260909.md` lists1529 these remaining adapters and the eventual actual-Υ/refund composition.1530 1531 ## Recursive error adapters and child-charge induction edges1532 1533 The frozen source `b0af68d` passed isolated `make check`. Its exact-source1534 receipt is `direct-child-outcomes-build-20260909.json`; independent reviews1535 are in `direct-child-outcomes-reviews-20260909.md`.1536 1537 `CallOutcome` gives exact CALL-family step/helper equations for all outcomes,1538 including error equivalence to the admitted literal child Θ error, no-child1539 denied results and the zero/one-fuel boundaries. Actual Z alone bounds the1540 stipend-inclusive allowance. `CreationOutcome` exposes the literal Λ child and1541 CREATE/CREATE2 settlement for all outcomes. It retains catch of every child1542 error, including OutOfFuel, and the post-child word-addition guard that can1543 reject a final step. It does not replace that guard by a natural inequality or1544 assume a successful parent.1545 1546 `RecursiveEventDebit` transports a charge on the same actual child to its actual1547 parent step. This covers both returned statuses, propagated errors, caught1548 creation errors and post-child guard rejection, with no double charging of1549 CALL's forwarding allowance. **These are induction edges:** the child's1550 `residual + charge <= allowance` bound is still an explicit hypothesis. They1551 are not yet the universal nested-event theorem. A mutual actual trace1552 extraction, structurally distinct child/continuation occurrence paths, and1553 composition with the actual Υ refund and valid block accounting remain open.1554 1555 ## Structural occurrence trees and execution-wrapper charge edges1556 1557 The frozen source `68c083a` passed isolated `make check`. Its exact-source1558 receipt is `direct-event-tree-edges-build-20260909.json`; independent reviews1559 are in `direct-event-tree-edges-reviews-20260909.md`.1560 1561 `EventTree` supplies fixed structural addresses: the local marked occurrence is1562 at `[]`, child addresses start with `false`, and continuation addresses start1563 with `true`. Its occurrence list has no duplicates and its length equals its1564 count. Repeated PC values, reused fuel in different frames and identical1565 subtrees do not collapse these structural addresses. This is pure structural1566 support, with no evaluator or gas claim by itself.1567 1568 `WrapperEventDebit` proves that actual Ξ preserves the X accounting residual,1569 and that the actual code Θ and Λ settlement can only reduce their own selected1570 execution's residual, including rollback and error outcomes. Failed creation1571 address encoding has zero residual and no selected init execution. Explicit1572 child-charge hypotheses transport through those wrappers. These proofs do not1573 yet provide the mutual nested-event certificate or its extraction, and the1574 raw precompile/zero-fuel wrapper cases still need their tree adapters. The1575 structural and wrapper results supply parts of that remaining composition;1576 they do not discharge it by definition.1577 1578 ## Remaining proof obligations and owners1579 1580 | Obligation | Dependency | Owner | Next verifiable result |1581 |---|---|---|---|1582 | Full getter from actual success | GetterInversion + SuccessfulUser | Validated at f52112e | Actual Θ output and read-only effects without assumed completion; mathematical tariff has explicit domain |1583 | Derive quote completion from successful runtime execution | SuccessInversion + SuccessfulQuote | Validated at 018cd2d | Actual successful user Θ implies a completed operational quote, without a gas bound |1584 | Append storage and log postconditions | SuccessfulAppend + UserQueueInvariant | Implemented with independent domain bounds | Actual Θ effects derive from success; initial representation and accounted budget remain to justify |1585 | Drain contents and FIFO | CommittedSystem already covers word pointers and every stale slot | Queue lane, consumed by integrator | Actual returned bytes equal independent concatenated oldest records |1586 | Remaining call composition | User and SYSTEM Θ at arbitrary resources; state/FIFO preservation | Implemented locally | Three direct predicates and all six same-predicate Θ mutants are implemented; registration validated at 9d44bcf; protocol-domain closure remains |1587 | Exact initialization and protocol history | InitializedInvariant + ConcreteHistory + versioned EL/CL references | Integrator/protocol lane | Extract actual transaction/block histories, including ancestor rollback and external frames, and justify address/scheduling |1588 | Structural bounds | AccountedState local preservation + independent execution-event budget | Queue/protocol lane | Actual initialized-history induction, including locally successful events later rolled back, and real gas/refund bridge |1589 | Mathematical tariff domain | Independent natural recurrence + justified resource/funding bounds | Fee/protocol lane | Bound on every intermediate and required execution resources |1590 | Final normative version/inhibition | Author clarification draft | Thomas | Explicit chosen versions and intended inhibition behavior |1591 1592 No numeric effort estimate is certified by this inventory. Calibrate new proofs1593 from bounded attempts and actual compiler/reviewer results; separate integration1594 work, new lemmas and external decisions. The most uncertain items are validated block accounting, initialized-history1595 preservation, and protocol justification of the mathematical-fee domain.1596 1597 ## Verification and delivery1598 1599 Run the FFI prerequisite, targeted module builds, axiom reports, relevant1600 mutation modules, metadata validation and `make check` on the final candidate.1601 Keep a single heavy build on this Mac and separate mutable build caches.1602 1603 Finite differential tests must retain engine version, bytecode hashes,1604 pre-states, inputs and results. Injected storage is not protocol reachability.1605 Test-budget exhaustion is not out-of-gas. Existing kill-lines remain, and new1606 direct postconditions must detect the corresponding semantic mutations.1607 1608 `make direct-regressions` runs the optional local Anvil corroboration. The saved1609 `audit/receipts/direct-semantics-20260909.json` records the script SHA-256,1610 Anvil/revm client version, Prague hardfork, pinned code hashes, exact injected1611 states, results and timestamps. Its ten fee/getter cases and seven other1612 transactions passed. Getter checks include actual committed transactions and1613 nonempty traces without writes/logs; `eth_call` alone would not establish that.1614 The enclosing-revert case checks successful inner append instructions before1615 rollback and distinguishes refunded call value from transaction gas paid.1616 These are finite observations on injected states, not protocol reachability.1617 1618 Before integration, an independent reviewer receives the exact commit and its1619 full dependencies. No merge to main, external transmission, normative change1620 or publication is implied by a successful local build.1621