Skip to content

synth v0.55.0

Choose a tag to compare

View all tags
@github-actions github-actions released this 07 Aug 17:22
· 272 commits to main since this release
v0.55.0
This tag was signed with the committer’s verified signature.
avrabe Ralf Anton Beier
SSH Key Fingerprint: zvTyfAFp29N6McgyIZRf8N4bOkpnU84deMxZN140NR4
Verified
Learn about vigilant mode.
97bd6db
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

  • feat(#901): ProvenSafeBoundsChecker — fail-closed, attested bounds-check elision from scry's proofs (VCR-MEM-004) by @avrabe in #915
  • fix(#916): i64 zero-fill mis-encoded for a high destination — MOVS transmuted to CMP at FIVE sites, not two by @avrabe in #919
  • L7: traceability repair — rivet ours-errors 2 → 0, VCR-RA-004/SEL-005 de-staled, VCR-VER-004 filed (#893) by @avrabe in #913
  • Make the evidence say what it measures: scope the coverage number, assert what the oracles actually execute (#910) by @avrabe in #918
  • VCR-DEC-001 increment 4 (VCR-REACH-001): the allocator models the i64 register-pair ops — 316→411 applied, measured (#242) by @avrabe in #917
  • aarch64: br_table + value-carrying block/loop/if (#851, VCR-A64-CF-001) by @avrabe in #914
  • VCR-RA-010: const-remat eligibility DERIVED from the stream, the hint only gates (#242) by @avrabe in #920
  • wcet: name the op and byte offset in an unmodeled-op decline (#921) by @avrabe in #922
  • release: v0.55.0 — "The scry seam" by @avrabe in #925

Full Changelog: v0.54.0...v0.55.0

Contributors

avrabe
Assets 12
Loading