feature: SIL reference vector for the cascade differential (DD-026 P2) — ARM half blocked on Renode resume, recorded honestly - #189
Merged
Conversation
…, jess's half)
relay proves the loop closes in source; jess proves it still closes after lowering. This is jess's
half — NOT a second simulator (relay owns SIL), but a single discriminating vector with a known-good
answer for the lowered ARM to be checked against.
sil_reference.py runs the SAME fused core module synth lowers, in wasmtime. One module, two
backends: any divergence is a lowering defect, not a modelling difference.
rate@0.7.0#tick : (param i32) -> (result i32) canonical ABI, pointer in / pointer out
arg -> vehicle-state (14 f32) ++ rate-setpoint (4 f32); ret -> torque-setpoint (4 f32)
REFERENCE: state w=(0.30,-0.15,0.07), sp=(1.0,0,0,0.5)
-> torque tx=1 ty=0.472507507 tz=-0.147003502 thrust=0.5
hex 3F800000 3EF1EC81 BE168816 3F000000
The vector is deliberately ASYMMETRIC — distinct body rates on all three axes. A symmetric or
all-zero input would be a vacuous differential, reproducible by a miscompile that drops terms.
ty and tz are non-obvious functions of the rate error, which is what makes it discriminating.
ARM SIDE NOT WORKING — attempt kept with what IS established: entry at 0x7a4, r0 = arg pointer,
r9 = globals base 0x20010100 (verified live), reset sequence, linmem mapping wasm 0x2280 ->
ARM 0x20002380. Blocker: after RunFor reaches the spin at 0x16c, setting cpu PC and resuming does
not execute (PC stays, r0 unchanged), with or without the thumb bit. That is Renode CPU-resume
plumbing, not falcon. Next attempt: drive the call from inside the image via a harness export, so
no PC redirect is needed — which is closer to how the on-target test must work anyway.
rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <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
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.
DD-026 P2 splits the proof: relay proves the loop closes in source (SIL); jess proves it still closes after lowering. This is jess's half — deliberately not a second simulator (relay owns SIL), but a single discriminating vector with a known-good answer for the lowered ARM to be checked against.
sil_reference.py— doneRuns the same fused core module synth lowers, in wasmtime. One module, two backends: any divergence is a lowering defect, not a modelling difference.
The vector is deliberately asymmetric — distinct body rates on all three axes. A symmetric or all-zero input would be a vacuous differential, reproducible by a miscompile that drops terms.
tyandtzare non-obvious functions of the rate error, which is what makes it discriminating rather than decorative.ARM half — not working, and recorded as such
What is established (all verified live in Renode, not inferred):
rate@0.7.0#tickat0x7a4r0= argument pointer (str.w r0, [sp, #152]), result inr0r9= globals-table base =0x20010100, set by the reset handler — so the export cannot be called before boot has run0x20000100) → setr9→ init globals →blxfirst export → spin at0x16c0x2280→ ARM0x20002380The blocker: after
RunForreaches the spin, settingcpu PCto the export entry and resuming does not execute — PC stays at0x7a4,r0unchanged, with and without the thumb bit. That's Renode CPU-resume plumbing, not falcon or lowering.Next attempt: drive the call from inside the image via a small harness export that calls
tickwith a fixed pointer and stores the result at a known address — no PC redirect needed, and closer to how the on-target test will have to work anyway.The attempt file is kept rather than deleted, so the next run starts from the established facts instead of rediscovering them.
rivet validate→ PASS.🤖 Generated with Claude Code