mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-05 20:30:58 +00:00
mrwulf
a46b92b41b
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
25 lines
2.1 KiB
Text
25 lines
2.1 KiB
Text
c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4 AUDIT-MANIFEST.txt
|
|
6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh
|
|
a556559d7dba1b565aad6724112e4f3aec73ad0b6a29c34855998edbf402f2d1 check.sh
|
|
5e582e44dfd210cb5b8e56f6c31907162fc8e1adf7dac7caf3afb435bbaccb53 extract.sh
|
|
d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4 GEN-MODEL.sha256
|
|
9acc69d66d0c35a88da6d6d020027e5b66ce992763cef3af8de653319abfbb8c inventory-allowlist-scalar.txt
|
|
8e2950712ce39ace9cffd3bb58a13984832ff7f3f43ba7b68aa2b1eaa2bc2116 inventory-allowlist.txt
|
|
0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh
|
|
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
|
b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh
|
|
7a9c89cf2b96313bd4bcddb534e8d06724bd7250234e670baadf6a9b0d1fbf81 model-correspondence.py
|
|
665cea5463959d5bc80c6549bf899c0450f3e9d597a4ac6acae7f1559325c1e8 MODEL-CORRESPONDENCE.txt
|
|
79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8 Proofs/Audit.lean
|
|
18e0cef25366bdcda67e8e347a222c169469654547b87adb01eb5b12aa9a9529 Proofs/InventoryBasic.lean
|
|
2b4f2bad2c82c64a1d29c873554b1728b86148f0bc27324c6e0b16defda22ca9 Proofs/InventoryCore.lean
|
|
132a1b039c70f4252c43be0ad5823145887e3e8c9f199d7e0f12d184c65ce265 Proofs/Inventory.lean
|
|
6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean
|
|
bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh
|
|
6de61b2b08ab6e05c7d38377ea8f70178da4a105bb1df21c6ba6bc05a647090d selftest-axgate.sh
|
|
7822c007d12d7be70003ea9de234102a2c4165cfab65a108e2960e51b87bee82 selftest-correspondence.sh
|
|
41d16df48b15b99512d10a805bb811db301e9d9c8b00e5e3e0186f0110d3b71a selftest-harness.sh
|
|
1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh
|
|
fc6d2905871500f2ee9c3f308fd8300cfcd1a7fa854d399d13812f7e2282f1fd selftest-shapes.sh
|
|
eb7367a1494f5203f0cbeace78c9522608d51825fdcbb7ae40962d2380a7bc79 selftest-statements.sh
|
|
7603b82c9c29a27f6659b8878d1a2e2365afb6541c3c5b2698ab2fee21bb2bde selftest-tiers.sh
|