Skip to content

v0.3.6

Latest
Latest

Choose a tag to compare

View all tags
@maximebuyse maximebuyse released this 15 Jan 10:43
· 473 commits to main since this release
hax-lib-v0.3.6
87ba968
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Changes to the Rust Engine:

  • Add a rejection phase for interleaving of expressions and statements not supported by the Lean do-notation syntax (#1739).
  • Add a phase to handle the monadic encoding: it explicitly introduces two new Hax primitives pure (to wrap values as monadic computations) and lift (to lift monadic computations into values) (#1746)
  • Add a mechanism to lookup pre- and post-conditions (#1805)

Changes to the frontend:

  • Update the pin of rustc (#1765)
  • Miscellaneous changes related to Charon (#1765)

Change to cargo-hax:

Changes to hax-lib:

  • Add Lean core models for options, results, default (#1747)
  • F* lib: improved while loops support, additions of some specific arithmetic operations and fixed TryInto for integer types (#1742)
  • Lean lib: use macros for int operations (#1795)
  • Lean lib: add new setup for bv_decide (#1828)
  • Lean lib: base specs on mathematical integers (#1829)
  • Lean lib: represent usize via a copy of UInt64 (#1829)
  • Lean lib: Add support for while loops (#1857, #1863)

Changes to the Lean backend:

  • Support for constants with arbitrary computation (#1738)
  • Add support for base-expressions of structs (#1736)
  • Use the explicit monadic phase to insert pure and ← only on demand, and not introduce extra do block (#1746)
  • Rename Result monad to RustM to avoid confusion with Rust Result type (#1768)
  • Add support for shift-left (#1785)
  • Add support for default methods of traits (#1777)
  • Add support for floats (#1784)
  • Add support for pattern matching on constant literals (#1789)
  • Add support for binding subpatterns in match constructs (#1790)
  • Add error when using patterns in function parameters (#1792)
  • Add grind annotations for various lemmas in the Lean library (#1802)
  • Add support for constant parameters to functions and traits (#1797)
  • Add support for associated types with equality constraints (#1806)
  • Make trait-level arguments explicit for all trait functions, adding them as extra parameters (#1803)
  • Add generation of specs from requires/ensures-annotations (#1815)
  • Add support for nonliteral array sizes (#1826)
  • Add hax_lib::lean::proof attribute (#1831)
  • Add support for #[hax_lib::opaque] (#1846)
  • Turn rejection phase into a transformation phase (#1840)

Miscellaneous:

  • Reserve extraction folder for auto-generated files in Lean examples (#1754)
Assets 2
Loading