feat(oci): tune per-stage shadow stacks (OCI-P06) — and unskip the verifiers that never ran - #355
Open
avrabe wants to merge 1 commit into
Open
feat(oci): tune per-stage shadow stacks (OCI-P06) — and unskip the verifiers that never ran#355avrabe wants to merge 1 commit into
avrabe wants to merge 1 commit into
Conversation
…rifiers that never ran
THE THIRD BLOCKER in this chain, and again found by a consumer running the
thing the previous fix enabled.
`__stack_pointer` init IS the stack size: the stack is [0, SP) growing down and
static data begins exactly at SP. All six published components carried
SP = 1048576 — the wasm-ld default, never set. meld's `--share-stack` (v0.48.0)
sizes ONE shared region as max_i(stack_i), so a single untuned participant
sizes it for everyone: 128x the F100's 8 KB SRAM, 4x the M7's 256 KB DTCM.
So the flag was sound and correct and bought NOTHING for the falcon set.
Removing memory.grow (OCI-P02) and adding relocations (OCI-P05) were each
necessary and neither sufficient. This is the third.
PER-STAGE, not uniform (jess's call, and the better argument): the two sizings
differ 8x where --share-stack is NOT used (total = sum) and are a wash where it
is — and its precondition holds only for the five LEAVES, since the `cascade`
orchestrator's frame is live across all of them. Per-stage is good in both
worlds; uniform is only competitive in the conditional one.
rate attitude position mixer 512 (scry bounds 16-112 B; 5-32x headroom)
iekf ekf cascade 8192 (iekf bound 4192 B; 2x)
flight 16384 (measured floor 12288 B)
EVIDENCE GRADES, which differ and are labelled in the artifacts:
MEASURED HERE rate passes its closed-loop proof at 512 B, convergence
identical to the 1 MB build (0.193 s); flight traps at 10240,
passes at 12288 with output bit-identical to the control.
BORROWED iekf/position/attitude/mixer bounds are jess's scry figures,
NOT reproduced here — those four have no execution oracle.
They corroborate: scry bounds flight at 10688, inside the independently
measured bracket (10240 traps < 10688 < 12288 passes).
A control was essential and nearly missed: the first sweep trapped at EVERY
size including 8192, which looked like a broken flag. Building --emit-relocs
alone reproduced the published output exactly, establishing the traps as signal.
--- AND A DEFECT FOUND BY RUNNING THE GATE ON MY OWN NEW VERIFIER ---
All four OCI-005 steps came back `skip-bench-only`, including three cheap
config greps. Cause: BENCH_PATTERNS matched
\bbuild-(flight-)?components?\.sh\b
unanchored — so any step that merely NAMED the script was classified bench-only.
FV-FALCON-OCI-004 (merged in #352/#353) was therefore shipping with ALL THREE
of its steps skipped: it verified NOTHING in CI. I cited "7 steps PASS" in that
PR; those passes were other artifacts'. A verifier that cannot run is
indistinguishable from one that passes — the same failure as the zero-match
filter (#342), one level down.
Anchored to INVOCATION rather than mention, with both shapes unit-tested:
scripts/build-components.sh 1.56 -> bench-only (correct)
bash|./ variants -> bench-only (correct)
grep -q '...' scripts/build-components.sh -> RUNS (was skipped)
Gate on the oci set: PASS 7 -> 11. Four assertions now actually execute.
Genuinely bench-only steps (wasm-tools, wasmtime) still skip.
rivet validate v0.19.0 — the version the gate pins: PASS, exit 0
gate (has-tag "oci"): 11 PASS, 0 FAIL, 8 bench-skipped
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
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.
Verify-Filter: (has-tag "oci")
The third blocker in this chain — and again found by a consumer running the thing the previous fix enabled.
The problem
__stack_pointerinit is the stack size: the stack is[0, SP)growing down, static data begins exactly at SP. All six published components carried SP = 1048576 — the wasm-ld default, never set.meld's
--share-stack(v0.48.0) sizes one shared region asmax_i(stack_i), so a single untuned participant sizes it for everyone:The flag was sound and correct and bought nothing for the falcon set. Removing
memory.grow(OCI-P02) and adding relocations (OCI-P05) were each necessary and neither sufficient.Per-stage, not uniform
jess's call, and the better argument: the two sizings differ 8× where
--share-stackis not used (total = Σ) and are a wash where it is — and its precondition holds only for the five leaves, since thecascadeorchestrator's frame is live across all of them. Per-stage is good in both worlds; uniform only competes in the conditional one.Evidence grades — they differ, and the artifacts say which is which
Measured here, by build-and-execute:
ratepasses its through-wasm closed-loop proof at 512 B, convergence identical to the 1 MB build (0.193 s).flighttraps at 10240, passes at 12288, output bit-identical to the control.Borrowed, not reproduced: the bounds for
iekf/position/attitude/mixerare jess's scry figures. Those four have no execution oracle here.They corroborate rather than merely coexist: scry bounds
flightat 10688, which sits inside the independently measured bracket (10240 traps < 10688 < 12288 passes).A control was essential and nearly missed. The first sweep trapped at every size including 8192, which looked like a broken flag. Building
--emit-relocsalone reproduced the published output exactly — that's what established the traps as real signal.And a defect found by running the gate on my own new verifier
All four OCI-005 steps came back
skip-bench-only— including three cheap config greps. Cause:Any step that merely named the script was classified bench-only.
FV-FALCON-OCI-004— merged in #352/#353 — was therefore shipping with all three steps skipped. It verified nothing in CI. I cited "7 steps PASS" in that PR; those passes belonged to other artifacts. A verifier that cannot run is indistinguishable from one that passes — the same failure as the zero-match filter (#342), one level down.Anchored to invocation, both shapes unit-tested:
scripts/build-components.sh 1.56bash/./variantsgrep -q '…' scripts/build-components.shGate on the oci set: PASS 7 → 11. Four assertions now actually execute; genuinely bench-only steps still skip.
Status:
implemented, notverifiedOCI-P06's kill-criterion — the fused cascade's shared region fits the budget and the image executes — is gale/meld's. The four borrowed bounds are the likeliest place for it to fail, and the artifact says so.
Refs pulseengine/meld#370, pulseengine/jess#167.
Evidence: pinned rivet v0.19.0 validate PASS exit 0; gate 11 PASS / 0 FAIL / 8 bench-skipped.
🤖 Generated with Claude Code