chore(release): v0.52.0 — enforce what we promise (7-lane hub: #865 #846 #869 #242 #871 #848 #867) - #878
Merged
Conversation
…FIED) Salvaged from the L7 agent that stalled mid-stream (226 tool-uses, no commit). 276 lines in liveness.rs. NOT verified — does not necessarily build/pass gates. A fresh agent re-verifies from scratch (build, VCR-RA-003 clean, cf_shapes_500:: ifelse accepted, ra003 clobber rejected, differential green) before this is trusted. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…rd_bv panic + hold 0.x-minor bumps main did NOT COMPILE (3x E0004). Dependabot auto-merged ordeal 0.9.1 -> 0.16.1 (#864) with NO CI RUN, and the four `BvTerm::Urem` match arms — removed when we downgraded to 0.9.1 (4ad175e), since that version lacks the variant — were never restored. 1. Restore the arms: term.rs (bv_rank, canonicalize_bv rebuild, SMT-LIB bvurem formatter) + the z3-solver-gated solver.rs (bv_to_z3 bvurem). 2. FIX A LATENT PANIC found while restoring them: bv_rank gave `Udiv` and `Urem` BOTH rank 5, but `ord_bv` asserts (via `unreachable!`) that rank-equal variants are exhaustively matched — and there is no (Udiv, Urem) cross pair, so comparing a Udiv against a Urem PANICS. Reachable: the rem model is `rem = a - (a/b)*b`, so div and rem terms meet under a commutative op. Urem now has its own rank (6, shifting And..Ite up one) and the `(Urem, Urem)` pair is matched. 3. KEEP the 0.16.1 bump — it is CORRECT: verified the full synth-verify suite runs 236 tests / 0 failed / ~33s (vs ~41s on 0.9.1). ordeal 0.16.1 fixes the unsigned-bvurem blast regression (ordeal#101) that 0.16.0 still had, so the =0.9.1 pin is no longer needed. This UNBLOCKS #848/#849. 4. CLOSE THE DEPENDABOT GAP (it has now bitten twice on this same dep): a 0.x MINOR bump is BREAKING by convention (for 0.x the minor is the de-facto major) but Dependabot labels it `semver-minor`, so the auto-merge workflow let it through. dependabot-auto-merge.yml now HOLDS 0.x-minor bumps (label + explanatory comment). Version strings are passed via env, never interpolated into the script body (pull_request_target + contents:write). Verified: build clean, synth-verify 236/236 green in ~33s, fmt + clippy clean, workflow YAML parses. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
#849) The #849 incident (4-6 h CI hangs, every run for three days) happened because there was NO wall-clock floor anywhere in the solver stack: the conflict budget does not map to time, and the div/rem trap VCs did not even go through the budgeted seam — `crate::trap` called `ordeal::trap::prove_trap_*`, which delegates to the UNBOUNDED `Solver::prove_valid`. Wire `Solver::check_with_deadline` (ordeal >=0.15) into BOTH seams: - `solver::OrdealSolver::check` now bounds by wall clock (default 15 s, `SYNTH_ORDEAL_DEADLINE_MS`; 0 disables and falls back to the existing `SYNTH_ORDEAL_MAX_CONFLICTS` conflict cap — ordeal's `Bound` is one-of, so a query carries a deadline OR a conflict cap, never both). - `trap::prove_trap_{equivalence,condition_equivalence}` now build the goal term themselves (`ot::trap_equivalence_vc` / `ot::trap_condition_equivalence`) and discharge it through the same bounded validity-as-UNSAT encoding, so the hardest VC class in the validator finally has a floor. - the Z3 differential oracle gets the identical budget via the `timeout` param — the "Z3 Verification" job hung on the same queries. Expiry degrades to `Unknown`, which every caller already treats conservatively (`ValidationResult::Unknown` / `TrapVerdict::Unknown`) — an undecided query is NEVER reported as `Verified`/`Preserved`. The certificate re-check and model self-check are untouched, so the bound costs completeness only, never soundness. DOCUMENTED LIMITATION (in the code): `check_with_deadline` bounds the SAT SEARCH, not bit-blasting/canonicalization. A query whose blast alone is pathological can still exceed the budget before the clock is consulted. This is a strong bound on the dominant cost, not a universal wall-clock guard. Refs #848, #849. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ks, enforce-by-default, hard-error mask/mpu The v0.51.0 aarch64 lowering (#851) emitted NO bounds check and --safety-bounds was a silent no-op (all four modes byte-identical): a zero-extended (uxtw) guest address reached up to x28 + 4GiB-1, an OOB read/arbitrary-write primitive where WASM requires a trap. - selector: new explicit MemBounds mode. Software emits, per access, 'mov w_k,#K; cmp w_addr,w_k; b.ls +2; brk #0' with K = limit - memarg.offset - access_size (compile-time), proving uxtw(addr)+offset+size <= limit BEFORE the dereference; K<0 (offset +size exceed the limit) emits an unconditional brk. Sound statically: memory.grow is not lowered on this backend, so the declared minimum IS the runtime size. - CLI: -b aarch64 DEFAULT is now software (enforce, don't hope); 'none' is the explicit unchecked opt-out (byte-identical to v0.51.0 output); mask/mpu HARD-ERROR (never silently accepted again). The backend re-checks (defense in depth) for non-CLI drivers. - single-function path now threads the module's declared memory-0 minimum (aarch64-scoped; ARM/RV32 configs unchanged) and records it in the safety manifest. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…819 redo) The numeric (optimized-path) join CFG seeds entry availability with the PRESERVED callee-saved set — pushed-in-prologue AND popped-at-every-exit — fixing the #819 false JoinValueNotAvailable{R8} hard-error on valid code (cf_shapes_500::ifelse dead result-mov of a void function) WITHOUT touching the label path's strict semantics (label red-first clobber tests keep their teeth). Not merely-entry-live: the seed is anchored to the save/restore contract and is empty on push-less functions, so garbage reads of never-established registers stay Violations. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…loses #848) Reverts db0f1f2 (the #849 un-hang revert). ordeal 0.16.1 fixes BOTH blast regressions the revert was forced by — signed `bvsrem` (ordeal#97) and unsigned `bvurem` (ordeal#101) — and the previous commit puts a per-query wall-clock deadline under every solve, so a future solver cliff degrades to `Unknown` instead of hanging CI for six hours. `ArmSemantics` `I64RemU`/`I64RemS` compose the 64-bit operands from their register halves (`concat`), apply the native `bvurem`/`bvsrem`, and split the result back to the rd pair; the divide-by-zero trap is reconstructed from the pseudo-op's `elide_zero_guard` field. `verify_i64_rem_value_preservation` asserts the FULL obligation (trap clause AND guarded value clause) against the ABI pair R0:R1, so the value model is load-bearing rather than decorative. MEASURED on 0.16.1 with the model live: the four i64-rem tests (8 x 64-bit bvurem/bvsrem VCs) decide in 2.42 s serial. Under the reverted #844 the same tests never terminated. Non-vacuity is gated, not narrated: `i64_rem_wrong_destination_register_is_rejected` (rd = R2:R3 instead of the ABI R0:R1 -> Invalid) and `i64_rem_value_model_closes_a_trap_only_gap` (the OLD trap-only VC ACCEPTS the same wrong-destination lowering; the new value VC REJECTS it) pin the exact accepted-under-havoc -> rejected-now discriminator. Verify-only: no codegen path touched, frozen anchors untouched by construction. Closes #848. Supersedes #854. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
RED: never-established callee-saved read at a numeric join (with prologue, R6 outside the push set) + push-less contract-empty seed; GREEN: the preserved one-arm-redef ifelse class (red-first-inverted), both-paths-define, dominator-defined, loop back-edge universe-init; DECLINE: off-boundary target + mixed label/numeric stream. Existing label ra003 clobber tests untouched and still red-catching (26/26 ra003 green). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…+ mode-difference gate RED on the pre-fix binary (15 failures: OOB reads return the poison sentinel / unmapped faults, all four --safety-bounds md5s identical); GREEN after: every OOB row brk-traps exactly where wasmtime traps, md5(none) != md5(software), default == software, mask/mpu hard-error. Trap classification is strict (only brk/UC_ERR_EXCEPTION counts) so the -1 row can never pass vacuously via an unmapped fault. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Neither job had a `timeout-minutes`, which is why the #849 solver cliff burned 4-6 h per run for three days instead of failing fast. The per-query deadline (#848) is the inner floor; these are the outer one. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ttern B Lt32Facts: forward MUST-dataflow of 'provably < 32 unsigned' register facts over the exact label-form CFG (intersection meet at joins, worklist fixpoint, unmodeled control flow declines the whole analysis, unmodeled register effects kill all facts). elide_shift_masks consults it when the intra-block window cannot see the masking def — a mask is elided only when EVERY path reaching the shift carries a bounding last-def of the amount register (the #682 invariant in dataflow form). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…anism gate 15 s was too tight: it cut off a PRE-EXISTING legitimate query. Measured on a dev host (debug, ordeal 0.16.1), the expansion_validator popcnt-HAKMEM link-1 equivalence needs 40.6 s to decide — it is genuinely hard, not a cliff — and a 15 s budget degraded it to Unknown, turning a real proof into a spurious non-answer. The re-landed 64-bit bvurem/bvsrem i64-rem VCs, by contrast, take 2.4 s for all four tests. 300 s is ~7x the measured pacer (headroom for a slower, parallel-loaded CI runner) while still turning a solver cliff from 6 hours into 5 minutes; the outer CI timeout-minutes bounds the aggregate. Adds solver::tests::deadline_degrades_to_unknown_never_to_proven: a 1 ms budget on a hard query must yield Unknown and MUST NOT yield Unsat (which every caller reads as proven), with the same query at deadline-disabled deciding Unsat so the gate is not vacuous. Plus default_deadline_decides_the_corpus (the shipped budget must not starve ordinary queries). Also writes the [Unreleased] CHANGELOG entries for both halves of the lane. Refs #848, #849. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…mpted comment Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The first cut re-proved the SAME hard instance unbounded as its non-vacuity control. Measured: negated mul-associativity runs >30 s unbounded at width 32, 16 AND 8 — it would have dominated the suite. Split the two legs instead: - bounded leg: width 8 at 1 ms -> must be Unknown, must NOT be Unsat, and the reason must NAME the deadline (a non-answer has to say why); - control: the SAME construction at width 3 -> Unsat in milliseconds. Associativity is an identity at every width, so the only way this gate could go vacuous is a coding error in the goal builder — which is exactly what the narrow control rules out. Re-proving the width-8 instance would cost >30 s for no extra information. Whole solver::tests module: 5 passed, 0.02 s. Refs #848, #849. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ing, always-trap, opt-out byte-identity) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…GELOG [Unreleased] entry Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…(selector doc + mem_851 gate docstring) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The trap-preservation gate does NOT go through `solver::new_solver`, so SYNTH_SOLVER_DIFF never cross-checks the div/rem VCs against Z3. That means the CI "Z3 Verification" job hung in #849 because it runs the same ORDEAL tests, not because Z3 was slow on them — the z3 `timeout` param this PR adds is defence in depth for the value-VC path that does use the oracle, not a fix for the observed hang. Say so in trap.rs and the CHANGELOG rather than letting the table imply coverage that does not exist. Routing trap VCs through the differential seam is a named follow-up. Refs #848, #849. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
clippy -D warnings (needless_borrows_for_generic_args) on the new mul_assoc_goal helper. Workspace clippy --all-targets now clean. Refs #848. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…conflicts) Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…erified) Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…irst) Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… reaching-def The decisive class the brief flags as the #682 silent-miscompile vector: a bounding `and rK,#c` that a linear/last-def scan would accept but that does NOT dominate the shift. - branched-over def (`b S ; and r3,r0,#15 ; S: mask+shift`) — the same three ops as the ELIDING cross-block test, merely permuted, and the verdict flips 0 vs 1: proof the analysis is flow-sensitive, not textual. - conditionally-skipped def (the taken Bcc edge bypasses the mask). - join whose other arm never touches rK at all (raw param, no unbounded def for a def-scan to trip over). All three keep the mask; all 11 elide_846 tests green. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… ops)
- decode-un-drop F32ConvertI64S/U, F64ConvertI64S/U, I64TruncF64S/U; add the
missing WasmOp variants I64TruncF32S/U
- f64.convert_i64_{s,u}: exact two-word build (VCVT hi/lo + 2^32 scale + one
correctly-rounding VADD)
- f32.convert_i64_{s,u}: same build + Fast2Sum residual + branch-free
round-to-odd fixup + single VCVT.F32.F64 demote (double-rounding-exact)
- i64.trunc_f32/f64_{s,u}: #709-class i64 domain guard (TRAP on
NaN/out-of-range, WASM 4.3.3) before the #782 word-decompose
- DP capability gate: all f64-machinery members (incl. the pre-existing
i64.trunc_sat_f32 pair, latent m4f hole) listed in is_scope_f64_op ->
single-precision targets loud-decline instead of emitting UNDEFINED
VCVT.F64 encodings
- select_default keeps register-blind honest declines by name
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… the destination The shipped non-vacuity gate proves the DESTINATION field is load-bearing (rem into R2:R3 instead of the ABI R0:R1 -> Invalid). That leaves a strictly stronger class unpinned: a lowering that writes the RIGHT registers and preserves the ÷0 trap but computes the WRONG remainder. i64_rem_wrong_signedness_is_rejected closes it — rem_u lowered to the signed pseudo-op (and rem_s to the unsigned one), correct ABI destination, correct trap. Only a real bvurem/bvsrem value model can see the difference, and it does: both directions come back Invalid with the expected counterexamples (negative dividend for rem_u-as-rem_s, negative divisor for rem_s-as-rem_u). Under the HAVOC model both sides were unconstrained ⟹ Verified. Cost: the SAT search is ~23 s locally (12× under the 300 s deadline) but FREE in suite wall-clock — it runs behind the pre-existing 40 s popcnt-HAKMEM proof, which remains the long pole (lib suite 36.2 s, unchanged). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…g killers+fuzz) vs wasmtime; realloc-sound Adds/Adc fixup The round-to-odd fixup's 64-bit increment is emitted as MODELED Adds/Adc instead of the I64Add pseudo-op: reg_effect=None ops are range-realloc segment barriers whose register READS are invisible to the segment-local liveness, so the colorer reused slo/shi for intermediates and the pair reaching the final VMOV was garbage (caught by this differential at land time; the segment validator shares the last-use assumption and accepted the wrong rewrite — filed as a follow-up allocator issue). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…t-arity call lowering (WIP) - elf_builder: external Call emits the canonical 8-byte auipc/jalr placeholder + R_RISCV_CALL_PLT reloc; .rela.text + undefined symbols (reloc-free objects byte-identical) - backend: CompiledFunction.relocations populated (RelocKind::RiscvCallPlt); compile_module maps synth_func_N -> import field name / local symbol - CLI: build_multi_func_riscv_elf threads relocs + import names; the single-function riscv path loud-declines instead of dropping relocs - selector: exact-arity call lowering from func_arg_counts (survivors preserved in callee-saved regs), void callees push nothing (func_result_counts), call results copied out of a0/a1 - fixture + 5-stage differential (read-back, ARM parity, real link, unicorn vs wasmtime execution) Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…coverage + feature-matrix row Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…harness hardening The preservation mv is path-local but the vstack rewrite is shared — inside a control frame another path could reach the consumer without the mv (path-dependent miscompile). Decline loudly for that shape. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ext walk, reloc-free byte-layout pin Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
#682 unsound size Measured on gale's real 656 B loom.wasm with a freshly built binary: 534 B / 10 masks (opt-out) -> 502 B / 3 masks (default), 75/75 mmio traces bit-identical vs wasmtime incl. pin >= 32. Read the 3 residual masks off the shipped object rather than guessing: one (mode<<2 on a frame-reloaded raw param) is PERMANENTLY load-bearing, two are the CRL/CRH relational idiom. Each is a 4-byte and.w and 502 - 3*4 = 490 exactly, so gale's 0.11.50 baseline had no mask at those sites at all -- 490 B is the size of the pre-#682 unsound lowering, not a target to chase. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
… CI wiring + CHANGELOG - synth-synthesis/tests/i64_float_conv_869.rs: m7dp lowers all 8 (converts guard-free, truncs exactly 2 UDFs), trunc_sat twins stay guard-free, Adds/Adc (not I64Add) pinned, m4f/m3 loud-decline by name - cross_backend_op_parity: new variants placed StructurallyExcluded(FLOAT) - trap.rs trunc_op maps I64TruncF32S/U; wasm_semantics 64-bit-typed arms; is_trap_gated_op comment names the symbolic-wiring residual (#756-class, execution-gated by the #869 differential meanwhile) - ci.yml: i64<->float family oracle wired into the ARM oracle job - allocator segment-liveness hazard filed as #872 Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…d, probe Homebrew LLVM first Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…mbolic trap-VC wiring stays the named residual Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
A body containing a call clobbers RA; without a prologue save the ret returns into the function's own call site forever. Invisible pre-#871 because call-containing RV32 functions never emitted. preserve_callee_saved now saves/restores RA for call-containing bodies, and VCR-RA-003 REQUIRES it (unsaved-RA nonleaf = CalleeSavedNotSaved violation, red-first test). Full #871 differential now 5/5: read-back + ARM parity + real ld.lld link + 16 unicorn-vs-wasmtime execution cases bit-identical. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Both loops index instrs only; iterate the slice directly. Pure refactor -- the gpio differential is re-run below on the rebuilt binary to confirm the 502 B / 3-mask result and the 75 mmio traces are unchanged. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…clippy unused-mut Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ect's reachability Coordinator question: was the missing non-leaf RA save reachable on shipped v0.51.0 via local calls? Answered from a main-built binary: NO. Every RV32 call shape (imported / local / self-recursive, with and without --relocatable, and the single-function --func-name path) declined with 'unsupported in skeleton: external call without relocation table'; Backend::compile_module has no caller, so every function was assembled alone and no Call label ever resolved. The RA defect was introduced and fixed within this lane. Completeness: local calls are ALSO newly emitted here, so - validator coverage pinned across call labels (synth_func_N / func_N / import) — the RA requirement is call-shape-agnostic; - the fixture gains a local-call export (reloc against a DEFINED symbol, nm -u must stay imports-only); - stage4 now resolves each patched target to a SYMBOL START (a wrong-offset or wrong-function reloc fails) and asserts the local call lands on a synth-defined function, not a stub. Differential 5/5: 8 relocs, 20 execution cases. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…nv-869 # Conflicts: # CHANGELOG.md
…l-reloc-871 # Conflicts: # CHANGELOG.md
…oins-242 # Conflicts: # CHANGELOG.md
…LOG headline Assembles the 7-lane v0.52 hub onto release/v0.52.0: L1 #865 aarch64 bounds-check + --safety-bounds enforcement (was a silent no-op) L2 #846 cross-block reaching-def shift-mask elision (gpio-thin) L3 #869 ARM 64-bit int<->float family (8 ops, trap-guarded, + the #756 gap) L4 #242/#819 VCR-RA-003 across-join enforcement (the acceptance-oracle core) L5 #871 RISC-V external-call relocations (R_RISCV_CALL_PLT) + the RA fix L6 #848 native i64 rem re-land behind a per-query solver deadline L7 #867 ISA-model adequacy — counted trusted base + uncovered complement All seven lane branches merged; every conflict was an additive CHANGELOG [Unreleased] collision, resolved keeping BOTH sides (the shared hot files — liveness.rs, main.rs, trap.rs — auto-merged). Duplicate ### Fixed sections from the merge consolidated into canonical Added/Changed/Fixed order. - Version 0.51.0 -> 0.52.0 (all path-dep pins + MODULE.bazel + npm + status.json). - Generated docs regenerated ONCE at assembly (--emit-status), per the #805 rule that lanes must not hand-edit them: claim_check 26/26, model-coverage freshness gate passes. - CHANGELOG [0.52.0] headline written. Combined-tree verification follows in the next commits (build + every lane's differential on the merged binary — individual lane greens do not prove a merge). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Both loops index instrs only; iterate the slice directly. Pure refactor -- the gpio differential is re-run below on the rebuilt binary to confirm the 502 B / 3-mask result and the 75 mmio traces are unchanged. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…s-846 # Conflicts: # CHANGELOG.md
L2 pushed a clippy style fix + a main-merge AFTER the initial assembly merge. Caught by re-verifying lane containment (ancestry) rather than assuming the earlier merge was final.
Codecov Report❌ Patch coverage is 📢 Thoughts on this report? Let us know! |
…tale the aarch64 FEATURE_MATRIX row Cold review (fresh context, commit 3c184fc) returned NOT-SAFE-TO-TAG on two mechanical defects; every functional/soundness/oracle claim passed, including its own independent re-proofs (built a v0.51.0 binary and confirmed the #865 bounds oracle FAILS there with 15 failures; mutated preserved_callee_saved and confirmed exactly 2 join tests fail; disassembled gpio_configure to verify the 502 - 3x4 = 490 arithmetic published on #846). 1. Cargo.lock was STALE at 0.51.0 while every manifest read 0.52.0. The v0.51.0 tag DID commit a bumped lock, so this broke release precedent and any "--locked" / reproducible build of the tagged tree. CI cannot catch it: no job builds with "--locked". Regenerated via "cargo update -w --offline": 18 synth-* pins 0.51.0 -> 0.52.0, zero dependency drift. 2. docs/status/FEATURE_MATRIX.md described a SHIPPED feature as unsupported -- the exact class the v0.51 cold review caught. The aarch64 row still called linear-memory OOB-trap a "follow-on" when #865 shipped it as the enforcing DEFAULT in this very release. Note the staleness gate structurally CANNOT catch this: it compares doc against render, so a stale TEMPLATE renders "correctly". Fixed the template row (bounds-checked by default; --safety-bounds selects the strategy; mask/mpu hard-error) and re-emitted. Verified: claim_check 26/26, model-coverage freshness green, no lingering 0.51.0 in any pin surface. Byte-invisible to codegen. Known follow-up (pre-existing, filed separately): the gpio_thin_846 differential is not wired into CI, so the #846 headline is not CI-enforced. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
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.
v0.52.0 — "Enforce what we promise"
Assembles the 7-lane v0.52 hub. Every backend in this release stopped over-promising somewhere, and each gap was closed by executing the fix rather than inspecting it.
--safety-boundswas a silent no-op (all 4 modes byte-identical, 4 GiB OOB read/write where wasmtime traps). Default enforces;mask/mpuhard-errorR_RISCV_CALL_PLT) — seam-importing drivers lower instead of decliningrem_u/rem_sre-landed behind a per-query wall-clock deadlineVerified on the MERGED binary (not per-lane greens)
Four lanes edited the same files, so lane-level greens don't prove the merge:
cargo test --workspace128 suites / 2527 tests / 0 failures · fmt clean · claim_check 26/26 · model-coverage freshness gate greenFound by the oracles themselves, mid-flight
ra— caught by the execution stage after byte, relocation and link checks were all green. Not user-reachable before this release (verified across five call shapes against a v0.51.0 binary).Honest residuals
gpio-thin stops at 502 B (490 requires re-introducing the #682 miscompile; 498 needs relational ranges). aarch64
mask/mpuhard-error rather than being implemented. ARM single-precision targets loud-decline the #869 family by name.🤖 Generated with Claude Code