Skip to content

v0.3.7

Latest
Latest

Choose a tag to compare

View all tags
@maximebuyse maximebuyse released this 20 May 15:18
· 111 commits to main since this release
hax-lib-v0.3.7
d8b5b3d
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:

  • Rename GenericConstraint::Type to TypeClass and ::Projection to Equality (#1996)
  • Remove BinOp resugaring (#1950)
  • Apply resugarings to linked items (pre/post conditions) (#1961)
  • Add new import_thir implemented in Rust and using FullDef, activated with --experimental-full-def (#1967)

Changes to the engine:

  • Omit type aliases whose body has unresolvable trait bounds instead of crashing (#2014)
  • Report let-chains (if let .. && let ..) as a soft error instead of panicking (#2014)

Changes to the frontend:

  • Fix support for ellipsis: add wildcard for every field (based on type info
    rather than number of subpatterns) (#2001)
  • Fix panic on constants of type &[&T] (e.g. &[&str]) caused by a wrong type for the synthesized array length (#2014)

Changes to cargo-hax:

Changes to hax-lib:

  • Lean lib: use Rust core models (#1865)
  • Lean lib: specs for negation (#1891)
  • Lean lib: Add casting for all integer type pairs (#1837)
  • Lean lib: bump lean to v4.28.0-rc1 (#1900)
  • Lean lib: Extract more core models (#1919)
  • Lean lib: Separate symbolic and bit-blasting specs (#1933)
  • Lean lib: Communicate user-generated specs to mvcgen (#1937)
  • Lean lib: Rust primitives for prop (#1942)
  • Lean lib: For-loops for all unsigned integers (#1951)
  • Lean lib: Upgrade to Lean v4.29.0-rc1 (#1962)
  • Lean lib: Add support for Int128 and UInt128 while waiting for upstream in Lean (#1968)
  • Lean lib: Refactor RustM as ExceptT Error Option (#1994)
  • Lean lib: Add Repr instance for tuples (#2000)
  • Lean lib: Make the proof of RustM.toBVRustM_bind compatible with Lean 4.29.0 (#2005)
  • F* lib: Add bit-extensionality (lemma_int_t_eq_via_bits), concrete Core_models.Num.impl_u64__rotate_left delegating to a new Rust_primitives.Integers.rotate_left_u, logand_commutative, fixed bit_or SMTPat semantics, bit_xor/get_bit_xor/get_bit_lognot SMTPats, and Rust_primitives.Hax.Monomorphized_update_at_Lemmas.lemma_index_update_at_range for libcrux SHA-3 equivalence proofs

Changes to the Lean backend:

  • Add hax_zify and hax_construct_pure tactics (#1888)
  • Add support for opaque impls (#1887)
  • Fix support for associated constants in trait impls (#1906)
  • Gather definitions in namespaces, shortening names (#1901)
  • Add support for associated types with constraints and inheritance (#1909)
  • Fix bug with monadic wrapping of trait constants (#1929)
  • Add type annotation for cast_op (#1925)
  • Add attributes for pureEnsures/pureRequires (#1931)
  • Extract correct PhantomData structure (#1932)
  • Standardize generated Lean naming to lowercase namespaces (#1914)
  • Fix associated constants with default values (#1941)
  • New default proof for the Lean backend & proof method attribute (#1938)
  • Prettier proof_mode annotations (#1943)
  • Detect recursive functions and mark them partial_fixpoint (#1946)
  • Add more binops (#1963)
  • Add a resugaring for ellipsis patterns (#2002)

Miscellaneous:

  • Fix Nix development shell: add an fstar devShell providing F* and the
    required environment variables (#1972)
Assets 2
Loading