coord: DD-026 — relay→jess flight-component consumption contract (jess#167) - #168
Merged
Conversation
…ss#167 position) relay opened jess#167 asking jess to pin the consumption contract for how it integrates relay's flight components (WASM on all 3 cores) before relay mints interfaces. DD-026 records jess's POSITION (status: proposed, pending relay's falcon-rate worked example): 1. GRANULARITY: relay delivers fine-grained Level-1 verified stream components as cosign OCI + a placement manifest; JESS owns per-core meld_fuse + lowering (loom->synth per-ISA->gale) + the flashable-set attestation. Not pre-fused bundles (DD-018 + jess signs its own fused output, TEST-PIX-026/029). 2. SEAM SHAPE: synchronous step(sensor-sample)->actuator-cmd at the ARINC-653 partition window (DD-025 outer, WCET-bounded); relay keeps stream<T> for Level-1 intra-bundle composition (inner kiln-async). 3. SEAM TYPES: spar-generated from jess's AADL, 1:1 with the HAL seams — already realized (ActuatorCmd.pwm / VehicleState.nav, REQ-PIX-007/TEST-PIX-023). 4. F100 FAILSAFE: maximal-wasm on M3 (TEST-PIX-028) with gale's VERIFIED HM FSM (VER-OS-HM-001, v0.5.0) as the mechanism — not a parallel relay-fsafe. 5. DELIVERY: OCI-per-component; jess's V-gates (scry/witness/repro/sigil) run on jess's fused set. Endorsed relay's falcon-rate worked example. Stated the sequencing honesty: the M7 cascade can't lower yet (float gate, AFD-035); the F100/M3 path is the green-today validation target. Replied on jess#167 with the full position. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… OCI (gale#223), aligning with relay's falcon-flight Per the consumption contract's OCI-per-component delivery: gale ships release-tarball .o/.wasm (not OCI) while relay went to ghcr-OCI, so jess's per-core meld-fuse would pull from two paths. Filed gale#223 asking gale to publish its verified consumable components (HM/failsafe FSM, gust:os, sync primitives, the fused gale-nano subset) as cosign-signed OCI wasm components - uniform acquisition + sidesteps the standalone-.o unshipped-scheduler-seam problem. RECORD (float-gated), aligned now while the contract shape is fresh. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…CI component (residual host = gust:hal), v0.6 cut gale maintainer agreed on gale#223. Updated the DD-026 delivery decision: - Artifact shapes pinned: v0.5.0 msgq .o = self-contained decision fragment (0 undef); .wasm = core module with the 9-symbol scheduler seam. Neither is the consumable unit (corrects my earlier '.o needs 9 symbols' imprecision). - Resolution: gale delivers a cosign OCI wasm COMPONENT = the fused gale-nano subset (msgq/mutex/sem + gust:os + executor) resolving the scheduler seam internally, residual host contract = gust:hal (DD-018 thin native seam) and stays that thin. jess's per-core meld_fuse pulls relay Level-1 + gale's fused component (both OCI). Cross-linked DD-026 <-> gale's forthcoming DD; tracked for gale v0.6. F100=VER-OS-HM-001 half already consistent. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…t gust:hal); three WIT layers Corrected per the gale component-model architecture: the app<->runtime COMPOSITION seam is gust:os (gale's typed capability world = 'the OS surface an app sees'), which relay's flight imports and gale's OCI component exports. gust:hal is the deeper NATIVE residual (mmio, jess- provided), not the composition seam. Three WIT layers, each owned right: (i) gust:os = capability abstraction (gale) - the composition seam (ii) data seams (sensor-sample/actuator-cmd/NavState) = app<->app (jess-AADL, REQ-PIX-007) (iii) gust:hal = native mmio residual (jess) Scheduler primitives live BELOW gust:os (resolved by the composed executor), never exposed. gale delivers the gust:os PROVIDERS as the OCI component; jess composes flight+providers along gust:os -> residual gust:hal. Refined on gale#223. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… integrator owns seam, loop-complete closed-loop-proof)
relay settled on jess#167: option (a) + two principles jess accepted.
P1: integrator (jess) owns the cross-core seam + width + airframe binding; relay stays
airframe/target-agnostic (ActuatorCmd.pwm=4xf32 is jess's X500-V2/quad specialization;
hex = jess seam-width + manifest change, relay mixer parameterized underneath). Confirms
decision 3.
P2: loop-complete minimality (smallest seam that closes the loop) + every relay component
ships a closed-loop proof (not a step stub). Proof division: relay proves loop-closes-
in-source (SIL); jess proves loop-survives-lowering (SIL-vs-Renode differential) = jess's
on-target value-add; stacks to the full V per stage. Bonus: falcon-rate as its own OCI
entity gives jess the per-stage skip inventory -> a falcon-skip-to-zero priority signal.
DD-026 stays 'proposed' until falcon-rate validates the seam end-to-end (relay building it).
Replied on jess#167. rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…le#225) + build target gale#224 (v0.6) gale landed its mirror decision with the gust:os correction baked in: DD-OS-DELIVERY-001 (gale#225, rivet PASS) - the consumable cut is a cosign OCI component EXPORTING gust:os, scheduler resolved below it, residual = gust:hal. Build target gale#224 (the fused gale-nano component) bound to v0.6, acceptance invariant = wasm-tools confirms a component exporting gust:os + after wac plug/meld/loom/synth the only undefined syms are the gust:hal mmio seam (no scheduler/heap leak). Already demonstrated at the tl/ts node level (VER-OS-SYSCALL-001). DD-026 <-> DD-OS-DELIVERY-001 cross-linked; consumption contract bilaterally pinned across relay/jess/gale. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ers shrink jess-native to gust:hal (the DD-026 driver half) gale v0.5.0's verified + silicon-validated thin-seam driver suite (spi/i2c/adc/can/pwm/gpio/ wdg over gust:hal) refines the DD-015 driver seam: the bus TRANSPORT that DD-015 put in jess's native host moves DOWN into gale-verified wasm, shrinking jess's native TCB to just gust:hal. New layering: gust:hal[jess] -> gale verified thin-seam bus driver -> relay protocol/decode/ voting -> sensor-sample[jess AADL] -> relay flight app. Open reconciliation (raised on jess#167): the gale-bus-driver <-> relay-protocol-driver boundary = the embedded-hal-async transport traits (gale implements, relay consumes) so the register bus is owned once; + gust-target-gen AADL vs jess's AADL needs one owner (jess). To pin in the DD-026 driver-path extension. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…+ M7 rate loop); NavState confirmed biases-not-rates relay found the cascade seams already exist (falcon:cascade@0.7.0) and asked jess (seam owner) to confirm the M4<->M7 data flow. Confirmed + added jess's side: - VehicleState.nav (16, biases + NO rates) is the canonical IEKF state; the rate loop takes the RAW gyro as a SEPARATE co-scheduled-on-M7 sample and bias-corrects it with NavState's gyro-bias (freshest inner-loop gyro, no cross-core/filter lag) - the standard PX4 fan-out. - Added ImuSample.raw (6xf32 = gyro3+accel3) to hardware/pixhawk6x-rt.aadl; spar emits `record imu-sample-raw` on both falcon.wit (rate loop) + estimator.wit (ekf) = the fan-out. WIT-derivation gate green (committed wit/ == spar codegen). - innovation stays OUT of the controller crossing (separate Health-Monitor signal, VER-OS-HM-001). - Recorded in DD-026. relay's one seam edit: rate re-feeds gyro from imu-sample, not vehicle-state. Verified: rivet validate PASS; spar parse+instance OK; WIT-derivation gate OK. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 23, 2026
…self-verify findings) (#169) Clean-room self-verify (2026-07-24) came back 5/7 CONFIRMED (WIT seams derive from AADL, rivet PASS, REQ-PIX-007 'implemented' + AFD-036 'resolved' both honest, DD-026 records match the real threads, CI gates non-bypassed). Two findings recorded on DD-026: - CAVEAT: the relay/jess/gale 'agreements' (jess#167, gale#223/#225) are all one maintainer (avrabe) across supplier hats - single-actor coordination, not independent sign-off. jess must keep validating claims against the REAL BUILD (per AFD-035), and the mechanical acceptance gates (gust:hal-residual check, falcon-rate consumption run, closed-loop-survives-lowering) are what make it real - not thread consensus. - MELD WATCH v0.42.0: ADR-7 multiply-instantiated + PIC linking, relevant to the per-core fuse; CI pinned v0.41.3; re-verify the reproducibility gate + multi-component fuse when un-floated. (The self-verify also flagged a CI-hygiene gap: #166/#168 main-branch push runs didn't complete - #166 concurrency-cancelled, #168 stuck queued - though both PR-branch runs were verified green before merge. This PR's merge re-triggers a fresh main run to close it.) 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
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.
relay opened jess#167 asking jess (the system-integration + on-target authority) to pin the consumption contract for how it integrates relay's flight components across the 3 cores, before relay mints interfaces the wrong shape. DD-026 records jess's position (status:
proposed, pending relay'sfalcon-rateworked example):meld_fuse+ lowering (loom→synth per-ISA→gale) + the flashable-set attestation. Not pre-fused bundles — DD-018 + jess signs its own fused output (TEST-PIX-026/029).step(sensor-sample) -> actuator-cmdat the ARINC-653 partition window (DD-025 outer, WCET-bounded); relay keepsstream<T>for Level-1 intra-bundle composition (inner kiln-async).ActuatorCmd.pwm/VehicleState.nav, REQ-PIX-007/TEST-PIX-023).relay-fsafe.Endorsed the
falcon-rateworked example; stated the sequencing honesty (M7 cascade is float-gated, AFD-035 — the F100/M3 path is the green-today validation target).Replied on jess#167 with the full position.
rivet validate→ PASS.🤖 Generated with Claude Code