Skip to content

synth v0.60.0

Choose a tag to compare

View all tags
@github-actions github-actions released this 27 Aug 17:27
· 147 commits to main since this release
v0.60.0
4e7a179
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

What's Changed

  • plan(v0.60): scope the release — "Derive what you check against", 8 artifacts by @avrabe in #1070
  • RQ-60-A64IMPORT (VCR-REACH-002 inc. 1): aarch64 import dispatch — SHN_UNDEF externals, the ARM #197 contract ported. Refs #1017, Refs #242 by @avrabe in #1071
  • RQ-60-VFPPRESSURE increment 1: AEABI-routed i64-f32 conversions on single-precision FPU targets - Refs #1069, Refs #869 by @avrabe in #1073
  • chore(rivet): RQ-60-CANARY + RQ-60-A64IMPORT implemented — the 4th and 5th orphaned flips, plus a floor left slack by @avrabe in #1074
  • RQ-60-VFPPRESSURE increment 2: frame-homed overflow VFP locals — the 13->14 homed-local wall falls, 5/5 falcon cascade stages on cortex-m7dp (Refs #1069) by @avrabe in #1075
  • RQ-60-FLIPCOUPLE (#1064): status-evidence gate — a release status must agree with the evidence on main; seven-instance replay 7/7 by @avrabe in #1076
  • chore(rivet): RQ-60-VFPPRESSURE implemented — 5/5 falcon stages verified, and why it stops short of verified by @avrabe in #1077
  • chore(rivet): RQ-60-VFPPRESSURE verified — jess ran the fused image and it executes on RT1176 by @avrabe in #1078
  • RQ-60-CFOBLIG (#1057) increment 1: the WASM model gains BrIf — constructor, executable semantics, and a kernel-checked correspondence obligation by @avrabe in #1079
  • RQ-60-WCETKEY (#1063): name-section names as durable WCET identities + symmetric --wcet-hints keys by @avrabe in #1081
  • RQ-60-RACOST (#242) increment 1: tied use/def webs — rmw colour mismatch unrepresentable by @avrabe in #1082
  • RQ-60-RACOST (#242) increment 2: real-encoder cost model + final-byte arbiter — 66 shrink / 0 grow by @avrabe in #1083
  • RQ-60-ARTIFACTSPLIT (#1059): per-requirement release-artifact files (v0.61+) + R5/R6 structural rules over all release files by @avrabe in #1084
  • RQ-60-WCETKEY (#1063) increment 2: refused hints reach the sidecar, not only stderr by @avrabe in #1086
  • fix(#1087): parse the ledger duplicate-key-strict — a +622-line waiver was recorded with a +10-line justification by @avrabe in #1088
  • RQ-60-CFOBLIG (#1057) inc 2: proof-inventory manifest — derive, don't guess theorem names (brif_correct is the 29th member of a class) by @avrabe in #1089
  • fix(#1085): two v0.60 artifacts pinned evidence that could not fail on the failure they define by @avrabe in #1090
  • chore(release): v0.60.0 assembly — "Derive what you check against, and reach is part of correctness" by @avrabe in #1092

Full Changelog: v0.59.0...v0.60.0

Contributors

avrabe
Assets 12
Loading