feat(bootloader): prove the verify-core — "loads only verified bytes"#3
Merged
Conversation
…ied bytes" The proof side of the layer-1-UI / PWA boot-blob work (Xahau discussion #759, xahaud PR #760). An on-chain bootloader is the root of trust for a Hook's UI: it fetches a larger stage-2 app and must run it ONLY if the bytes hash to the pinned value. That go/no-go gate is small + bounded — exactly what this engine proves. prove_bootloader.py proves: accept (hand control to stage-2) => candidate hash == pinned hash, all 32 bytes. A loader satisfying it cannot be tricked into executing unverified code, so prove(Hook) + prove(bootloader) = the whole app's trust base formally verified, UI included. Same byte-exact-equality discipline as the guardrail's dst-lock, here over a 32-byte SHA-512Half. Fixtures + matrix: bootloader_verify (full 32-byte compare) -> PROVEN(0); bootloader_prefix_bug (only 4 of 32 bytes) -> COUNTEREXAMPLE(2); bootloader_skip_bug (no check at all) -> COUNTEREXAMPLE(2). 143 tests pass. SCOPE: proves the verify gate's accept condition; the wallet supplies the candidate hash = SHA-512Half(fetched bytes). Honest about that boundary in the driver docstring. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Hugegreencandle
added a commit
that referenced
this pull request
Jun 20, 2026
…-SWITCH (primitive #3) inactivity-release: accept-with-emit => ledger_last_time >= last_seen + TMO (128-bit, underflow-safe) — a dead-man-switch / inheritance / recovery Hook releases ONLY after the owner has been inactive for >= TMO seconds; any owner activity (which updates last_seen, slot 0x02) resets the timer. ledger_last_time is SYMBOLIC -> proven for ALL times. A hook that emits without reading the time OR last_seen fails closed to COUNTEREXAMPLE. deadman_ok = the most complex hook yet (TWO behaviors: owner-activity records last_seen=now [only- increase, keeps monotonic]; cron releases after inactivity), certifying 7 PROVEN invariants: inactivity-release [NEW] + emit-budget + emit-dst-lock + trigger-lock + nospend + monotonic (across 2 slots) + termination. AUDITED BEFORE COMMIT (2 parallel auditors): driver sound (no false-PROVEN; byte order verified via the deadman_ok-PROVEN logic — NO false byte-order CRITICAL this time) + hook sound (owner detection guarded, inactivity gate underflow-safe, slots distinct/monotonic, emit only on cron+inactive+in-cap, no grief/ premature/over-release). Applied the one fail-closed nit (INCONCLUSIVE on a wrong-length last_seen slot). deadman_ok->PROVEN, deadman_early_bug->CEX, vesting (no TMO)->N/A. 156 tests, soundness 0 false-PROVEN. Prover now 35 invariants; 3 certified autonomous primitives (subscription, vesting, dead-man-switch). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The proof side of the layer-1-UI / PWA boot-blob work — Xahau Discussion #759, xahaud draft PR #760.
An on-chain bootloader is the root of trust for a Hook's UI: it fetches a larger stage-2 app and must run it only if the bytes hash to the pinned value. That go/no-go gate is small + bounded — exactly what this engine proves.
prove_bootloader.pyproves: accept (hand control to stage-2) ⟹ candidate hash == pinned hash (all 32 bytes). This closes one link — the gate's accept logic — the same byte-exact-equality discipline as the guardrail's dst-lock, here over a 32-byte SHA-512Half. Out of model + trusted (do not read this as "whole app proven"): the on-chainSetBootstores the blob verbatim and verifies nothing; the wallet'sSHA-512Half; stage-2 sandboxing. The proven artifact is a reference model, not a deployed hook.Matrix
bootloader_verify(full 32-byte compare) → PROVEN (0)bootloader_prefix_bug(only 4 of 32 bytes) → COUNTEREXAMPLE (2)bootloader_skip_bug(no check) → COUNTEREXAMPLE (2)143 tests pass.
Scope (honest): proves the verify gate's accept condition; the wallet supplies the candidate =
SHA-512Half(fetched bytes). Stated in the driver docstring.🤖 Generated with Claude Code