diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index c67b9e2..f9307f8 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1244,7 +1244,14 @@ artifacts: jess CONSEQUENCE: the msgq is the VERIFIED inter-core IPC carrier for the NavState crossing (REQ-PIX-007 / TEST-PIX-030) - jess's current oracle uses a hand-rolled SHMEM flag handshake; the next rung grounds it on gale's k_msgq (over the shmem vring + the MU doorbell already in - rt1176-dualcore.repl), closing gale#65's gust ipc-rx on jess's side. The gust:os seam + + rt1176-dualcore.repl), closing gale#65's gust ipc-rx on jess's side. WHAT JESS NEEDS TO CONSUME + k_msgq (found 2026-07-24, RECORD not file - jess is float-gated, not ready-to-bind): the + gale-wasm-msgq-v0.4.0-cortex-m4f.o has 9 UNDEFINED scheduler-seam symbols (gale_w_msgq_pend / + ready_thread / reschedule / thread_swap_data / unpend_first_thread / spin_lock/unlock / + arch_thread_return_value_set / memcpy) - the gale kernel, which the v0.4.0 release does NOT + ship as standalone linkable objects. So to LINK+RUN k_msgq jess needs gale to also expose the + kernel-seam .o (or jess links the fused gale-nano core that already contains it) - the concrete + gale ask to FILE when jess can bind. The gust:os seam + executor are the gale-nano substrate for REQ-PIX-002 (M7 native base) / REQ-PIX-009 (F100). TRACK DISCIPLINE (do NOT treat proposed-as-delivered): the above are on gale's CUT v0.4.0 FUNCTIONAL line (SHA-verified assets on the release). gale's SAFETY line is a SEPARATE diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index d63c136..962eaee 100644 --- a/artifacts/findings.yaml +++ b/artifacts/findings.yaml @@ -1227,6 +1227,12 @@ artifacts: codegen-affecting flight change or synth moves. Also handed synth a minimal #345 repro (large fn -> literal pool >4095 B from the ldr; a function-SIZE effect, not global-count) on synth#782 for the falcon-skip-to-zero lane; 2 concrete fixes offered (movw/movt pair, or constant-island pool flush). + UPDATE 2026-07-24 (synth v0.50.0, falcon-v1.127): 14 -> 13 skips. v0.50 is mostly deps + verified- + codegen infra (VCR-WASM-001 i64 add/sub/mul/and/or/xor exec wiring; RV32 RA validator) - NOT + falcon-lane float fixes; the incidental -1 is likely an i64 op cleared by the i64-exec wiring. + run-stabilization still lowers. #345 (my minimal repro) NOT yet actioned (3x #345 remain); no new + pole. Remaining 13 = 3x #345 literal-pool + 2x #503 + #518 + VFP-f32-exhaustion + VCR-RA-003 + + no-free-callee + i64-spill + #331. Progression 26->16->14->13. Gate STILL OPEN (13>0). tags: [release-watch, synth, arm, hard-float, gi-fpu, trunc-sat, on-target, falcon, blocking] fields: detected-by: jess release-watch chain-measure on synth v0.45.1 (meld v0.41.1, falcon-flight-v1.123); real-fused-core 26/156 skips vs the "#369 closed" claim; confirmed trunc_sat minimal repro; filed synth#782 diff --git a/artifacts/phase2-pixhawk.yaml b/artifacts/phase2-pixhawk.yaml index 2820880..122c164 100644 --- a/artifacts/phase2-pixhawk.yaml +++ b/artifacts/phase2-pixhawk.yaml @@ -190,7 +190,7 @@ artifacts: - id: REQ-PIX-007 type: requirement title: Inter-core/inter-component comms - WIT-typed contracts, fused same-core / RPC cross-core over a shared-memory transport - status: draft + status: implemented release: v0.7.0 description: > Same-core components are meld-fused (WIT seams -> direct calls); cross-core (M4<->M7, @@ -217,10 +217,22 @@ artifacts: estimator(M4)->falcon(M7) crossing datum is NavState = the IEKF state {q, v, p, b_g, b_a} = 16x f32 = 64 bytes - a single fixed-size MU/SHMEM message (the `vehicle-state` in the spar-generated estimator/falcon.wit). relay-iekf is a separable no_std crate with no hidden - back-edges, so this is the whole inter-core estimator contract; the byte payload (list) - will gain this structure as the AADL feature types refine. falcon(M7)->failsafe(F100) carries + back-edges, so this is the whole inter-core estimator contract. falcon(M7)->failsafe(F100) carries the per-motor actuator commands (byte-exact pass-through, REQ-PIX-004 PART-P02). - category: functional + STATUS draft->IMPLEMENTED 2026-07-24: both halves of the requirement now have green CI-gated + evidence. (1) WIT-TYPED CONTRACTS - the AADL data types are now STRUCTURED (VehicleState.nav = + record of 16 f32; ActuatorCmd.pwm = record of 4 f32), spar codegen emits `record vehicle-state-nav` + / `record actuator-cmd-pwm` (not opaque list), gated by TEST-PIX-023 (the "will gain structure" + note above is DONE; AFD-036 resolved). (2) RPC CROSS-CORE over the shared-SRAM transport - the 16xf32 + NavState crosses M4->SHMEM->M7 BYTE-EXACT on the dual-core RT1176 Renode model, gated by TEST-PIX-030. + Fused same-core (meld -> direct calls) is exercised by the scry gate on the fused core. REMAINING TO + `verified`: ground the transport on gale's VERIFIED k_msgq (gale v0.4.0 gale-wasm-msgq, DD-023) + instead of the current hand-rolled SHMEM flag handshake - BLOCKED this tick: the msgq .o needs the + gale scheduler seam (gale_w_msgq_pend/ready_thread/reschedule/thread_swap_data/unpend_first_thread/ + spin_lock/memcpy = 9 undefined syms) which the v0.4.0 release does NOT ship as standalone objects. + RECORD (not file, per DD-022/023 sequencing - jess is #369/float-gated, not ready-to-bind): to + consume k_msgq jess needs gale to also expose the kernel-seam objects (or link the fused gale-nano + core); tracked on the DD-023 GALE row + gale#65. category: functional priority: should links: - type: traces-to