v0.2.3

A small patch update while we work on large scale changes. A Soteria Rust flag was changed, and we saw overall performance improvements of Soteria Rust and C, by up to 20% and 8% respectively!

This release supersedes v0.2.0–v0.2.2; all of their changes are included here.

Added

• The binary packages now ship LICENSE, NOTICE, THIRD_PARTY_NOTICES and the LICENSES/ and third-party-licenses/ directories.

Changed

• Soteria Rust: renamed --recursive-validity to --reference-to-invalid-memory to better reflect that it's a lint (allow/deny/warn) and not a flag. It is also now set to allow by default, to improve performance.
• Update THIRD_PARTY_NOTICES to be up to date.
• Minor soundness fixes.
• Minor performance improvements to Soteria Rust and Soteria C.

Packaging

• Removed an unresolved soteria-c import from Soteria's test dependencies.
• Declared printbox explicitly, and set minimum versions for zarith (1.13) and menhir (20230415).
• Added menhir and ocamlformat as test dependencies.
• OCaml tests that use the solver are now skipped when Z3 is not installed.

Frontend versions

Built against:

• Charon soteria-tools/charon 4398b734716b0f3c26a8b43b8791e698bc242139
• Obol soteria-tools/obol d27ea9db94a7ad0bca8559a817a1936d19d38b5a