Skip to content

Vow 0.3.0

Latest

Choose a tag to compare

@github-actions github-actions released this 16 Jul 13:59
Immutable release. Only release title and notes can be modified.

What's Changed

  • Add release.sh wrapper for triggering the Release workflow by @pmatos in #494
  • ci: add advisory macOS bootstrap + test jobs by @pmatos in #493
  • fix(verifier): bound ESBMC memory usage by @pmatos in #502
  • fix(clif-shim): make macOS link reproducible (#500) by @pmatos in #509
  • [codex] Add release toolchain tarballs by @pmatos in #508
  • build(deps): bump actions/download-artifact from 7 to 8 by @dependabot[bot] in #517
  • build(deps): bump cranelift-codegen from 0.131.1 to 0.131.2 by @dependabot[bot] in #518
  • build(deps): bump serde_json from 1.0.149 to 1.0.150 by @dependabot[bot] in #519
  • build(deps): bump cranelift-frontend from 0.131.1 to 0.131.2 by @dependabot[bot] in #544
  • build(deps): bump cranelift-module from 0.131.1 to 0.131.2 by @dependabot[bot] in #543
  • build(deps): bump cranelift-native from 0.131.1 to 0.131.2 by @dependabot[bot] in #542
  • build(deps): bump cranelift family from 0.131 to 0.132 by @pmatos in #565
  • docs: 0.3.0 foundations stabilization plan (arena + verification) by @pmatos in #564
  • build(deps): bump codecov/codecov-action from 6 to 7 by @dependabot[bot] in #566
  • fix(verify): mark nested-collection vec ops as non-modelable by @pmatos in #549
  • fix(sat): add overflow guards to lit_var/lit_bucket/lit_value contracts by @pmatos in #545
  • Fix C emitter emitting return value; in void functions by @pmatos in #548
  • Reject linear types as BTreeMap values by @pmatos in #550
  • fix(checker): attribute multi-module diagnostics to correct source file by @pmatos in #547
  • Remove verify-only collection capacity flags (#278) by @pmatos in #579
  • region: refresh handle_inst Return-arm comment for CallerReturn (#372) by @pmatos in #581
  • fix(checker): bind match payload for built-in Option/Result by @pmatos in #695
  • docs(audit): 2026-06-10 Vow language & compiler audit — 165 findings, 111 issues filed (milestone 0.4.0) by @pmatos in #694
  • docs(spec): design narrow-int numeric tower (ADR 0001) by @pmatos in #522
  • docs(spec): contract methodology — which properties to verify (#81) by @pmatos in #576
  • feat(contracts): static contract-quality classifier (#81) by @pmatos in #577
  • docs(skill): bundle contract methodology into the agent skill (#81) by @pmatos in #578
  • fix(checker): enforce vow-clause purity in the self-hosted compiler (#586) by @pmatos in #701
  • fix(checker): effect and linear errors must fail the build (#705) by @pmatos in #706
  • fix(verify): fail closed when the verifier worker panics (#413) by @pmatos in #707
  • chore: regenerate --help/skill mirror after ADR 0001 (#522) by @pmatos in #708
  • fix(contracts): vow contracts --verify fails closed on unproven contracts (#479) by @pmatos in #709
  • fix(verify): tighten arena addr bound to strict < (#480) by @pmatos in #722
  • test(verify): assert returned allocation alignment (#430) by @pmatos in #723
  • test(verify): assert try_extend success/rejection contract (#433) by @pmatos in #724
  • test(verify): verify try_extend frame condition (#431, #432) by @pmatos in #725
  • feat(verify): precise per-clause contracts --verify status via ESBMC --multi-property (#81 PR-A) by @pmatos in #716
  • feat(verify): detect vacuous contracts via ESBMC --error-label (#81 PR-B) by @pmatos in #717
  • feat(verify): detect trivially-satisfiable (weak) ensures via body-replace (#81 PR-C) by @pmatos in #718
  • feat(contracts): harden dispatch contracts + CI weak-gate (#81 PR-D) by @pmatos in #719
  • refactor(contracts): tag families are structural, not contracted (#81 PR-E) by @pmatos in #720
  • fix(verify): single-shot --unwind 5 --boolector for arena harness (#516) by @pmatos in #721
  • test(verify): directed mid-size path-oversized chunk scenario (#422-#426) by @pmatos in #726
  • test(full_test): run arena/esbmc verify under the 2 GB ulimit (#546) by @pmatos in #727
  • refactor(verify): rename VerifyOutcome::Skipped to NotRun (#385) by @pmatos in #728
  • test(full_test): check function parity in compare_verify soft-fail (#377) by @pmatos in #730
  • fix(skill): live-toolchain probe must not hard-fail when vow is absent (#582) by @pmatos in #729
  • fix(help): align generated help with implemented builtins by @pmatos in #758
  • test(clif-shim): unit-test inst_region_for_value region inference (#367) by @pmatos in #731
  • fix(runtime): checked arithmetic in Vec reserve growth (#435) by @pmatos in #732
  • feat(test): distinguish contract_skipped from verify_failed (#386) by @pmatos in #733
  • docs(design): code-complexity research + vowc complexity tool design by @pmatos in #757
  • ci: fix stale Codecov slug, add codecov.yml + coverage badges by @pmatos in #754
  • test(verify): assert returned allocation alignment (#430) by @pmatos in #749
  • fix(skill): resync embedded + mirror skill docs after #386 contract_skipped by @pmatos in #762
  • test(verify): remove ESBMC unwind/SMT bounds from contract fixtures (#552) by @pmatos in #734
  • feat(checker): enforce mut in the type checker (#735) by @pmatos in #743
  • feat(contracts): harden remaining 11 weak bit-packers, weak-gate → 0 (#81) by @pmatos in #765
  • test(verify): verifier-evaluation suite — false-accept / false-reject / blame (#334) by @pmatos in #766
  • chore(deps): bump the cranelift group with 5 updates by @dependabot[bot] in #763
  • Verification honesty: remove tautological contracts, fix u64/refinement soundness holes, correct strategy label by @pmatos in #736
  • feat(verify): add --replay-cex differential test of verifier model vs runtime (#335) by @pmatos in #780
  • feat(complexity): vow complexity subcommand (Phases 1-4) by @pmatos in #776
  • feat(perfetto): --perfetto compilation trace flag (Chrome/Perfetto trace of build+verify) by @pmatos in #785
  • feat(perfetto): implement --perfetto tracer in the self-hosted compiler (#784) by @pmatos in #789
  • fix(region): lift loop-carried values out of refreshed loop arenas, reclaiming small Vec leaks (#400) by @pmatos in #788
  • fix(build): prefer release over debug archives in cargo-target lib fallback by @pmatos in #791
  • fix(sat-bench): tolerate result rows without elapsed_s in summary by @pmatos in #793
  • chore(deps): bump sysinfo from 0.33.1 to 0.39.3 by @dependabot[bot] in #787
  • chore(deps): bump actions/checkout from 6 to 7 by @dependabot[bot] in #786
  • stdlib/: unify standard library + add documentation website by @pmatos in #792
  • fix(verifier): remove weak invariant unwind-bound contract by @pmatos in #800
  • ci(docs): hash-pin MkDocs build dependencies by @pmatos in #815
  • fix(complexity): count parameter refinements in contract metrics by @pmatos in #812
  • fix(test): keep complexity parity loop set-e safe by @pmatos in #811
  • fix(verify): namespace verifier C user functions by @pmatos in #805
  • fix(verify): declare unsigned long nondet extern by @pmatos in #803
  • fix(verify-eval): tighten harness diagnostics by @pmatos in #799
  • fix(reports): enforce calibration snapshot retention policy by @pmatos in #808
  • fix(complexity): precompute fan-in counts by @pmatos in #810
  • refactor(skill): index self-hosted support content by @pmatos in #814
  • fix(complexity): complete deferred predicate metric follow-ups by @pmatos in #809
  • test(verify): clarify non-gating stress fixture comment by @pmatos in #798
  • fix(json): share analysis string escaping by @pmatos in #806
  • fix(verifier): fail loud on unknown nondet type ids by @pmatos in #804
  • fix(verify): name callee precondition counterexamples by @pmatos in #807
  • test(verify): lock libc-named user function modelability by @pmatos in #826
  • fix(ci): run verifier eval against self-hosted compiler by @pmatos in #802
  • fix(contracts): use suffix membership in suffix_len by @pmatos in #801
  • docs(stdlib): correct verification status after unreserving abs by @pmatos in #827
  • fix(complexity): harden reads and free vars by @pmatos in #813
  • build(deps): bump sysinfo from 0.39.3 to 0.39.5 by @dependabot[bot] in #833
  • build(deps): bump actions/configure-pages from 5 to 6 by @dependabot[bot] in #828
  • build(deps): bump actions/deploy-pages from 4 to 5 by @dependabot[bot] in #829
  • build(deps): bump actions/setup-python from 5 to 6 by @dependabot[bot] in #831
  • build(deps): bump actions/upload-pages-artifact from 3 to 5 by @dependabot[bot] in #830
  • build(deps): bump the cranelift group with 5 updates by @dependabot[bot] in #832
  • build(deps): bump actions/cache from 5 to 6 by @dependabot[bot] in #836
  • fix(cli): command-specific missing-source error + document complexity in --help --human by @pmatos in #834
  • fix(compiler): keep loop-carried u64 unsigned across merge phis (#840) by @pmatos in #842
  • build: install self-hosted compiler as 'vow'; add --with-rust-compiler by @pmatos in #845
  • feat(stdlib): base-2^32 bignum with u64 interop, bitwise ops, monus by @pmatos in #839
  • perf(stdlib): small-int fast path for bignum by @pmatos in #847
  • test: rename stale tests/multi/bignum fixture to bignum_legacy by @pmatos in #849
  • fix(compiler): reject u64/i64 mixing in self-hosted checker by @pmatos in #852
  • build(deps): bump the cranelift group across 1 directory with 5 updates by @dependabot[bot] in #837
  • fix(compiler): close u64/i64 hole at is_coercible sites via literal marker (#853) by @pmatos in #854
  • test(skill): assert generated support cardinality by @pmatos in #856
  • refactor(compiler): clarify fan-in count increment by @pmatos in #857
  • fix(verify): keep libc-named user functions modelable by @pmatos in #858
  • test(compiler): make complexity I/O test path-independent by @pmatos in #859
  • docs(cli): document counterexample arg value sentinel by @pmatos in #860
  • refactor(compiler): centralize caller precondition sentinel by @pmatos in #861
  • fix(compiler): preserve u64 match result phi type by @pmatos in #863
  • fix(compiler): align legacy missing-source message by @pmatos in #862
  • fix(installer): hint after legacy toolchain upgrades by @pmatos in #864
  • perf(compiler): index lowerer instruction types by id by @pmatos in #865
  • fix(compiler): preserve Option payload type in self-hosted match by @pmatos in #867
  • fix(types): preserve trailing return statement type by @pmatos in #866
  • fix(types): separate integer literal marker from i32 by @pmatos in #868
  • refactor(complexity): extract pure analyze_function from run_complexity_command by @pmatos in #869
  • refactor(test): extract pure build_test_result from run_test_command by @pmatos in #870
  • refactor(examples): promote chess demo to its own folder by @pmatos in #873
  • refactor(examples): make ucinewgame the canonical per-game reset by @pmatos in #874
  • refactor(contracts): extract pure build_contract_entries from run_contracts_command by @pmatos in #876
  • fix(runtime): reserve exit code 134 for runtime aborts by @pmatos in #880
  • refactor(test): extract pure filter_test_files from run_test_command by @pmatos in #878
  • fix(region): free per-node move-list allocations in recursive search (#871) by @pmatos in #879
  • build(deps): bump sysinfo from 0.39.5 to 0.39.6 by @dependabot[bot] in #884
  • feat(vow-verify): codify safe-vs-unsafe adaptive-retry discipline (#337) by @pmatos in #885
  • fix(verify): model user structs in ESBMC via heap model (#397) by @pmatos in #887
  • refactor(verify): single source of truth for the ESBMC command line by @pmatos in #886
  • refactor(region): remove vestigial AMBIGUOUS machinery (superseded by #871 widen-to-Root) by @pmatos in #889
  • refactor(vow): extract contract-quality classification into a deep module by @pmatos in #890
  • refactor(codegen): extract return-materialization into a deep module by @pmatos in #891
  • build(deps): bump idna from 3.11 to 3.15 in /workflow by @dependabot[bot] in #892
  • ci: restrict GITHUB_TOKEN permissions in CI workflows by @pmatos in #895
  • refactor(runtime): encapsulate arena chunk-link access behind accessors by @pmatos in #896
  • refactor(vow): extract counterexample partial-evaluators into cex_eval module by @pmatos in #897
  • build(deps): bump clap from 4.6.1 to 4.6.2 by @dependabot[bot] in #900
  • feat(region): surface RegionRootEscape notes for multi-slot widen-to-Root by @pmatos in #898
  • refactor(vow): extract counterexample replay into a deep replay module by @pmatos in #901
  • fix(compiler): call cemit_str2 not clif's str2 in c_emitter heap-model store (#902) by @pmatos in #906
  • fix(runtime): use *const c_char for FFI string pointers (aarch64 build) by @pmatos in #913

Full Changelog: v0.2.0...v0.3.0