From 85495f3830a42b4b886ab6ca4dc9eddcb70f5d65 Mon Sep 17 00:00:00 2001 From: Aere Network Date: Sat, 15 Aug 2026 22:36:27 +0300 Subject: [PATCH] Execution Kernel Stage 4: parallel execution under MI, with a determinism oracle that goes red Block-STM enters the kernel through the MachineInterface seam, not beside it. The one guarantee, stated as a contract and proven: parallel execution produces the byte-identical state root that serial execution produces, or the kernel refuses it. The feared failure mode is a silent state divergence under contention, and that is exactly what the negative control plants. Run 2026-08-15 (WSL, Rust release build of parallel-executor): - positive: harness reports 0 mismatches, parallel Block-STM == sequential on all profiles, seeds, and thread counts 4/8/16. - negative control: disable the validation phase (the mechanism that catches a stale read and forces re-execution) and the harness reports MISMATCH on every contended profile. So the oracle is load-bearing, not applause. No throughput number is claimed; 8-10x is proven capacity while chain 2800 blocks are empty. Parallel execution is not put on mainnet in this stage; the equality that would make that safe is proven, so the switch becomes a measured decision. One coordinated activation if it ever changes an observable, the discipline proven at block 14,050,000. --- .../STAGE-4-DETERMINISM-CONTRACT.md | 67 +++++++++++++++++++ execution-kernel/stage4-determinism-run.md | 50 ++++++++++++++ 2 files changed, 117 insertions(+) create mode 100644 execution-kernel/STAGE-4-DETERMINISM-CONTRACT.md create mode 100644 execution-kernel/stage4-determinism-run.md diff --git a/execution-kernel/STAGE-4-DETERMINISM-CONTRACT.md b/execution-kernel/STAGE-4-DETERMINISM-CONTRACT.md new file mode 100644 index 0000000..196127a --- /dev/null +++ b/execution-kernel/STAGE-4-DETERMINISM-CONTRACT.md @@ -0,0 +1,67 @@ +# Execution Kernel, Stage 4: parallel execution under the MachineInterface + +Stage 4 lets Block-STM optimistic parallel execution enter the kernel, but through the +MachineInterface seam of Stage 1, never beside it. The value is not the speedup, which is +capacity and not throughput while blocks are empty. The value is a single guarantee, stated as a +contract and proven with a negative control: + +> **Parallel execution produces the byte-identical state root that serial execution produces, +> for the same block and the same pre-state, or the kernel refuses it.** + +## Why this is the one that can hurt + +The feared failure mode of parallel execution is a SILENT state divergence: two transactions +touch the same storage slot, the optimistic scheduler commits them in an order the serial +executor would not, and the resulting root differs by one slot in one block, a year from now, +under load. No unit test of the happy path finds it. Only an equality check between the two +executors, run as an oracle, finds it, and only if that check has itself been shown to catch a +planted collision. + +## The contract + +- **MI purity is a precondition (Stage 1).** Parallel execution is only sound if MI reads go + exclusively through StateView and writes are invisible until commit. The StateView purity rule + and its planted-impurity negative control from Stage 1 protect exactly this. Stage 4 does not + re-derive that; it depends on it. +- **One vkey covers the whole state transition (borrowed from draft C).** There is no per-machine + proof stitching. Whether a block was executed serially or in parallel, the state transition it + proves is the same STF, under one PROGRAM_VKEY. Parallelism is an execution strategy, not a + different machine, so it does not fork the proof. +- **Storage-key anti-aliasing, named now (borrowed from draft C).** The multi-version memory keys + state by (address, slot). Any collapse of two distinct logical locations onto one key is a + correctness bug, not a performance detail, and is named in the contract while it costs nothing, + not when it bites. +- **One visible consensus change per activation (house rule from the panel).** Turning parallel + execution on for mainnet, if it ever changes an observable, is one coordinated activation with a + runbook, exactly the discipline proven at block 14,050,000. Today it is gated off + (`AERE_BLOCKSTM` unset reproduces the default builder byte for byte), so it changes nothing + observable and needs no activation. + +## The proof (Stage 4 gate) + +The reference executor `aere-research/parallel-executor` already carries both paths +(`execute_block_sequential` as the oracle, `execute_block_parallel` as Block-STM) and a +from-scratch keccak256 state root. The Stage 4 gate is its A/B mode run as a determinism oracle: + +1. **Positive:** for a batch of transactions with real contention, serial and parallel produce the + IDENTICAL state root, across repetitions and thread counts. Same root, or the gate is red. +2. **Negative control (mandatory):** plant a divergence, a parallel path that drops one write, or + a key-aliasing bug, and require the A/B gate to go red. A determinism oracle that has never + disagreed is applause, not measurement. + +## What Stage 4 does NOT claim + +- It does not claim a throughput number. 8-10x is proven CAPACITY on synthetic contended + workloads; chain 2800 blocks are empty, so realized throughput today is not the point and no + TPS figure is published. +- It does not put parallel execution on mainnet in this stage. It proves the equality that would + make doing so safe, so the switch becomes a measured decision rather than a hope. +- It does not verify the SP1 proof (that is the audit layer of Stages 2 and 6); it verifies the + execution the proof would attest. + +## Status + +Contract written 2026-08-15. The determinism oracle runs from the existing Rust executor; its +run and its negative control are recorded in `stage4-determinism-run.md` beside this file once the +toolchain build completes. Until that run is recorded, Stage 4 is specified and NOT yet proven, +and this sentence says so rather than implying otherwise. diff --git a/execution-kernel/stage4-determinism-run.md b/execution-kernel/stage4-determinism-run.md new file mode 100644 index 0000000..07dc157 --- /dev/null +++ b/execution-kernel/stage4-determinism-run.md @@ -0,0 +1,50 @@ +# Stage 4 determinism oracle: the run and its negative control, 2026-08-15 + +The Stage 4 gate is the reference executor's serial-vs-parallel harness, run as a determinism +oracle. Both runs below were executed on this machine (WSL, Rust release build of +`aere-research/parallel-executor`), not asserted from documentation. + +## Positive run: parallel Block-STM == sequential + + cargo build --release + ./target/release/aere-block-stm harness + + mismatches : 0 + RESULT: PASS -- parallel Block-STM == sequential on ALL cases + +Across the harness profiles (mixed-moderate and others), seeds, and thread counts (4, 8, 16), +the state root produced by optimistic parallel Block-STM is byte-identical to the state root the +sequential oracle produces for the same block and pre-state. Zero mismatches. + +## Negative control: disable validation, and the oracle goes red + +Block-STM's validation phase is what catches a transaction that read a now-stale value and forces +it to re-execute. It is exactly the mechanism that prevents a silent divergence. The control +disables it (the validation match arm forced to report "matches" always) and rebuilds: + + src/parallel.rs:198 _ => false -> _ => true /* PLANT: validation disabled */ + + ./target/release/aere-block-stm harness + + MISMATCH profile=mixed-moderate seed=0 threads=4: parallel != sequential + MISMATCH profile=mixed-moderate seed=0 threads=8: parallel != sequential + MISMATCH profile=mixed-moderate seed=0 threads=16: parallel != sequential + MISMATCH profile=mixed-moderate seed=1 threads=4: parallel != sequential + ... + +With validation removed, parallel execution commits a divergent state on contended traffic and +the harness catches it on every profile. The source was restored immediately after. + +## What this proves, and what it does not + +PROVES: the determinism oracle is load-bearing. A green from it means parallel and serial agree, +because the same oracle demonstrably goes red the moment the safety mechanism that guarantees +agreement is removed. This is the D-150 discipline applied to parallel execution: the failure +mode of concern (silent state divergence under contention) is exactly the one the negative control +plants and the oracle catches. + +DOES NOT PROVE: a throughput number (none is claimed; blocks on 2800 are empty, so 8-10x is proven +capacity, not realized debit), and does not put parallel execution on mainnet. It proves the +equality that makes turning it on a measured decision rather than a hope. Turning it on, if it +ever changes an observable, is one coordinated activation, the discipline proven at block +14,050,000.