diff --git a/CHANGELOG.md b/CHANGELOG.md index 621f05f5..27350472 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,7 +5,12 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [Unreleased] +## [0.60.0] - 2026-08-27 + +**Derive what you check against — and reach is part of correctness.** + +Two invariants, and the release spent most of its findings on the first one +turning out to apply to its own machinery. ### Added @@ -32,6 +37,184 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 wasmtime under unicorn with spec-exact domain-asserting builtin stubs, every trap row executed on both sides). +- **RQ-60-A64IMPORT (#1017, #1071): AArch64 import dispatch — imports become + `SHN_UNDEF` externals.** The top-ranked real-world blocker (~121 of 805 + modules, 88 of 101 components) was a module whose code calls an imported + function, or whose funcref table holds one: it loud-declined wholesale. + This is synth's own ARM `--relocatable` #173/#197 contract ported, not new + policy — a call to an import lowers through the same `bl` + `R_AARCH64_CALL26` + path as a local call, a table slot holding an import emits a `b ` + trampoline (`JUMP26`) against the import's wasm field name, and the + relocatable ELF builder gained a driver-supplied undefined-externals + ALLOWLIST emitting `STB_GLOBAL STT_FUNC SHN_UNDEF` symbols. A symbol neither + placed nor listed keeps the #1013 clean refusal, so a declined local callee + can never silently become a link-time external; an unnamed import still + declines (never fabricate a symbol). `ld.lld` links the objects against + assembled definitions and unicorn executes the linked images: `run(37) = 42` + through the import, table dispatch slot0 (import) 41 -> 42 and slot1 (local) + 21 -> 42. Import-free modules are byte-identical. + **The acceptance rate is UNMEASURED since this change** — the 805-module + corpus lives with the downstream consumer, the re-run is requested, and the + artifact's own rule ("a change that adds a code path without moving the + census has not delivered") is why this says so rather than implying the + 1.6% figure moved. + +- **RQ-60-VFPPRESSURE increment 2 (#1069): frame-homed overflow VFP locals — + the 13->14 homed-local wall falls.** (Increment 1's entry is already in + `[Unreleased]` and stays as written: the AEABI-routed i64<->f32 conversions + on single-precision FPU targets.) + Increment 2 adds frame-homed overflow f32/f64 locals as a LAST-RESORT retry + taken only after the #881 rung also failed, so every function that compiled + before is produced by exactly the same path (falcon `rate.o`/`mixer.o` + bit-identical main vs branch). Unlocks `attitude#tick`, `ekf#estimate` and + `position#tick` on cortex-m7dp — **5 of 5 falcon cascade stages**, the + issue's own definition of done. Verified downstream: the fused image builds + and EXECUTES on an RT1176 M7. + +- **RQ-60-WCETKEY (#1063): name-section names as durable WCET identities.** + `synth-wcet-v1` named functions from the export section only, so an internal + function was `func_` — an index silently retargets when an unrelated + edit adds or removes an earlier function. Names now come from the name + section with the v0 crate disambiguator stripped, and `--wcet-hints` keys are + symmetric with them. Measured downstream on a real `gust:os` composite: + **7 of 13 loop-declined functions were `func_` before; 0 after.** + An index key for a function that carries a name is REFUSED, and the refusal + names the key to use instead. + Increment 2 makes those refusals machine-readable: the sidecar gains a + top-level `hints` object present exactly when a hints file was passed, so a + consumer can distinguish (a) no hints, (b) hints consumed, (c) hints supplied + and ALL refused — three states that were previously two. Every key-resolution + diagnostic carries the same machine tag stderr names. Merits-level rejections + stay in per-function `hint_rejections` (the hint reached a verifier); key + diagnostics are top-level (it never did). `.text` is byte-identical across all + three states. + +- **RQ-60-CFOBLIG (#1057): the WASM model gains `BrIf`, and the proof inventory + is DERIVED rather than guessed from theorem names.** Increment 1 adds the + first control-flow constructor to `WasmInstructions.v` with executable + semantics and a kernel-checked correspondence obligation discharged against + the same `exec_program_br` executor as the #73 division trap guards. + Increment 2 answers a measurement dispute properly: a downstream consumer + derived theorem names from rule kinds by CamelCase->snake_case and reported + `brif_correct` as the tree's only deviation. Measured, it is the **29th + member of a class** — every signed/unsigned comparison, div, rem and shift + uses the fused spelling (`i32_divs_correct`, not `i32_div_s_correct`) — and + **19 `*_correct` names are declared in two different files with different + statements**, so a name-keyed matcher is wrong in both directions. So neither + side renames: `artifacts/proof-inventory.json` (`synth-proof-inventory-v1`) + is generated from the proof tree, with binding and strength decided + SEMANTICALLY (does the statement apply the constructor to `exec_wasm_instr` / + `compile_wasm_to_arm` and run the ARM executor?) and never from names. The + constructor universe is parsed from `WasmInstructions.v`. Freshness is + byte-compared in the required claim-check job and the manifest's Qed re-count + is pinned fields-equal to the ledger's independent derivation, so a hand-edit + reds both. **Corrected while doing this:** all 138 constructors are Qed-bound; + the honest frontier is 63 result-correspondence vs 75 existence-only, i.e. + STRENGTH rather than absence. + +### Fixed + +- **RQ-60-RACOST (#242): the allocator's cost model prices real encoder bytes, + and a final-byte arbiter makes no-growth a construction rather than a check.** + Increment 1 merges tied use/def webs so an rmw colour mismatch is + UNREPRESENTABLE rather than detected. Increment 2 replaces occurrence counts + with the real encoder's own byte lengths — and the measurement redirected the + design: the dominant regression had an essentially IDENTITY colouring and grew + +96 B because preserving the input assignment defeats a downstream + canonicalization that lets const-CSE collapse twelve `movw`/`movt` pairs. No + colour-time cost model at any fidelity can see a downstream-pass interaction, + so candidates are now sized through the real pipeline and shipped only when + strictly smaller — the no-growth property becomes a CONSTRUCTION rather than + a check, and future allocator work (splitting, coalescing) inherits it. + Measured **66 functions shrink, 0 grow**; that figure comes from the + comparison script, which declares itself `ci-status: manual (measurement)` + and deliberately carries no verdict. What IS CI-gated is the allocator's + CORRECTNESS — `vcr_dec_001_graph_alloc_differential` and + `vcr_dec_001_join_alloc_execution_differential` — not the size number. + +- **#1087: `claims.yaml` carried a duplicate `reason:` key, and the ledger + recorded a +622-line waiver with a +10-line justification.** YAML keeps the + last value on a duplicate key, silently, so the surviving justification for + RQ-60-VFPPRESSURE increment 1's growth of the instruction selector was + RQ-59-I64SHIFT's reason for a different change in a different release. + `check_ratchet` asks only whether a waiver exists at this value and whether + its reason is non-empty — neither question can tell the right reason from + someone else's. The ledger is now parsed duplicate-key-strict at both load + sites, with a diagnostic naming the DISCARDED value's line. The same strict + loader already guarded the release artifacts (#1059); it had simply never + been pointed at the file every other claim is checked against. + One number to read carefully afterwards: `selector_lines_code`'s waiver + count went **9 -> 10 with the value unchanged at 19,199**. That is the + signature of a destroyed record being RESTORED — the swallowed + RQ-59-I64SHIFT waiver getting its own `to: 18288` entry back — not of a + further growth being permitted. + +### Infrastructure — the release's own theme, applied to itself + +- **RQ-60-FLIPCOUPLE (#1064): a release status must agree with the evidence on + main.** `scripts/status_evidence_check.py` refuses a claiming status whose + declared evidence is absent, a non-claiming status whose evidence exists, a + release file contributing zero artifacts (the #1064 silent-skip shape), and an + id-named delivery commit nobody acknowledged. Seven-instance replay, 7/7. +- **RQ-60-ARTIFACTSPLIT (#1059): the single-file artifact write surface is + split, and the splice that motivated it is replayed as a fixture.** From + v0.61 each requirement gets its own file under `artifacts/release-vX.YY/` + with a comments-only `_release.yaml`, verified empirically to load on both + the CI-pinned rivet 0.23.0 and 0.32.0. Structural rules cover the flat files + that remain forever: every artifact must carry its own `links:` (the splice + that absorbed a sibling's trace links), ids must be unique across files, and + a per-requirement file contributing zero artifacts is red on its own. + +- **#1085: two artifacts pinned evidence that could not fail on the failure + they define.** `RQ-60-A64IMPORT`'s description says the acceptance number is + the deliverable; its `done-when` checked that a code path exists — which the + description explicitly says is *not* the deliverable. `RQ-60-CANARY`'s + claim is that every rule-emitted expansion is EXECUTED; its predicate named + a function in a source file, and would still have held with the gate + deleted. Both now pin the mechanism: CANARY pins the canary gate's own + non-vacuity floor (`emulations >= 1200`), proven sensitive — dropping that + floor to 0 turns the artifact red. Found by auditing all eight v0.60 + artifacts against the bar each description sets; three of eight had it. + +### Known and stated, not fixed + +- **The subtraction ratchet moved the wrong way this release** — and not on + one pin. Live, from `claim_check.py claims.yaml --metric` on `main`: + + metric now baseline delta direction + selector_lines_code 19199 17897 +1302 must FALL + selector_wildcard_arms_code 55 55 +0 must FALL + sel_dsl_rules 80 80 +0 must RISE + mirror_marker_files 60 57 +3 must FALL + mirror_obligation_files 24 23 +1 must FALL + + Three ceilings rose, the rule floor did not. Every step carries + a written waiver bound to its exact value, and the two largest are reach work + on targets that previously had NO lowering at all (VFPPRESSURE increments 1 + and 2, +622 and +289), where nothing could be deleted in exchange because + every existing path is byte-frozen. That is a defensible reason and it is + still the pattern the v0.58 correction exists to make visible: the verified + path did not grow this release and the hand-written one did. +- **The V is NOT closed on the right-hand side, and this release does not + claim it is (#1091).** `release-execution`'s traceability completeness gate + requires every `implemented` artifact to carry a `verifies` link to a + verification artifact. Measured: **60 of 60 release artifacts across + v0.56-v0.60 have none** — five consecutive releases, 100%. `rivet coverage` + does run inside the required Rivet Validation job, reports + `sys2-has-verification` at **61/152 (40.1%)**, and exits 0 regardless: it + prints, it does not assert. The verification itself EXISTS in every case + (unicorn differentials, `ld.lld`-linked execution, Rocq proofs, mutation- + killed gates); what is missing is the typed link that makes it queryable — + "invisible to the trace graph", not "unverified". Not a v0.60 blocker, + because the gap predates it by four releases and nothing about it is new; + stated here because a release that quietly assumed "traceability + completeness" would be claiming a gate that has never once fired. + +- **RQ-60-CANARY's code shipped in v0.59.0**, not here. The artifact sits in + v0.60's scope and closes its traceability here; the capability — the + pseudo-op expansion canary gate — was released in v0.59.0 and is credited in + that section. See #1085 for the gate that would have caught the mis-scope. + ## [0.59.0] - 2026-08-26 **The loud direction was covered, the silent one was not.** diff --git a/Cargo.lock b/Cargo.lock index 63911704..ea94738b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1111,14 +1111,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.59.0" +version = "0.60.0" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "synth-core", @@ -1127,7 +1127,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "synth-core", @@ -1138,7 +1138,7 @@ dependencies = [ [[package]] name = "synth-backend-aarch64" -version = "0.59.0" +version = "0.60.0" dependencies = [ "synth-core", "thiserror", @@ -1147,7 +1147,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "synth-core", @@ -1156,7 +1156,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "proptest", @@ -1169,7 +1169,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "synth-core", @@ -1178,11 +1178,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.59.0" +version = "0.60.0" [[package]] name = "synth-cli" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "clap", @@ -1210,7 +1210,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "gimli", @@ -1225,7 +1225,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "synth-core", @@ -1239,7 +1239,7 @@ dependencies = [ [[package]] name = "synth-mcdc-harness" -version = "0.59.0" +version = "0.60.0" dependencies = [ "synth-backend-riscv", "synth-core", @@ -1247,14 +1247,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.59.0" +version = "0.60.0" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.59.0" +version = "0.60.0" dependencies = [ "criterion", "synth-cfg", @@ -1262,11 +1262,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.59.0" +version = "0.60.0" [[package]] name = "synth-synthesis" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "proptest", @@ -1281,7 +1281,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "clap", @@ -1297,7 +1297,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.59.0" +version = "0.60.0" dependencies = [ "anyhow", "chrono", @@ -1316,7 +1316,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.59.0" +version = "0.60.0" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index ac2239b2..be3ec8c6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -29,7 +29,7 @@ resolver = "2" # semver to publish, so the convention now catches up: workspace # version follows the release tag, bumped pre-tag in the release # checklist. See docs/release-process.md. -version = "0.59.0" +version = "0.60.0" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index b1b8d1ac..e6043105 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -7,7 +7,7 @@ module( name = "synth", # Kept in lockstep with [workspace.package] version in Cargo.toml. # Both are bumped pre-tag — see docs/release-process.md. - version = "0.59.0", + version = "0.60.0", ) # Bazel dependencies diff --git a/artifacts/status.json b/artifacts/status.json index a657b317..0b363176 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -33,7 +33,7 @@ "selector_lines_total": 29845, "selector_wildcard_arms_code": 55, "selector_wildcard_arms_total": 90, - "version": "0.59.0", + "version": "0.60.0", "verus_spec_fns": 8, "wasmcert_bridge_qed": 104 } diff --git a/crates/synth-backend-aarch64/Cargo.toml b/crates/synth-backend-aarch64/Cargo.toml index 4b190044..e5ce2f7f 100644 --- a/crates/synth-backend-aarch64/Cargo.toml +++ b/crates/synth-backend-aarch64/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "AArch64 (A64) host-native backend for synth — integer subset (milestone 1, #538)" [dependencies] -synth-core = { path = "../synth-core", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } thiserror.workspace = true tracing.workspace = true diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 628dc6de..3158b11a 100644 --- a/crates/synth-backend-awsm/Cargo.toml +++ b/crates/synth-backend-awsm/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "aWsm backend integration for the Synth compiler" [dependencies] -synth-core = { path = "../synth-core", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index 92b811ee..bc12e02f 100644 --- a/crates/synth-backend-riscv/Cargo.toml +++ b/crates/synth-backend-riscv/Cargo.toml @@ -11,8 +11,8 @@ categories.workspace = true description = "RISC-V encoder, ELF builder, PMP allocator, and bare-metal startup for synth" [dependencies] -synth-core = { path = "../synth-core", version = "0.59.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.60.0" } anyhow.workspace = true thiserror.workspace = true tracing.workspace = true @@ -21,4 +21,4 @@ tracing.workspace = true proptest.workspace = true # VCR-SEL-005 (#851): the cross-backend op-parity oracle probes the AArch64 # selector as the THIRD backend (tests/cross_backend_op_parity.rs only). -synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.59.0" } +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.60.0" } diff --git a/crates/synth-backend-wasker/Cargo.toml b/crates/synth-backend-wasker/Cargo.toml index be1c254b..6c522ad3 100644 --- a/crates/synth-backend-wasker/Cargo.toml +++ b/crates/synth-backend-wasker/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "Wasker backend integration for the Synth compiler" [dependencies] -synth-core = { path = "../synth-core", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index 319fe49b..32f3f184 100644 --- a/crates/synth-backend/Cargo.toml +++ b/crates/synth-backend/Cargo.toml @@ -15,8 +15,8 @@ default = ["arm-cortex-m"] arm-cortex-m = ["synth-synthesis"] [dependencies] -synth-core = { path = "../synth-core", version = "0.59.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.59.0", optional = true } +synth-core = { path = "../synth-core", version = "0.60.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.60.0", optional = true } anyhow.workspace = true thiserror.workspace = true @@ -24,4 +24,4 @@ thiserror.workspace = true # #667 move 2: the i64 pseudo-op expansion certification oracle # (tests/i64_expansion_certification.rs) feeds THIS crate's emitted encoder # bytes to the synth-verify expansion validator. Dev-only — no prod-dep edge. -synth-verify = { path = "../synth-verify", version = "0.59.0", features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.60.0", features = ["arm"] } diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 26859b33..c66e856e 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -66,23 +66,23 @@ exports_only_275_probe = [] # Path deps carry `version` so `cargo publish` rewrites them to the # crates.io coordinate. Bumping the workspace version requires # updating these in lockstep — see docs/release-process.md. -synth-core = { path = "../synth-core", version = "0.59.0" } -synth-frontend = { path = "../synth-frontend", version = "0.59.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.59.0" } -synth-backend = { path = "../synth-backend", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } +synth-frontend = { path = "../synth-frontend", version = "0.60.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.60.0" } +synth-backend = { path = "../synth-backend", version = "0.60.0" } # AArch64 host-native backend (#538) — small pure-Rust crate, always on. -synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.59.0" } +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.60.0" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.59.0", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.59.0", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.59.0", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.60.0", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.60.0", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.60.0", optional = true } # Optional translation validation — pure-Rust ordeal engine by default (#553), # no C++ toolchain needed. For the Z3 differential oracle build with # `--features verify,synth-verify/z3-solver` (+ SYNTH_SOLVER_DIFF=1 at runtime). -synth-verify = { path = "../synth-verify", version = "0.59.0", optional = true, features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.60.0", optional = true, features = ["arm"] } # Optional PulseEngine WASM optimizer # Uncomment when loom crate is available: diff --git a/crates/synth-frontend/Cargo.toml b/crates/synth-frontend/Cargo.toml index 1b5ef1b5..c4bba172 100644 --- a/crates/synth-frontend/Cargo.toml +++ b/crates/synth-frontend/Cargo.toml @@ -14,7 +14,7 @@ description = "WASM/WAT parser and module decoder frontend for the Synth compile # Internal path deps carry an explicit version so `cargo publish` # can rewrite to the crates.io coordinate. `path` is used for # in-workspace builds; `version` is what crates.io sees. -synth-core = { path = "../synth-core", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index 10896865..729766c3 100644 --- a/crates/synth-opt/Cargo.toml +++ b/crates/synth-opt/Cargo.toml @@ -11,7 +11,7 @@ categories.workspace = true description = "Peephole optimization passes for the Synth compiler" [dependencies] -synth-cfg = { path = "../synth-cfg", version = "0.59.0" } +synth-cfg = { path = "../synth-cfg", version = "0.60.0" } [dev-dependencies] criterion = { version = "0.8", features = ["html_reports"] } diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml index 0cfd2ba9..a90b4aca 100644 --- a/crates/synth-synthesis/Cargo.toml +++ b/crates/synth-synthesis/Cargo.toml @@ -11,9 +11,9 @@ categories.workspace = true description = "WASM-to-ARM instruction selection and peephole optimizer" [dependencies] -synth-core = { path = "../synth-core", version = "0.59.0" } -synth-cfg = { path = "../synth-cfg", version = "0.59.0" } -synth-opt = { path = "../synth-opt", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } +synth-cfg = { path = "../synth-cfg", version = "0.60.0" } +synth-opt = { path = "../synth-opt", version = "0.60.0" } serde.workspace = true anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml index 27a00da6..2d8ba0df 100644 --- a/crates/synth-verify/Cargo.toml +++ b/crates/synth-verify/Cargo.toml @@ -22,12 +22,12 @@ arm = ["synth-synthesis"] [dependencies] # Core dependencies (always required) -synth-core = { path = "../synth-core", version = "0.59.0" } -synth-cfg = { path = "../synth-cfg", version = "0.59.0" } -synth-opt = { path = "../synth-opt", version = "0.59.0" } +synth-core = { path = "../synth-core", version = "0.60.0" } +synth-cfg = { path = "../synth-cfg", version = "0.60.0" } +synth-opt = { path = "../synth-opt", version = "0.60.0" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.59.0", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.60.0", optional = true } # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553). # EXACT-PINNED deliberately: for a 0.x solver a MINOR bump is a breaking bump, diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 644637a2..d396821b 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -7,7 +7,7 @@ > stale. All numbers come from [`artifacts/status.json`](../../artifacts/status.json), > which is re-derived from source on every run — never hand-edited. -**Workspace version:** 0.59.0 +**Workspace version:** 0.60.0 --- diff --git a/npm/package.json b/npm/package.json index ab76c038..c14c0d07 100644 --- a/npm/package.json +++ b/npm/package.json @@ -1,6 +1,6 @@ { "name": "@pulseengine/synth", - "version": "0.59.0", + "version": "0.60.0", "description": "synth — a WebAssembly-to-ARM/RISC-V/AArch64 compiler with mechanized correctness proofs. Produces bare-metal ELF binaries for embedded targets.", "bin": { "synth": "./run.js"