From 50e5990dd69a1e86077d2aa22872a9f80249b1cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 3 Jul 2025 19:03:35 +0200 Subject: [PATCH 01/44] Add special case for anonymous constants (not output produced) --- rust-engine/src/ast/identifiers.rs | 5 +++++ rust-engine/src/lean.rs | 11 +++++++++++ 2 files changed, 16 insertions(+) diff --git a/rust-engine/src/ast/identifiers.rs b/rust-engine/src/ast/identifiers.rs index abe7fd51f..957755201 100644 --- a/rust-engine/src/ast/identifiers.rs +++ b/rust-engine/src/ast/identifiers.rs @@ -102,6 +102,11 @@ pub mod global_id { } } + /// Returns true if the GlobalId is actually empty (reduced to "_") + pub fn is_empty(&self) -> bool { + self.to_debug_string() == "_".to_string() + } + /// Raw printing of identifier separated by underscore. Used for testing pub fn to_debug_string(&self) -> String { match self { diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index b960df634..97ff2e723 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -34,6 +34,17 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Item { impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { match self { + ItemKind::Fn { + name, + generics: _, + body: _, + params, + safety: _, + } if name.is_empty() && params.is_empty() => { + // Anonymous const, ignored + // Todo: turn it into a proper refactor (see Hax issue #1542) + allocator.nil() + } ItemKind::Fn { name, generics: _, From bbfcca791d2e3dcc6c709ca559748732ffe92daf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 3 Jul 2025 19:04:17 +0200 Subject: [PATCH 02/44] Remove newlines between empty document --- rust-engine/src/lean.rs | 27 ++++++++++++++++++++------- rust-engine/src/main.rs | 5 +---- 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 97ff2e723..e21c7f361 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -53,15 +53,23 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { safety: _, } => { // Generics are ignored for now + + let args = if params.is_empty() { + allocator.nil() + } else { + docs![ + allocator, + allocator.softline(), + allocator.intersperse(params, allocator.line()), + ] + .align() + .group() + }; docs![ allocator, "def ", name, - allocator.softline(), - allocator - .intersperse(params, allocator.line()) - .align() - .group(), + args, docs![allocator, allocator.line(), ": ", &body.ty].group(), " :=", allocator.line(), @@ -69,12 +77,17 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { ] .nest(INDENT) .group() + .append(allocator.hardline()) + .append(allocator.hardline()) } ItemKind::TyAlias { name, generics: _, ty, - } => docs![allocator, "abbrev ", name, allocator.reflow(" := "), ty].group(), + } => docs![allocator, "abbrev ", name, allocator.reflow(" := "), ty] + .group() + .append(allocator.hardline()) + .append(allocator.hardline()), ItemKind::Type { name: _, generics: _, @@ -106,7 +119,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { } => print_todo!(allocator), ItemKind::Error(_diagnostic) => print_todo!(allocator), ItemKind::Resugared(_resugared_ty_kind) => print_todo!(allocator), - ItemKind::NotImplementedYet => allocator.text("-- unimplemented yet"), + ItemKind::NotImplementedYet => allocator.nil(), } } } diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index d71351ab9..bef92c75a 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -31,10 +31,7 @@ fn lean_backend(items: Vec) { .append(allocator.hardline()) .append(allocator.hardline()); - let item_docs: DocBuilder<_, Span> = header.append(allocator.intersperse( - items.iter(), - allocator.hardline().append(allocator.hardline()), - )); + let item_docs: DocBuilder<_, Span> = header.append(allocator.concat(items.iter())); hax_rust_engine::hax_io::write(&hax_types::engine_api::protocol::FromEngine::File(File { path: krate + ".lean", From 821757a94db5f693368b9d99d753a4d08840b272 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 15 Jul 2025 18:44:39 +0200 Subject: [PATCH 03/44] Update proof lib for Barrett example --- hax-lib/proof-libs/lean/Lib.lean | 129 +++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 hax-lib/proof-libs/lean/Lib.lean diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean new file mode 100644 index 000000000..d2ed3862c --- /dev/null +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -0,0 +1,129 @@ +-- This library is the panic-free version of the prelude, where identifiers are +-- *as most as possible* interpreted without any proof obligation, ignoring +-- potential rust panics. It is useful for testing, but proving properties with +-- it would not guarantee panic freedom. + +-- Logic +abbrev hax_logical_op_and := (fun a b => a ∧ b) + +-- Integer types +abbrev u8 := Nat -- to fix +abbrev u16 := UInt16 +abbrev u32 := UInt32 +abbrev u64 := UInt64 +abbrev usize := USize +abbrev i8 := Int -- to fix +abbrev i16 := Int16 +abbrev i32 := Int32 +abbrev i64 := Int64 +abbrev isize := ISize + +-- Coercions between integers types: +instance : Coe i32 i64 where + coe x := x.toInt64 + +instance : Coe i64 i32 where + coe x := x.toInt32 + +-- Arithmetic +@[simp] +def hax_machine_int_add {α} [Add α] (x y: α) := x + y +@[simp] +def hax_machine_int_sub {α} [Sub α] (x y: α) := x - y +@[simp] +def hax_machine_int_mul {α} [Mul α] (x y: α) := x * y +@[simp] +def hax_machine_int_rem {α} [Mod α] (x y: α) := x % y +@[simp] +def hax_machine_int_shr {α β γ} [HShiftRight α β γ] (a: α) (b: β) : γ := a >>> b +@[simp] +def ops_arith_Neg_neg {α} [Neg α] (x:α) := -x + +@[simp] +def hax_machine_int_eq {α} (x y: α) [BEq α] : Bool := x == y +@[simp] +def hax_machine_int_ne (x y: Int) : Bool := x != y +@[simp] +def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Bool := x < y +@[simp] +def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Bool := x ≤ y +@[simp] +def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Bool := x ≥ y +@[simp] +def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Bool := x > y + +-- Tuples +structure hax_Tuple2_arg α β where +hax_Tuple2_Tuple0 : α +hax_Tuple2_Tuple1 : β + +inductive hax_Tuple2 (α β: Type) +| constr_hax_Tuple2 : (hax_Tuple2_arg α β) -> hax_Tuple2 α β + +abbrev hax_Tuple0 := () + +-- Nums +def num_impl_wrapping_add : Nat -> Nat -> Nat := sorry +def num_impl_from_le_bytes {α} : (Array α) -> u32 := sorry + +-- Casts +@[simp] +def convert_From_from {α β} [Coe α β] (x:α) : β := x +@[simp] +def hax_cast_op {α β} [Coe α β] (x:α) : β := x + +-- Results +inductive result_Result α β +| ok : α -> result_Result α β +| err : β -> result_Result α β + +axiom array_TryFromSliceError : Type + +-- Assert +def assert : Bool -> Unit := fun _ => () +def assume : Prop -> Unit := fun _ => () +def prop_constructors_from_bool : Bool -> Prop := sorry + +-- Hax +def hax_folds_fold_range + (s: Nat) + (e: Nat) : + ((Array u32) -> Nat -> Bool) -> + (Array u32) -> + ((Array u32) -> Nat -> (Array u32)) -> + (Array u32) := sorry + +def hax_monomorphized_update_at_update_at_usize : + (Array u32) -> + Nat -> + u32 -> + (Array u32) := sorry + +abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize (_: Nat) (_: Nat) := Nat + +def result_impl_unwrap {α} : α -> Array β := sorry + +-- Vectors +def hax_repeat (x:Nat) (y:Nat) : Array u32 := sorry + +-- Ranges + +structure ops_range_Range_arg (α: Type) where +ops_range_Range_start : α +ops_range_Range_end : α + +inductive ops_range_Range (α: Type) where +| constr_ops_range_Range : ops_range_Range_arg α -> ops_range_Range α + + +-- Arrays +def ops_index_Index_index (a: Array u8) : α -> β := sorry +def convert_TryInto_try_into {α} : Array α -> + result_Result (Array α) array_TryFromSliceError := sorry + + +-- Slices +def slice_impl_len (a: Array u32) : Nat := sorry + +-- Bytes +def num_impl_to_le_bytes : u32 -> Array u8 := sorry From 67f7f5bda7a5c676c848d046da28186c33a07f02 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 16 Jul 2025 14:14:47 +0200 Subject: [PATCH 04/44] Invert parens and groups in lean output --- .../barrett/proofs/lean/extraction/Lib.lean | 84 +------------------ rust-engine/src/lean.rs | 25 +++--- 2 files changed, 13 insertions(+), 96 deletions(-) mode change 100644 => 120000 examples/barrett/proofs/lean/extraction/Lib.lean diff --git a/examples/barrett/proofs/lean/extraction/Lib.lean b/examples/barrett/proofs/lean/extraction/Lib.lean deleted file mode 100644 index c71b38d20..000000000 --- a/examples/barrett/proofs/lean/extraction/Lib.lean +++ /dev/null @@ -1,83 +0,0 @@ -abbrev u8 := Nat -abbrev u16 := Nat -abbrev u32 := Nat -abbrev u64 := Nat -abbrev usize := Nat -abbrev i8 := Nat -abbrev i16 := Nat -abbrev i32 := Nat -abbrev i64 := Nat -abbrev isize := Nat - --- Arithmetic -def hax_machine_int_add (x y: Nat) := x + y -def hax_machine_int_mul (x y: Nat) := x * y -def hax_machine_int_bitxor (x y: Nat) : Nat := sorry - -def hax_machine_int_eq (x y: Nat) : Bool := x = y -def hax_machine_int_ne (x y: Nat) : Bool := x != y -def hax_machine_int_ge (x y: Nat) : Bool := x >= y -def hax_machine_int_gt (x y: Nat) : Bool := x > y -def hax_machine_int_le (x y: Nat) : Bool := x <= y -def hax_machine_int_lt (x y: Nat) : Bool := x < y - - --- Nums -def num_impl_wrapping_add : Nat -> Nat -> Nat := sorry -def num_impl_from_le_bytes {α} : (Array α) -> u32 := sorry - --- Results -inductive result_Result α β -| ok : α -> result_Result α β -| err : β -> result_Result α β - -axiom array_TryFromSliceError : Type - --- Assert -def assert : Bool -> Unit := fun _ => () -def assume : Prop -> Unit := fun _ => () -def prop_constructors_from_bool : Bool -> Prop := sorry - --- Hax -def hax_folds_fold_range - (s: Nat) - (e: Nat) : - ((Array u32) -> Nat -> Bool) -> - (Array u32) -> - ((Array u32) -> Nat -> (Array u32)) -> - (Array u32) := sorry - -def hax_monomorphized_update_at_update_at_usize : - (Array u32) -> - Nat -> - u32 -> - (Array u32) := sorry - -abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize (_: Nat) (_: Nat) := Nat - -def result_impl_unwrap {α} : α -> Array β := sorry - --- Vectors -def hax_repeat (x:Nat) (y:Nat) : Array u32 := sorry - --- Ranges - -structure ops_range_Range_arg (α: Type) where -ops_range_Range_start : α -ops_range_Range_end : α - -inductive ops_range_Range (α: Type) where -| constr_ops_range_Range : ops_range_Range_arg α -> ops_range_Range α - - --- Arrays -def ops_index_Index_index (a: Array u8) : α -> β := sorry -def convert_TryInto_try_into {α} : Array α -> - result_Result (Array α) array_TryFromSliceError := sorry - - --- Slices -def slice_impl_len (a: Array u32) : Nat := sorry - --- Bytes -def num_impl_to_le_bytes : u32 -> Array u8 := sorry diff --git a/examples/barrett/proofs/lean/extraction/Lib.lean b/examples/barrett/proofs/lean/extraction/Lib.lean new file mode 120000 index 000000000..e758df14c --- /dev/null +++ b/examples/barrett/proofs/lean/extraction/Lib.lean @@ -0,0 +1 @@ +../../../../../proof-libs/lean/Lib.lean \ No newline at end of file diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index e21c7f361..9822d98b1 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -62,7 +62,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { allocator.softline(), allocator.intersperse(params, allocator.line()), ] - .align() + .nest(INDENT) .group() }; docs![ @@ -142,8 +142,8 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b TyKind { head.pretty(allocator) .append(allocator.softline()) .append(allocator.intersperse(args, allocator.softline())) - .group() .parens() + .group() } } TyKind::Arrow { inputs, output } => allocator @@ -161,8 +161,8 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b TyKind { TyKind::Slice(ty) => docs![allocator, "Array ", ty].parens(), TyKind::Array { ty, length } => { docs![allocator, "Vector ", ty, allocator.softline(), &(**length),] - .parens() .group() + .parens() } TyKind::RawPointer => print_todo!(allocator), TyKind::AssociatedType { impl_: _, item: _ } => print_todo!(allocator), @@ -271,12 +271,11 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { bounds_impls: _, trait_: _, } => { - let separator = allocator.line(); head.pretty(allocator) .append(allocator.softline()) - .append(allocator.intersperse(args, separator).nest(INDENT)) - .parens() + .append(allocator.intersperse(args, allocator.softline()).nest(INDENT)) .group() + .parens() } ExprKind::Literal(literal) => literal.pretty(allocator), ExprKind::Array(exprs) => docs![ @@ -355,8 +354,8 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { ExprKind::LocalId(local_id) => local_id.pretty(allocator), ExprKind::Ascription { e, ty } => docs![allocator, e, allocator.reflow(" : "), ty] .nest(INDENT) - .parens() - .group(), + .group() + .parens(), ExprKind::Assign { lhs: _, value: _ } => print_todo!(allocator), ExprKind::Loop { body: _, @@ -374,13 +373,13 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { captures: _, } => docs![ allocator, + allocator.line_(), allocator.reflow("fun "), - allocator.intersperse(params, allocator.line()), - allocator.reflow(" =>"), - allocator.line(), + allocator.intersperse(params, allocator.line()).group(), + allocator.reflow(" => "), body ] - .nest(INDENT) + //.nest(INDENT) .group() .parens(), ExprKind::Block { @@ -476,7 +475,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Param { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { docs![allocator, &self.pat, allocator.softline(), ": ", &self.ty] .nest(INDENT) - .parens() .group() + .parens() } } From a4add12f0b5c042b3006e7688488969f7b88d2f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 21 Jul 2025 09:57:34 +0200 Subject: [PATCH 05/44] Update proof-lib for chacha20 example --- hax-lib/proof-libs/lean/Lib.lean | 149 ++++++++++++++++++++++++++----- 1 file changed, 128 insertions(+), 21 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index d2ed3862c..bcefe3056 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -3,16 +3,46 @@ -- potential rust panics. It is useful for testing, but proving properties with -- it would not guarantee panic freedom. +-- Aeneas errors + +inductive Error where + | assertionFailure: Error + | integerOverflow: Error + | divisionByZero: Error + | arrayOutOfBounds: Error + | maximumSizeExceeded: Error + | panic: Error + | undef: Error +deriving Repr, BEq + +open Error + +inductive Result.{u} (α : Type u) where + | ok (v: α): Result α + | fail (e: Error): Result α + | div +deriving Repr, BEq + +instance : Monad Result where + pure x := .ok x + bind x f := match x with + | .ok v => f v + | .fail e => .fail e + | .div => .div + +instance : LawfulMonad Result := sorry + -- Logic abbrev hax_logical_op_and := (fun a b => a ∧ b) -- Integer types abbrev u8 := Nat -- to fix +abbrev i8 := Int -- to fix + abbrev u16 := UInt16 abbrev u32 := UInt32 abbrev u64 := UInt64 abbrev usize := USize -abbrev i8 := Int -- to fix abbrev i16 := Int16 abbrev i32 := Int32 abbrev i64 := Int64 @@ -25,7 +55,27 @@ instance : Coe i32 i64 where instance : Coe i64 i32 where coe x := x.toInt32 +instance : Coe USize Nat where + coe x := x.toNat + +instance : Coe (BitVec 32) u32 where + coe x := UInt32.ofBitVec x + +instance {n} : CoeOut (BitVec n) (Result u32) where + coe x := match n with + | 32 => .ok (UInt32.ofBitVec x) + | _ => .fail (integerOverflow) + +instance : Coe u32 (BitVec 32) where + coe x := x.toBitVec + +instance : Coe u32 Nat where + coe x := x.toNat + -- Arithmetic +section Arithmetic + +-- Overflowing operations @[simp] def hax_machine_int_add {α} [Add α] (x y: α) := x + y @[simp] @@ -37,12 +87,14 @@ def hax_machine_int_rem {α} [Mod α] (x y: α) := x % y @[simp] def hax_machine_int_shr {α β γ} [HShiftRight α β γ] (a: α) (b: β) : γ := a >>> b @[simp] +def hax_machine_int_bitxor {α} [Xor α] (a b: α) : α := a ^^^ b +@[simp] def ops_arith_Neg_neg {α} [Neg α] (x:α) := -x @[simp] def hax_machine_int_eq {α} (x y: α) [BEq α] : Bool := x == y @[simp] -def hax_machine_int_ne (x y: Int) : Bool := x != y +def hax_machine_int_ne {α} (x y: α) [BEq α] : Bool := x != y @[simp] def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Bool := x < y @[simp] @@ -52,8 +104,42 @@ def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Bool := @[simp] def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Bool := x > y +abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize + (lo: USize) (hi: USize) := USize +-- {u : usize // lo ≤ u ∧ u ≤ hi} + +-- #check hax__autogenerated_refinement__BoundedUsize_BoundedUsize 0 19 +-- #check fun (x: {usize // True}) => x.val + +set_option pp.coercions false + +-- instance {n lo hi : Nat} {hlo: lo ≤ x} {hhi: x ≤ hi}: +-- OfNat (hax__autogenerated_refinement__BoundedUsize_BoundedUsize lo hi) x where +-- ofNat := { +-- val := x , +-- property := by +-- constructor +-- . unfold Nat.cast + +-- apply USize.le_iff_toNat_le.mp + +-- . apply USize.le_iff_toNat_le.mp +-- grind + +-- } +-- #check (10: hax__autogenerated_refinement__BoundedUsize_BoundedUsize 0 10) + +-- Wrapping operations +@[simp] +def num_impl_wrapping_add {α} [Add α] (x y: α) := x + y + +@[simp] +def num_impl_rotate_left {w} := @BitVec.rotateLeft w + +end Arithmetic + -- Tuples -structure hax_Tuple2_arg α β where +structure hax_Tuple2_arg (α β: Type) where hax_Tuple2_Tuple0 : α hax_Tuple2_Tuple1 : β @@ -63,7 +149,6 @@ inductive hax_Tuple2 (α β: Type) abbrev hax_Tuple0 := () -- Nums -def num_impl_wrapping_add : Nat -> Nat -> Nat := sorry def num_impl_from_le_bytes {α} : (Array α) -> u32 := sorry -- Casts @@ -80,26 +165,36 @@ inductive result_Result α β axiom array_TryFromSliceError : Type -- Assert -def assert : Bool -> Unit := fun _ => () +def assert (b:Bool) : Result Unit := + if b then pure () + else .fail (Error.assertionFailure) + def assume : Prop -> Unit := fun _ => () def prop_constructors_from_bool : Bool -> Prop := sorry -- Hax -def hax_folds_fold_range - (s: Nat) - (e: Nat) : - ((Array u32) -> Nat -> Bool) -> - (Array u32) -> - ((Array u32) -> Nat -> (Array u32)) -> - (Array u32) := sorry - -def hax_monomorphized_update_at_update_at_usize : - (Array u32) -> - Nat -> - u32 -> - (Array u32) := sorry - -abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize (_: Nat) (_: Nat) := Nat +def hax_folds_fold_range {α} + (s e : Nat) + (_filter : α -> Nat -> Bool) + (init: α) + (f : α -> Nat -> Result α) := + Array.foldlM f init (Array.range e) s e + +-- Arrays + +def hax_monomorphized_update_at_update_at_usize {α} + (a: Array α) (i:Nat) (v:α) : Result (Array α) := + if h: i < a.size then + pure ( Array.set a i v ) + else + .fail (.arrayOutOfBounds) + +def hax_update_at {α n} (m : Vector α n) (i : Nat) (v : α) : Result (Vector α n) := + if i < n then + .ok ( Vector.setIfInBounds m i v) + else + .fail (.arrayOutOfBounds) + def result_impl_unwrap {α} : α -> Array β := sorry @@ -116,12 +211,24 @@ inductive ops_range_Range (α: Type) where | constr_ops_range_Range : ops_range_Range_arg α -> ops_range_Range α + -- Arrays -def ops_index_Index_index (a: Array u8) : α -> β := sorry +section Arrays +def ops_index_Index_index (a: Array α) (i:Nat) : Result α := + match a[i]? with + | .none => .fail arrayOutOfBounds + | .some v => .ok v + def convert_TryInto_try_into {α} : Array α -> result_Result (Array α) array_TryFromSliceError := sorry +instance {α n} : CoeOut (Vector α n) (Array α) where + coe x := x.toArray + +instance {α β} [i:Coe α β]: Coe (Array α) (Array β) where + coe x := Array.map i.coe x +end Arrays -- Slices def slice_impl_len (a: Array u32) : Nat := sorry From 45b88098a7a145893856e686a7ca58b3e2efb0bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 22 Jul 2025 14:53:26 +0200 Subject: [PATCH 06/44] Make the Lean backend into a proper OCaml backend to control phases --- engine/backends/lean/dune | 21 +++++ engine/backends/lean/lean_backend.ml | 132 +++++++++++++++++++++++++++ engine/bin/dune | 1 + engine/bin/lib.ml | 16 +--- 4 files changed, 158 insertions(+), 12 deletions(-) create mode 100644 engine/backends/lean/dune create mode 100644 engine/backends/lean/lean_backend.ml diff --git a/engine/backends/lean/dune b/engine/backends/lean/dune new file mode 100644 index 000000000..0c5b33e6f --- /dev/null +++ b/engine/backends/lean/dune @@ -0,0 +1,21 @@ +(library + (name lean_backend) + (package hax-engine) + (wrapped false) + (libraries hax_engine base) + (preprocess + (pps + ppx_yojson_conv + ppx_sexp_conv + ppx_compare + ppx_hash + ppx_deriving.show + ppx_deriving.eq + ppx_inline + ppx_functor_application + ppx_matches))) + +(env + (_ + (flags + (:standard -w -A)))) diff --git a/engine/backends/lean/lean_backend.ml b/engine/backends/lean/lean_backend.ml new file mode 100644 index 000000000..cee16f2a2 --- /dev/null +++ b/engine/backends/lean/lean_backend.ml @@ -0,0 +1,132 @@ +open Hax_engine +open Utils +open Base + +include + Backend.Make + (struct + open Features + include Off + include On.Monadic_binding + include On.Slice + include On.Macro + include On.Construct_base + include On.Quote + include On.Dyn + include On.Unsafe + end) + (struct + let backend = Diagnostics.Backend.FStar + end) + +module SubtypeToInputLanguage + (FA : Features.T + with type mutable_reference = Features.Off.mutable_reference + and type continue = Features.Off.continue + and type break = Features.Off.break + and type mutable_reference = Features.Off.mutable_reference + and type mutable_pointer = Features.Off.mutable_pointer + and type mutable_variable = Features.Off.mutable_variable + and type reference = Features.Off.reference + and type raw_pointer = Features.Off.raw_pointer + and type early_exit = Features.Off.early_exit + and type question_mark = Features.Off.question_mark + and type as_pattern = Features.Off.as_pattern + and type lifetime = Features.Off.lifetime + and type monadic_action = Features.Off.monadic_action + and type arbitrary_lhs = Features.Off.arbitrary_lhs + and type nontrivial_lhs = Features.Off.nontrivial_lhs + and type loop = Features.Off.loop + and type block = Features.Off.block + and type for_loop = Features.Off.for_loop + and type while_loop = Features.Off.while_loop + and type for_index_loop = Features.Off.for_index_loop + and type state_passing_loop = Features.Off.state_passing_loop + and type fold_like_loop = Features.Off.fold_like_loop + and type match_guard = Features.Off.match_guard + and type trait_item_default = Features.Off.trait_item_default) = +struct + module FB = InputLanguage + + include + Subtype.Make (FA) (FB) + (struct + module A = FA + module B = FB + include Features.SUBTYPE.Id + include Features.SUBTYPE.On.Monadic_binding + include Features.SUBTYPE.On.Construct_base + include Features.SUBTYPE.On.Slice + include Features.SUBTYPE.On.Macro + include Features.SUBTYPE.On.Quote + include Features.SUBTYPE.On.Dyn + include Features.SUBTYPE.On.Unsafe + end) + + let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend)) +end + +module AST = Ast.Make (InputLanguage) + +module BackendOptions = struct + type t = Hax_engine.Types.f_star_options_for__null +end + +open Ast + +module U = Ast_utils.Make (InputLanguage) +module Visitors = Ast_visitors.Make (InputLanguage) +open AST + +module Context = struct + type t = { + current_namespace : string list; + items : item list; + interface_mode : bool; + line_width : int; + } +end + +open Phase_utils +module DepGraphR = Dependencies.Make (Features.Rust) + +module TransformToInputLanguage = + [%functor_application + Phases.Reject.RawOrMutPointer(Features.Rust) + |> Phases.Transform_hax_lib_inline + |> Phases.Specialize + |> Phases.Drop_sized_trait + |> Phases.Simplify_question_marks + |> Phases.And_mut_defsite + |> Phases.Reconstruct_asserts + |> Phases.Reconstruct_for_loops + |> Phases.Reconstruct_while_loops + |> Phases.Direct_and_mut + |> Phases.Reject.Arbitrary_lhs + |> Phases.Drop_blocks + |> Phases.Drop_match_guards + |> Phases.Drop_references + |> Phases.Trivialize_assign_lhs + |> Side_effect_utils.Hoist + |> Phases.Hoist_disjunctive_patterns + |> Phases.Simplify_match_return + |> Phases.Local_mutation + |> Phases.Rewrite_control_flow + |> Phases.Drop_return_break_continue + |> Phases.Functionalize_loops + |> Phases.Reject.Question_mark + |> Phases.Reject.As_pattern + |> Phases.Traits_specs + |> Phases.Simplify_hoisting + |> Phases.Newtype_as_refinement + |> Phases.Reject.Trait_item_default + |> Phases.Bundle_cycles + |> Phases.Reorder_fields + |> Phases.Sort_items + |> SubtypeToInputLanguage + |> Identity + ] + [@ocamlformat "disable"] + +let apply_phases (items : Ast.Rust.item list) : AST.item list = + TransformToInputLanguage.ditems items diff --git a/engine/bin/dune b/engine/bin/dune index da07f5d3e..815872542 100644 --- a/engine/bin/dune +++ b/engine/bin/dune @@ -5,6 +5,7 @@ (libraries hax_engine fstar_backend + lean_backend coq_backend ssprove_backend easycrypt_backend diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index da8be0bbc..8a8252270 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -257,7 +257,8 @@ let engine () = Printexc.raise_with_backtrace exn bt module ExportRustAst = Export_ast.Make (Features.Rust) -module ExportFStarAst = Export_ast.Make (Fstar_backend.InputLanguage) +module ExportLeanAst = Export_ast.Make (Lean_backend.InputLanguage) + (** Entry point for interacting with the Rust hax engine *) let driver_for_rust_engine () : unit = @@ -274,20 +275,11 @@ let driver_for_rust_engine () : unit = let imported_items = import_thir_items [] input in let imported_items = (* TODO: this let binding is applying the phases from the F* backend *) - Fstar_backend.apply_phases - { - cli_extension = EmptyStructempty_args_extension; - fuel = Int64.zero; - ifuel = Int64.zero; - interfaces = []; - line_width = 80; - z3rlimit = Int64.zero; - } - imported_items + Lean_backend.apply_phases imported_items in let rust_ast_items = List.concat_map - ~f:(fun item -> ExportFStarAst.ditem item) + ~f:(fun item -> ExportLeanAst.ditem item) imported_items in let response = Rust_engine_types.ImportThir { output = rust_ast_items } in From 21395f7921a1d1e8bfa27c4f6d33a1a891b258f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 23 Jul 2025 15:37:47 +0200 Subject: [PATCH 07/44] WIP on ChachaProof --- hax-lib/proof-libs/lean/Lib.lean | 362 ++++++++++++++++++++++++------- rust-engine/src/lean.rs | 233 +++++++++++++------- tests/lean-tests/src/lib.rs | 11 + 3 files changed, 445 insertions(+), 161 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index bcefe3056..bc1e9748d 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -1,9 +1,12 @@ --- This library is the panic-free version of the prelude, where identifiers are --- *as most as possible* interpreted without any proof obligation, ignoring --- potential rust panics. It is useful for testing, but proving properties with --- it would not guarantee panic freedom. - +-- This library provides a monadic encoding over Hax primitives -- Aeneas errors +import Std.Tactic.Do +import Std.Do.Triple +import Std.Tactic.Do.Syntax +import Std + +open Std.Do +open Std.Tactic inductive Error where | assertionFailure: Error @@ -23,73 +26,148 @@ inductive Result.{u} (α : Type u) where | div deriving Repr, BEq -instance : Monad Result where - pure x := .ok x - bind x f := match x with +@[simp] +def Result.pure (x:α) : Result α := .ok x + +@[simp] +def Result.bind (x: Result α) (f: α -> Result β) := match x with | .ok v => f v | .fail e => .fail e | .div => .div -instance : LawfulMonad Result := sorry +instance ResultMonad : Monad Result where + pure := Result.pure + bind := Result.bind + +instance : LawfulMonad Result where + id_map x := by + dsimp [id, Functor.map] + cases x; + all_goals grind + map_const := by + intros α β + dsimp [Functor.map, Functor.mapConst] + seqLeft_eq x y := by + dsimp [Functor.map, SeqLeft.seqLeft, Seq.seq] + cases x ; all_goals cases y + all_goals try simp + seqRight_eq x y := by + dsimp [Functor.map, SeqRight.seqRight, Seq.seq] + cases x ; all_goals cases y + all_goals try simp + pure_seq g x := by + dsimp [Functor.map, Seq.seq, pure] + bind_pure_comp f x := by + dsimp [Functor.map] + cases x ; all_goals dsimp [bind, pure] + bind_map f x := by + dsimp [Functor.map, bind, pure, Seq.seq] + pure_bind x f := by + dsimp [pure, bind] + bind_assoc x f g := by + dsimp [pure, bind] + cases x; all_goals simp + +-- set_option pp.coercions false +instance Result.instWP : WP Result (.except Error .pure) where + wp x := match x with + | .ok v => wp (Pure.pure v : Except Error _) + | .fail e => wp (throw e : Except Error _) + | .div => PredTrans.const ⌜False⌝ + +-- set_option pp.raw true +instance Result.instWPMonad : WPMonad Result (.except Error .pure) where + wp_pure := by intros; ext Q; simp [wp, PredTrans.pure, Pure.pure, Except.pure, Id.run] + wp_bind x f := by + simp only [instWP] + ext Q + cases x <;> simp [PredTrans.bind, PredTrans.const, Bind.bind] + + + +instance : Coe α (Result α) where + coe x := pure x + -- Logic -abbrev hax_logical_op_and := (fun a b => a ∧ b) +abbrev hax_logical_op_and := (fun a b => a && b) -- Integer types -abbrev u8 := Nat -- to fix -abbrev i8 := Int -- to fix +abbrev u8 := UInt8 abbrev u16 := UInt16 abbrev u32 := UInt32 abbrev u64 := UInt64 abbrev usize := USize +abbrev i8 := Int8 abbrev i16 := Int16 abbrev i32 := Int32 abbrev i64 := Int64 abbrev isize := ISize --- Coercions between integers types: -instance : Coe i32 i64 where - coe x := x.toInt64 +class ToNat (α: Type) where + toNat : α -> Nat + +-- should use a macro here +instance : ToNat USize where + toNat x := x.toNat +instance : ToNat u64 where + toNat x := x.toNat +instance : ToNat u32 where + toNat x := x.toNat +instance : ToNat u16 where + toNat x := x.toNat +instance : ToNat Nat where + toNat x := x + +instance : Coe i32 (Result i64) where + coe x := pure (x.toInt64) -instance : Coe i64 i32 where - coe x := x.toInt32 +instance : Coe i64 (Result i32) where + coe x := pure (Int64.toInt32 x) -instance : Coe USize Nat where +instance : Coe u32 Nat where coe x := x.toNat -instance : Coe (BitVec 32) u32 where - coe x := UInt32.ofBitVec x +instance : Coe Nat usize where + coe x := USize.ofNat x -instance {n} : CoeOut (BitVec n) (Result u32) where - coe x := match n with - | 32 => .ok (UInt32.ofBitVec x) - | _ => .fail (integerOverflow) +instance : Coe USize UInt32 where + coe x := x.toUInt32 -instance : Coe u32 (BitVec 32) where - coe x := x.toBitVec +instance : Coe USize (Result u32) where + coe x := if h: x.toNat < UInt32.size then pure (x.toUInt32) + else Result.fail .integerOverflow + +instance {β} : Coe (α -> usize -> β) (α -> Nat -> β) where + coe f a x := f a (USize.ofNat x) +instance {β} : Coe (α -> i32 -> β) (α -> Nat -> β) where + coe f a x := f a (Int32.ofNat x) + +instance : OfNat (Result Nat) n where + ofNat := pure (n) -instance : Coe u32 Nat where - coe x := x.toNat -- Arithmetic section Arithmetic -- Overflowing operations @[simp] -def hax_machine_int_add {α} [Add α] (x y: α) := x + y +def hax_machine_int_add {α} [Add α] (x y: α) := Result.pure (x + y) +@[simp] +def hax_machine_int_sub {α} [Sub α] (x y: α) := Result.pure (x - y) @[simp] -def hax_machine_int_sub {α} [Sub α] (x y: α) := x - y +def hax_machine_int_mul {α} [Mul α] (x y: α) := Result.pure (x * y) @[simp] -def hax_machine_int_mul {α} [Mul α] (x y: α) := x * y +def hax_machine_int_div {α} [Div α] (x y: α) := Result.pure (x / y) @[simp] -def hax_machine_int_rem {α} [Mod α] (x y: α) := x % y +def hax_machine_int_rem {α} [Mod α] (x y: α) := Result.pure (x % y) @[simp] -def hax_machine_int_shr {α β γ} [HShiftRight α β γ] (a: α) (b: β) : γ := a >>> b +def hax_machine_int_shr {α β γ} [HShiftRight α β γ] (a: α) (b: β) : Result γ := Result.pure (a >>> b) @[simp] -def hax_machine_int_bitxor {α} [Xor α] (a b: α) : α := a ^^^ b +def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := Result.pure (a ^^^ b) @[simp] -def ops_arith_Neg_neg {α} [Neg α] (x:α) := -x +def ops_arith_Neg_neg {α} [Neg α] (x:α) := Result.pure (-x) @[simp] def hax_machine_int_eq {α} (x y: α) [BEq α] : Bool := x == y @@ -104,6 +182,7 @@ def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Bool := @[simp] def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Bool := x > y + abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize (lo: USize) (hi: USize) := USize -- {u : usize // lo ≤ u ∧ u ≤ hi} @@ -131,106 +210,233 @@ set_option pp.coercions false -- Wrapping operations @[simp] -def num_impl_wrapping_add {α} [Add α] (x y: α) := x + y +def num_impl_wrapping_add {α} [Add α] (x y: α) := Result.pure (x + y) + + +class RotateLeft (α: Type) where + rotateLeft : α -> Nat -> α + +instance {w} : RotateLeft (BitVec w) where + rotateLeft x n := BitVec.rotateLeft x n + +instance : RotateLeft usize where + rotateLeft x n := USize.ofBitVec (BitVec.rotateLeft x.toBitVec n) + +instance : RotateLeft u32 where + rotateLeft x n := UInt32.ofBitVec (BitVec.rotateLeft x.toBitVec n) @[simp] -def num_impl_rotate_left {w} := @BitVec.rotateLeft w +def num_impl_rotate_left {α} [r: RotateLeft α] (x: α) (n: Nat) : Result α := + Result.pure (r.rotateLeft x n) end Arithmetic -- Tuples -structure hax_Tuple2_arg (α β: Type) where -hax_Tuple2_Tuple0 : α -hax_Tuple2_Tuple1 : β -inductive hax_Tuple2 (α β: Type) -| constr_hax_Tuple2 : (hax_Tuple2_arg α β) -> hax_Tuple2 α β +def hax_Tuple0 : Type := Unit +def constr_hax_Tuple0 : hax_Tuple0 := () +instance : Coe hax_Tuple0 Unit where + coe _ := () + + +def hax_Tuple1 (α: Type) : Type := α × Unit +def constr_hax_Tuple1 {hax_Tuple1_Tuple0: α} : hax_Tuple1 α := (hax_Tuple1_Tuple0, ()) + +def hax_Tuple2 (α β: Type) : Type := α × β +def constr_hax_Tuple2 {α β} {hax_Tuple2_Tuple0: α} {hax_Tuple2_Tuple1 : β} : hax_Tuple2 α β + := (hax_Tuple2_Tuple0, hax_Tuple2_Tuple1) + -abbrev hax_Tuple0 := () -- Nums -def num_impl_from_le_bytes {α} : (Array α) -> u32 := sorry +-- TO remove once name display is fixed + +def num_impl_from_le_bytes {α} (x: Vector α n) : u32 := (0: u32) -- TOFIX -- Casts @[simp] -def convert_From_from {α β} [Coe α β] (x:α) : β := x +def convert_From_from {α β} [Coe α (Result β)] (x:α) : (Result β) := x @[simp] -def hax_cast_op {α β} [Coe α β] (x:α) : β := x +def hax_cast_op {α β} [Coe α (Result β)] (x:α) : (Result β) := x -- Results inductive result_Result α β | ok : α -> result_Result α β | err : β -> result_Result α β -axiom array_TryFromSliceError : Type +instance {β : Type} : Monad (fun α => result_Result α β) where + pure x := .ok x + bind {α α'} x (f: α -> result_Result α' β) := match x with + | .ok v => f v + | .err e => .err e + +inductive array_TryFromSliceError where + | array_TryFromSliceError -- Assert def assert (b:Bool) : Result Unit := if b then pure () else .fail (Error.assertionFailure) -def assume : Prop -> Unit := fun _ => () -def prop_constructors_from_bool : Bool -> Prop := sorry +def assume : Prop -> Result Unit := fun _ => pure () +def prop_constructors_from_bool (b :Bool) : Prop := (b = true) -- Hax + +-- To extend with invariants def hax_folds_fold_range {α} (s e : Nat) - (_filter : α -> Nat -> Bool) + (_inv : α -> Nat -> Result Bool) (init: α) - (f : α -> Nat -> Result α) := + (f : α -> Nat -> Result α) : Result α := Array.foldlM f init (Array.range e) s e -- Arrays -def hax_monomorphized_update_at_update_at_usize {α} - (a: Array α) (i:Nat) (v:α) : Result (Array α) := +def hax_monomorphized_update_at_update_at_usize {α n} + (a: Vector α n) (i:Nat) (v:α) : Result (Vector α n) := if h: i < a.size then - pure ( Array.set a i v ) + pure ( Vector.set a i v ) else .fail (.arrayOutOfBounds) def hax_update_at {α n} (m : Vector α n) (i : Nat) (v : α) : Result (Vector α n) := if i < n then - .ok ( Vector.setIfInBounds m i v) + pure ( Vector.setIfInBounds m i v) else .fail (.arrayOutOfBounds) -def result_impl_unwrap {α} : α -> Array β := sorry +def result_impl_unwrap (α: Type) (β:Type) (x: result_Result α β) : (Result α) := + match x with + | .ok v => pure v + | .err _ => .fail .panic -- Vectors -def hax_repeat (x:Nat) (y:Nat) : Array u32 := sorry +def hax_repeat {α} (v:α) (n:Nat) : Result (Vector α n) := + pure (Eq.mp (congrArg (Vector α) (@Array.size_replicate α n v)) + (Array.replicate n v).toVector) -- Ranges -structure ops_range_Range_arg (α: Type) where -ops_range_Range_start : α -ops_range_Range_end : α - inductive ops_range_Range (α: Type) where -| constr_ops_range_Range : ops_range_Range_arg α -> ops_range_Range α - - +| constr_ops_range_Range + {ops_range_Range_start: α} + {ops_range_Range_end: α} : ops_range_Range α + +def constr_ops_range_Range {α} {ops_range_Range_start : α} {ops_range_Range_end : α} := + ops_range_Range.constr_ops_range_Range + (ops_range_Range_start := ops_range_Range_start) + (ops_range_Range_end := ops_range_Range_end) + +def ops_index_Index_index {α β γ} (a: α) (i:β) + [GetElem α β (Result γ) (fun _ _ => True) ] : (Result γ) := a[i] + +instance : + GetElem + (Array α) + (ops_range_Range usize) + (Result (Array α)) (fun _ _ => True) where + getElem xs i _ := match i with + | @ops_range_Range.constr_ops_range_Range _ s e => + let size := xs.size; + if (s > e || e > size || s > size) then + Result.fail Error.arrayOutOfBounds + else + pure ( xs.extract s e ) + +instance {α n} [tn: ToNat β]: + GetElem + (Vector α n) + (ops_range_Range β) + (Result (Array α)) (fun _ _ => True) where + getElem xs i _ := match i with + | @ops_range_Range.constr_ops_range_Range _ s e => + let e := tn.toNat e; + let s := tn.toNat s; + let size := xs.size; + if (s > e || e > size || s > size) then + Result.fail Error.arrayOutOfBounds + else + pure ( (Vector.extract xs s e ).toArray) + + +instance GetElemResult [tn: ToNat β] : GetElem (Array α) β (Result α) (fun _ _ => True) where + getElem xs i _ := match xs[tn.toNat i]? with + | .some v => pure v + | .none => Result.fail .arrayOutOfBounds + +instance : GetElem (Array α) usize (Result α) (fun _ _ => True) := + GetElemResult +instance : GetElem (Array α) Nat (Result α) (fun _ _ => True) := + GetElemResult + +instance {α β : Type} {n : Nat} [tn: ToNat β]: GetElem (Vector α n) β (Result α) (fun _ _ => True) where + getElem xs i _ := match xs[tn.toNat i]? with + | .some v => pure v + | .none => Result.fail (.arrayOutOfBounds) + +instance {α : Type} {n : Nat}: GetElem (Vector α n) Nat (Result α) (fun _ _ => True) where + getElem xs i _ := match xs[i]? with + | .some v => pure v + | .none => Result.fail (.arrayOutOfBounds) -- Arrays section Arrays -def ops_index_Index_index (a: Array α) (i:Nat) : Result α := - match a[i]? with - | .none => .fail arrayOutOfBounds - | .some v => .ok v -def convert_TryInto_try_into {α} : Array α -> - result_Result (Array α) array_TryFromSliceError := sorry - -instance {α n} : CoeOut (Vector α n) (Array α) where - coe x := x.toArray - -instance {α β} [i:Coe α β]: Coe (Array α) (Array β) where - coe x := Array.map i.coe x +def convert_TryInto_try_into {α n} (a: Array α) : + Result (result_Result (Vector α n) array_TryFromSliceError) := + pure ( + if h: a.size = n then + result_Result.ok (Eq.mp (congrArg _ h) a.toVector) + else + .err .array_TryFromSliceError + ) end Arrays + -- Slices -def slice_impl_len (a: Array u32) : Nat := sorry +def alloc_Global : Type := Unit + +def unsize {α n} (a: Vector α n) : Result (Array α) := + pure (a.toArray) + +def slice_impl_len α (a: Array α) : Nat := a.size +def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α + +def vec_impl_new (α: Type) (Allocator:Type) : Result (vec_Vec α Allocator) := + Result.pure ((List.nil).toArray) + +def vec_impl_len (α: Type) (Allocator:Type) (x: vec_Vec α Allocator) : Result Nat := + Result.pure x.size + +def vec_impl_extend_from_slice (α Allocator) (x: vec_Vec α Allocator) (y: Array α) + : Result (vec_Vec α Allocator):= + pure (x.append y) + +def slice_impl_to_vec {β} α (a: Array α) : Result (vec_Vec α β) := + pure a + +-- For +instance {α n} : Coe (Array α) (Result (Vector α n)) where + coe x := + if h: x.size = n then by + rw [←h] + apply Result.pure + apply (Array.toVector x) + else .fail (.arrayOutOfBounds) + -- Bytes -def num_impl_to_le_bytes : u32 -> Array u8 := sorry +def num_impl_to_le_bytes (_:u32) : Result (Vector u8 4) := + pure (#v[0, 0, 0, 0]) -- TOFIX + + +-- Closures +def ops_function_Fn_call {α β} (f: α -> β) (x: α) := f x + + +-- Miscellaneous +def ops_deref_Deref_deref {α Allocator} (v: vec_Vec α Allocator) + : Result (Array α) + := pure v diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 9822d98b1..4c48801a6 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -6,7 +6,6 @@ use crate::ast::span::Span; use crate::printer::Allocator; -use std::iter::once; use pretty::{docs, DocAllocator, DocBuilder, Pretty}; @@ -47,20 +46,33 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { } ItemKind::Fn { name, - generics: _, + generics, body, params, safety: _, } => { - // Generics are ignored for now - + let generics = if generics.params.is_empty() { + None + } else { + Some( + docs![ + allocator, + allocator.line(), + allocator + .intersperse(&generics.params, allocator.softline()) + .braces() + .group() + ] + .group(), + ) + }; let args = if params.is_empty() { allocator.nil() } else { docs![ allocator, - allocator.softline(), - allocator.intersperse(params, allocator.line()), + allocator.line(), + allocator.intersperse(params, allocator.softline()), ] .nest(INDENT) .group() @@ -69,9 +81,16 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { allocator, "def ", name, + generics, args, - docs![allocator, allocator.line(), ": ", &body.ty].group(), - " :=", + docs![ + allocator, + allocator.line(), + ": ", + docs![allocator, "Result ", &body.ty].group() + ] + .group(), + " := do", allocator.line(), docs![allocator, &*body.kind].group() ] @@ -146,12 +165,13 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b TyKind { .group() } } - TyKind::Arrow { inputs, output } => allocator - .intersperse( - inputs.into_iter().chain(once(output)), - allocator.softline().append("-> "), - ) - .parens(), + TyKind::Arrow { inputs, output } => docs![ + allocator, + allocator.intersperse(inputs.into_iter(), allocator.reflow(" -> ")), + "Result", + output + ] + .parens(), TyKind::Ref { inner: _, mutable: _, @@ -161,8 +181,8 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b TyKind { TyKind::Slice(ty) => docs![allocator, "Array ", ty].parens(), TyKind::Array { ty, length } => { docs![allocator, "Vector ", ty, allocator.softline(), &(**length),] - .group() .parens() + .group() } TyKind::RawPointer => print_todo!(allocator), TyKind::AssociatedType { impl_: _, item: _ } => print_todo!(allocator), @@ -200,7 +220,14 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Expr { impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Pat { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - (self.kind).pretty(allocator) + docs![ + allocator, + self.kind.pretty(allocator), + allocator.reflow(" : "), + &self.ty + ] + .parens() + .group() } } @@ -208,11 +235,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b PatKind { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { match self { PatKind::Wild => allocator.text("_"), - PatKind::Ascription { pat, ty } => { - docs![allocator, pat, allocator.softline(), ": ", ty] - .nest(INDENT) - .group() - } + PatKind::Ascription { pat, ty: _ } => pat.kind.pretty(allocator), PatKind::Or { sub_pats: _ } => print_todo!(allocator), PatKind::Array { args: _ } => print_todo!(allocator), PatKind::Deref { sub_pat: _ } => print_todo!(allocator), @@ -252,35 +275,60 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { then, else_, } => match else_ { - Some(else_branch) => allocator - .concat([ - allocator.text("if"), - allocator.softline().append(condition).nest(INDENT), - allocator.line().append("then"), - allocator.softline().append(then).nest(INDENT), - allocator.line().append("else"), - allocator.softline().append(else_branch).nest(INDENT), - ]) - .group(), + Some(else_branch) => docs![ + allocator, + docs![allocator, "if", allocator.line(), condition].group(), + allocator.line(), + docs![allocator, "then", allocator.line(), then] + .group() + .nest(INDENT), + allocator.line(), + docs![allocator, "else", allocator.line(), else_branch] + .group() + .nest(INDENT), + ] + .group(), None => print_todo!(allocator), }, ExprKind::App { head, args, - generic_args: _, + generic_args, bounds_impls: _, trait_: _, } => { - head.pretty(allocator) - .append(allocator.softline()) - .append(allocator.intersperse(args, allocator.softline()).nest(INDENT)) - .group() + let generic_args = if generic_args.is_empty() { + None + } else { + Some( + allocator + .line() + .append( + allocator + .intersperse(generic_args, allocator.line()) + .nest(INDENT), + ) + .group(), + ) + }; + let args = if args.is_empty() { + None + } else { + Some( + allocator + .line() + .append(allocator.intersperse(args, allocator.line()).nest(INDENT)) + .group(), + ) + }; + docs![allocator, "← ", head, generic_args, args] .parens() + .group() } ExprKind::Literal(literal) => literal.pretty(allocator), ExprKind::Array(exprs) => docs![ allocator, - "#[", + "#v[", allocator .intersperse(exprs, allocator.text(",").append(allocator.line())) .nest(INDENT), @@ -297,31 +345,40 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { // Should be turned into a resugaring once https://github.com/cryspen/hax/pull/1528 have been merged let record_args = if fields.len() > 0 { Some( - allocator.softline().append( - allocator - .intersperse( - fields.iter().map(|field: &(GlobalId, Expr)| { - docs![ - allocator, - &field.0, - " ", - allocator.reflow(":= "), - &field.1 - ] - .group() - }), - allocator.reflow(", "), - ) - .group() - .braces(), - ), + allocator + .line() + .append( + allocator + .intersperse( + fields.iter().map(|field: &(GlobalId, Expr)| { + docs![ + allocator, + &field.0, + allocator.reflow(" := "), + &field.1 + ] + .parens() + .group() + }), + allocator.line(), + ) + .group(), + ) + .group(), ) } else { None }; - docs![allocator, ".constr_", constructor, record_args] - .group() - .nest(INDENT) + docs![ + allocator, + "constr_", + constructor, + allocator.softline(), + record_args + ] + .parens() + .group() + .nest(INDENT) } ExprKind::Match { scrutinee: _, @@ -337,25 +394,31 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { inner: _, } => print_todo!(allocator), ExprKind::Deref(_expr) => print_todo!(allocator), - ExprKind::Let { lhs, rhs, body } => { - docs![ - allocator, - "let ", - lhs, - " :=", - allocator.softline(), - docs![allocator, rhs].group(), - ";", - allocator.line(), - body, - ] - } + ExprKind::Let { lhs, rhs, body } => docs![ + allocator, + "let ", + lhs, + " ←", + docs![allocator, allocator.line(), "pure", allocator.line(), rhs] + .group() + .nest(INDENT), + ";", + allocator.line(), + body, + ] + .group(), ExprKind::GlobalId(global_id) => global_id.pretty(allocator), ExprKind::LocalId(local_id) => local_id.pretty(allocator), - ExprKind::Ascription { e, ty } => docs![allocator, e, allocator.reflow(" : "), ty] - .nest(INDENT) - .group() - .parens(), + ExprKind::Ascription { e, ty } => { + let monadic_encoding = match *e.kind { + ExprKind::Literal(_) | ExprKind::Construct { .. } => None, + _ => Some("← "), + }; + docs![allocator, monadic_encoding, e, allocator.reflow(" : "), ty] + //.nest(INDENT) + .parens() + .group() + } ExprKind::Assign { lhs: _, value: _ } => print_todo!(allocator), ExprKind::Loop { body: _, @@ -373,15 +436,16 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { captures: _, } => docs![ allocator, - allocator.line_(), allocator.reflow("fun "), - allocator.intersperse(params, allocator.line()).group(), - allocator.reflow(" => "), + allocator.intersperse(params, allocator.softline()).group(), + allocator.reflow("=> do"), + allocator.line(), body ] //.nest(INDENT) + .parens() .group() - .parens(), + .nest(INDENT), ExprKind::Block { body: _, safety_mode: _, @@ -473,9 +537,12 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b GlobalId { impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Param { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - docs![allocator, &self.pat, allocator.softline(), ": ", &self.ty] - .nest(INDENT) - .group() - .parens() + self.pat.pretty(allocator) + } +} + +impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b GenericParam { + fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { + self.ident.pretty(allocator) } } diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index 5cb31301e..51d89a6b8 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -24,3 +24,14 @@ fn closure() -> i32 { } type UsizeAlias = usize; + +// Hello world example from https://hacspec.zulipchat.com/#narrow/channel/269544-general/topic/hax.20.2B.20coq/with/528801096 +fn main() { + let x = square(10u8); + println!("{}", x); +} + +#[hax_lib::requires(n < 16u8)] +fn square(n: u8) -> u8 { + n * n +} From 730eabaa9276b73bcb52b28be80f652e3934db72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 24 Jul 2025 12:05:27 +0200 Subject: [PATCH 08/44] Add Result.ofOption and @[spec] attributes --- hax-lib/proof-libs/lean/Lib.lean | 78 +++++++++++++++++++------------- 1 file changed, 47 insertions(+), 31 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index bc1e9748d..e40be3ee5 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -1,5 +1,4 @@ -- This library provides a monadic encoding over Hax primitives --- Aeneas errors import Std.Tactic.Do import Std.Do.Triple import Std.Tactic.Do.Syntax @@ -8,6 +7,7 @@ import Std open Std.Do open Std.Tactic +-- Aeneas errors inductive Error where | assertionFailure: Error | integerOverflow: Error @@ -27,7 +27,11 @@ inductive Result.{u} (α : Type u) where deriving Repr, BEq @[simp] -def Result.pure (x:α) : Result α := .ok x +instance Result.instPure: Pure Result where + pure x := .ok x + +@[simp, spec] +def Result.pure (x: α) : Result α := (Result.instPure.pure x) @[simp] def Result.bind (x: Result α) (f: α -> Result β) := match x with @@ -35,40 +39,47 @@ def Result.bind (x: Result α) (f: α -> Result β) := match x with | .fail e => .fail e | .div => .div -instance ResultMonad : Monad Result where - pure := Result.pure +@[simp] +def Result.ofOption {α} (x:Option α) (e: Error) : Result α := match x with + | .some v => pure v + | .none => .fail e + +@[simp] +instance Result.instMonad : Monad Result where + pure := pure bind := Result.bind -instance : LawfulMonad Result where +@[simp] +instance Result.instLawfulMonad : LawfulMonad Result where id_map x := by - dsimp [id, Functor.map] + dsimp [id, Functor.map, Result.pure] cases x; all_goals grind map_const := by intros α β dsimp [Functor.map, Functor.mapConst] seqLeft_eq x y := by - dsimp [Functor.map, SeqLeft.seqLeft, Seq.seq] + dsimp [Functor.map, SeqLeft.seqLeft, Seq.seq, Result.pure] cases x ; all_goals cases y all_goals try simp seqRight_eq x y := by - dsimp [Functor.map, SeqRight.seqRight, Seq.seq] + dsimp [Functor.map, SeqRight.seqRight, Seq.seq, Result.pure] cases x ; all_goals cases y all_goals try simp pure_seq g x := by - dsimp [Functor.map, Seq.seq, pure] + dsimp [Functor.map, Seq.seq, pure, Result.pure] bind_pure_comp f x := by dsimp [Functor.map] - cases x ; all_goals dsimp [bind, pure] bind_map f x := by - dsimp [Functor.map, bind, pure, Seq.seq] + dsimp [Functor.map, bind, pure, Seq.seq, Result.pure] pure_bind x f := by - dsimp [pure, bind] + dsimp [pure, bind, Result.pure] bind_assoc x f g := by dsimp [pure, bind] cases x; all_goals simp -- set_option pp.coercions false +@[simp] instance Result.instWP : WP Result (.except Error .pure) where wp x := match x with | .ok v => wp (Pure.pure v : Except Error _) @@ -76,8 +87,9 @@ instance Result.instWP : WP Result (.except Error .pure) where | .div => PredTrans.const ⌜False⌝ -- set_option pp.raw true +@[simp] instance Result.instWPMonad : WPMonad Result (.except Error .pure) where - wp_pure := by intros; ext Q; simp [wp, PredTrans.pure, Pure.pure, Except.pure, Id.run] + wp_pure := by intros; ext Q; simp [wp, PredTrans.pure, Pure.pure, Except.pure, Id.run, Result.pure] wp_bind x f := by simp only [instWP] ext Q @@ -88,9 +100,9 @@ instance Result.instWPMonad : WPMonad Result (.except Error .pure) where instance : Coe α (Result α) where coe x := pure x - -- Logic abbrev hax_logical_op_and := (fun a b => a && b) +abbrev hax_logical_op_or := (fun a b => a || b) -- Integer types @@ -120,30 +132,40 @@ instance : ToNat u16 where instance : ToNat Nat where toNat x := x +@[simp] instance : Coe i32 (Result i64) where coe x := pure (x.toInt64) +@[simp] instance : Coe i64 (Result i32) where coe x := pure (Int64.toInt32 x) +@[simp] instance : Coe u32 Nat where coe x := x.toNat +@[simp] instance : Coe Nat usize where coe x := USize.ofNat x +@[simp] instance : Coe USize UInt32 where coe x := x.toUInt32 +@[simp] instance : Coe USize (Result u32) where coe x := if h: x.toNat < UInt32.size then pure (x.toUInt32) else Result.fail .integerOverflow +@[simp] instance {β} : Coe (α -> usize -> β) (α -> Nat -> β) where coe f a x := f a (USize.ofNat x) + +@[simp] instance {β} : Coe (α -> i32 -> β) (α -> Nat -> β) where coe f a x := f a (Int32.ofNat x) +@[simp] instance : OfNat (Result Nat) n where ofNat := pure (n) @@ -152,17 +174,17 @@ instance : OfNat (Result Nat) n where section Arithmetic -- Overflowing operations -@[simp] -def hax_machine_int_add {α} [Add α] (x y: α) := Result.pure (x + y) -@[simp] +@[simp, spec] +def hax_machine_int_add {α} [Add α] (x y: α) : Result α := pure (x + y) +@[simp, spec] def hax_machine_int_sub {α} [Sub α] (x y: α) := Result.pure (x - y) -@[simp] +@[simp, spec] def hax_machine_int_mul {α} [Mul α] (x y: α) := Result.pure (x * y) -@[simp] +@[simp, spec] def hax_machine_int_div {α} [Div α] (x y: α) := Result.pure (x / y) -@[simp] +@[simp,spec] def hax_machine_int_rem {α} [Mod α] (x y: α) := Result.pure (x % y) -@[simp] +@[simp, spec] def hax_machine_int_shr {α β γ} [HShiftRight α β γ] (a: α) (b: β) : Result γ := Result.pure (a >>> b) @[simp] def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := Result.pure (a ^^^ b) @@ -256,7 +278,7 @@ def num_impl_from_le_bytes {α} (x: Vector α n) : u32 := (0: u32) -- TOFIX -- Casts @[simp] def convert_From_from {α β} [Coe α (Result β)] (x:α) : (Result β) := x -@[simp] +@[simp, spec] def hax_cast_op {α β} [Coe α (Result β)] (x:α) : (Result β) := x -- Results @@ -362,9 +384,7 @@ instance {α n} [tn: ToNat β]: instance GetElemResult [tn: ToNat β] : GetElem (Array α) β (Result α) (fun _ _ => True) where - getElem xs i _ := match xs[tn.toNat i]? with - | .some v => pure v - | .none => Result.fail .arrayOutOfBounds + getElem xs i _ := Result.ofOption (xs[tn.toNat i]?) .arrayOutOfBounds instance : GetElem (Array α) usize (Result α) (fun _ _ => True) := GetElemResult @@ -372,14 +392,10 @@ instance : GetElem (Array α) Nat (Result α) (fun _ _ => True) := GetElemResult instance {α β : Type} {n : Nat} [tn: ToNat β]: GetElem (Vector α n) β (Result α) (fun _ _ => True) where - getElem xs i _ := match xs[tn.toNat i]? with - | .some v => pure v - | .none => Result.fail (.arrayOutOfBounds) + getElem xs i _ := Result.ofOption (xs[tn.toNat i]?) .arrayOutOfBounds instance {α : Type} {n : Nat}: GetElem (Vector α n) Nat (Result α) (fun _ _ => True) where - getElem xs i _ := match xs[i]? with - | .some v => pure v - | .none => Result.fail (.arrayOutOfBounds) + getElem xs i _ := Result.ofOption xs[i]? .arrayOutOfBounds -- Arrays section Arrays From c5f8164bb256c4bd6f57e3ce328f00f8d945af34 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 24 Jul 2025 12:06:02 +0200 Subject: [PATCH 09/44] Have arithmetic operations panicking + new notation (+?) --- hax-lib/proof-libs/lean/Lib.lean | 189 +++++++++++++++++++++++++++---- 1 file changed, 166 insertions(+), 23 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index e40be3ee5..346396a39 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -95,9 +95,7 @@ instance Result.instWPMonad : WPMonad Result (.except Error .pure) where ext Q cases x <;> simp [PredTrans.bind, PredTrans.const, Bind.bind] - - -instance : Coe α (Result α) where +instance Result.instCoe {α} : Coe α (Result α) where coe x := pure x -- Logic @@ -132,14 +130,10 @@ instance : ToNat u16 where instance : ToNat Nat where toNat x := x -@[simp] +@[simp, spec] instance : Coe i32 (Result i64) where coe x := pure (x.toInt64) -@[simp] -instance : Coe i64 (Result i32) where - coe x := pure (Int64.toInt32 x) - @[simp] instance : Coe u32 Nat where coe x := x.toNat @@ -173,23 +167,164 @@ instance : OfNat (Result Nat) n where -- Arithmetic section Arithmetic +/-- +The notation typeclass for homogeneous addition that returns a Result. +This enables the notation `a +? b : α` where `a : α`, `b : α`. For now, there is +no heterogeneous version +-/ +class HaxAdd α where + /-- `a +? b` computes the panicking sum of `a` and `b`. + The meaning of this notation is type-dependent. -/ + add : α → α → Result α + +@[inherit_doc] infixl:65 " +? " => HaxAdd.add + +/-- +The notation typeclass for homogeneous substraction that returns a Result. +This enables the notation `a -? b : α` where `a : α`, `b : α`. For now, there is +no heterogeneous version +-/ +class HaxSub α where + /-- `a -? b` computes the panicking substraction of `a` and `b`. + The meaning of this notation is type-dependent. -/ + sub : α → α → Result α + +@[inherit_doc] infixl:65 " -? " => HaxSub.sub + +/-- +The notation typeclass for homogeneous multiplication that returns a Result. +This enables the notation `a *? b : α` where `a : α`, `b : α`. For now, there is +no heterogeneous version +-/ +class HaxMul α where + /-- `a -? b` computes the panicking multiplication of `a` and `b`. + The meaning of this notation is type-dependent. -/ + mul : α → α → Result α + +@[inherit_doc] infixl:70 " *? " => HaxMul.mul + +/-- The typeclass behind the notation `a >>>? b : α` where `a b : α`. -/ +class HaxShiftRight α where + /-- `a >>>? b` computes the panicking right-shift of `a` by `b`. The meaning + of this notation is type-dependent. It panics if `b` exceeds the size of + `a`. -/ + shiftRight : α → α → Result α + +@[inherit_doc] infixl:75 " >>>? " => HaxShiftRight.shiftRight + +namespace Int64 + +instance instHaxAdd : HaxAdd Int64 where + add x y := + if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x + y) + +@[spec] +theorem HaxAdd_spec_bv (x y: i64) : + ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄ + (x +? y) + ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ] + +instance instHaxSub : HaxSub Int64 where + sub x y := + if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x - y) + +@[spec] +theorem HaxSub_spec_bv (x y: i64) : + ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄ + (x -? y) + ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub] + +instance instHaxMul : HaxMul Int64 where + mul x y := + if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x * y) + +@[spec] +theorem HaxMul_spec_bv (x y: i64) : + ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄ + (x *? y) + ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul] + +instance instHaxShiftRight : HaxShiftRight Int64 where + shiftRight x y := + if (y ≤ 32) then pure (x >>> y) + else .fail .integerOverflow + +@[spec] +theorem HaxShiftRight_spec_bv (x y: i64) : + ⦃ y ≤ 32 ⦄ + ( x >>>? y) + ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight] + +end Int64 + +namespace Int32 + +instance instHaxAdd : HaxAdd Int32 where + add x y := + if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x + y) + +@[spec] +theorem HaxAdd_spec_bv (x y: i32) : + ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄ + (x +? y) + ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ] + +-- @[spec] +-- theorem HaxAdd_spec_Int (x y: i32) : +-- ⦃ x.toInt + y.toInt < Int32.maxValue.toInt ⦄ +-- (x +? y : Result i32) +-- ⦃ ⇓ r => r = x + y ⦄ +-- := by +-- mvcgen [Int32.instHaxAdd ] +-- cases h__overflow : ((toBitVec x).saddOverflow (toBitVec y)) <;> try simp +-- have := @BitVec.toInt_add_of_not_saddOverflow _ (x.toBitVec) (y.toBitVec) +-- simp [] + +instance instHaxSub : HaxSub Int32 where + sub x y := + if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x - y) + +@[spec] +theorem HaxSub_spec_bv (x y: i32) : + ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄ + (x -? y : Result i32) + ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub] + +instance instHaxMul : HaxMul Int32 where + mul x y := + if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x * y) + +@[spec] +theorem HaxMul_spec_bv (x y: i32) : + ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄ + (x *? y : Result i32) + ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul] + +end Int32 + -- Overflowing operations @[simp, spec] -def hax_machine_int_add {α} [Add α] (x y: α) : Result α := pure (x + y) -@[simp, spec] -def hax_machine_int_sub {α} [Sub α] (x y: α) := Result.pure (x - y) +def hax_machine_int_add {α} [HaxAdd α] (x y: α) : Result α := x +? y @[simp, spec] -def hax_machine_int_mul {α} [Mul α] (x y: α) := Result.pure (x * y) +def hax_machine_int_sub {α} [HaxSub α] (x y: α) : Result α := x -? y @[simp, spec] -def hax_machine_int_div {α} [Div α] (x y: α) := Result.pure (x / y) -@[simp,spec] -def hax_machine_int_rem {α} [Mod α] (x y: α) := Result.pure (x % y) +def hax_machine_int_mul {α} [HaxMul α] (x y: α) : Result α := x *? y +@[simp] +def hax_machine_int_div {α} [Div α] (x y: α) : Result α := pure (x / y) +@[simp] +def hax_machine_int_rem {α} [Mod α] (x y: α) : Result α := pure (x % y) @[simp, spec] -def hax_machine_int_shr {α β γ} [HShiftRight α β γ] (a: α) (b: β) : Result γ := Result.pure (a >>> b) +def hax_machine_int_shr {α} [HaxShiftRight α] (a b: α) : Result α := (a >>>? b) @[simp] def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := Result.pure (a ^^^ b) @[simp] -def ops_arith_Neg_neg {α} [Neg α] (x:α) := Result.pure (-x) +def ops_arith_Neg_neg {α} [Neg α] (x:α) : Result α := pure (-x) @[simp] def hax_machine_int_eq {α} (x y: α) [BEq α] : Bool := x == y @@ -232,7 +367,7 @@ set_option pp.coercions false -- Wrapping operations @[simp] -def num_impl_wrapping_add {α} [Add α] (x y: α) := Result.pure (x + y) +def num_impl_wrapping_add {α} [Add α] (x y: α) : Result α := pure (x + y) class RotateLeft (α: Type) where @@ -249,7 +384,7 @@ instance : RotateLeft u32 where @[simp] def num_impl_rotate_left {α} [r: RotateLeft α] (x: α) (n: Nat) : Result α := - Result.pure (r.rotateLeft x n) + pure (r.rotateLeft x n) end Arithmetic @@ -276,10 +411,18 @@ def constr_hax_Tuple2 {α β} {hax_Tuple2_Tuple0: α} {hax_Tuple2_Tuple1 : β} : def num_impl_from_le_bytes {α} (x: Vector α n) : u32 := (0: u32) -- TOFIX -- Casts -@[simp] +@[simp, spec] def convert_From_from {α β} [Coe α (Result β)] (x:α) : (Result β) := x + +class Cast (α β: Type) where + cast : α → Result β + +@[spec] +instance : Cast i64 i32 where + cast x := pure (Int64.toInt32 x) + @[simp, spec] -def hax_cast_op {α β} [Coe α (Result β)] (x:α) : (Result β) := x +def hax_cast_op {α β} [c: Cast α β] (x:α) : (Result β) := c.cast x -- Results inductive result_Result α β @@ -421,10 +564,10 @@ def slice_impl_len α (a: Array α) : Nat := a.size def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α def vec_impl_new (α: Type) (Allocator:Type) : Result (vec_Vec α Allocator) := - Result.pure ((List.nil).toArray) + pure ((List.nil).toArray) def vec_impl_len (α: Type) (Allocator:Type) (x: vec_Vec α Allocator) : Result Nat := - Result.pure x.size + pure x.size def vec_impl_extend_from_slice (α Allocator) (x: vec_Vec α Allocator) (y: Array α) : Result (vec_Vec α Allocator):= From f8ba7b891674e0540056a9d45beff4a228727799 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 28 Jul 2025 15:34:29 +0200 Subject: [PATCH 10/44] Improvements to arithmetic library --- hax-lib/proof-libs/lean/Lib.lean | 277 ++++++++++++++++++++++++------- 1 file changed, 216 insertions(+), 61 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 346396a39..d862f8e70 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -119,14 +119,19 @@ class ToNat (α: Type) where toNat : α -> Nat -- should use a macro here +@[simp] instance : ToNat USize where toNat x := x.toNat +@[simp] instance : ToNat u64 where toNat x := x.toNat +@[simp] instance : ToNat u32 where toNat x := x.toNat +@[simp] instance : ToNat u16 where toNat x := x.toNat +@[simp] instance : ToNat Nat where toNat x := x @@ -167,50 +172,218 @@ instance : OfNat (Result Nat) n where -- Arithmetic section Arithmetic -/-- -The notation typeclass for homogeneous addition that returns a Result. -This enables the notation `a +? b : α` where `a : α`, `b : α`. For now, there is -no heterogeneous version --/ +/-- The notation typeclass for homogeneous addition that returns a Result. This +enables the notation `a +? b : α` where `a : α`, `b : α`. For now, there is no +heterogeneous version -/ class HaxAdd α where - /-- `a +? b` computes the panicking sum of `a` and `b`. - The meaning of this notation is type-dependent. -/ + /-- `a +? b` computes the panicking sum of `a` and `b`. The meaning of this + notation is type-dependent. -/ add : α → α → Result α -@[inherit_doc] infixl:65 " +? " => HaxAdd.add - -/-- -The notation typeclass for homogeneous substraction that returns a Result. +/-- The notation typeclass for homogeneous substraction that returns a Result. This enables the notation `a -? b : α` where `a : α`, `b : α`. For now, there is -no heterogeneous version --/ +no heterogeneous version -/ class HaxSub α where /-- `a -? b` computes the panicking substraction of `a` and `b`. The meaning of this notation is type-dependent. -/ sub : α → α → Result α -@[inherit_doc] infixl:65 " -? " => HaxSub.sub - -/-- -The notation typeclass for homogeneous multiplication that returns a Result. -This enables the notation `a *? b : α` where `a : α`, `b : α`. For now, there is -no heterogeneous version --/ +/-- The notation typeclass for homogeneous multiplication that returns a Result. +This enables the notation `a *? b : Result α` where `a b : α`. For now, there is +no heterogeneous version -/ class HaxMul α where - /-- `a -? b` computes the panicking multiplication of `a` and `b`. - The meaning of this notation is type-dependent. -/ + /-- `a -? b` computes the panicking multiplication of `a` and `b`. The + meaning of this notation is type-dependent. -/ mul : α → α → Result α -@[inherit_doc] infixl:70 " *? " => HaxMul.mul +/-- The notation typeclass for homogeneous division that returns a Result. This +enables the notation `a /? b : Result α` where `a b : α`. For now, there is no +heterogeneous version -/ +class HaxDiv α where + /-- `a -? b` computes the panicking multiplication of `a` and `b`. The + meaning of this notation is type-dependent. -/ + div : α → α → Result α -/-- The typeclass behind the notation `a >>>? b : α` where `a b : α`. -/ +/-- The typeclass behind the notation `a >>>? b : Result α` where `a b : α`. -/ class HaxShiftRight α where /-- `a >>>? b` computes the panicking right-shift of `a` by `b`. The meaning - of this notation is type-dependent. It panics if `b` exceeds the size of - `a`. -/ + of this notation is type-dependent. It panics if `b` exceeds the size of `a`. + -/ shiftRight : α → α → Result α +/-- The notation typeclass for remainder. This enables the notation `a %? b : +Result α` where `a b : α`. -/ +class HaxRem α where + /-- `a %? b` computes the panicking remainder upon dividing `a` by `b`. The + meaning of this notation is type-dependent. It panics if b is zero -/ + rem : α → α → Result α + +@[inherit_doc] infixl:65 " +? " => HaxAdd.add +@[inherit_doc] infixl:65 " -? " => HaxSub.sub +@[inherit_doc] infixl:70 " *? " => HaxMul.mul @[inherit_doc] infixl:75 " >>>? " => HaxShiftRight.shiftRight +@[inherit_doc] infixl:70 " %? " => HaxRem.rem +@[inherit_doc] infixl:70 " /? " => HaxDiv.div + +-- Overflowing operations +@[simp, spec] +def hax_machine_int_add {α} [HaxAdd α] (x y: α) : Result α := x +? y +@[simp, spec] +def hax_machine_int_sub {α} [HaxSub α] (x y: α) : Result α := x -? y +@[simp, spec] +def hax_machine_int_mul {α} [HaxMul α] (x y: α) : Result α := x *? y +@[simp] +def hax_machine_int_div {α} [HaxDiv α] (x y: α) : Result α := x /? y +@[simp] +def hax_machine_int_rem {α} [HaxRem α] (x y: α) : Result α := x %? y +@[simp, spec] +def hax_machine_int_shr {α} [HaxShiftRight α] (a b: α) : Result α := a >>>? b +@[simp] +def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := Result.pure (a ^^^ b) +@[simp] +def ops_arith_Neg_neg {α} [Neg α] (x:α) : Result α := pure (-x) + +@[simp] +def hax_machine_int_eq {α} (x y: α) [BEq α] : Bool := x == y +@[simp] +def hax_machine_int_ne {α} (x y: α) [BEq α] : Bool := x != y +@[simp] +def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Bool := x < y +@[simp] +def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Bool := x ≤ y +@[simp] +def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Bool := x ≥ y +@[simp] +def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Bool := x > y + + + +namespace USize + +instance instHaxAdd : HaxAdd USize where + add x y := + if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x + y) + +@[spec] +theorem HaxAdd_spec_bv (x y: usize) : + ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄ + (x +? y) + ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ] + +instance instHaxSub : HaxSub USize where + sub x y := + if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x - y) + +@[spec] +theorem HaxSub_spec_bv (x y: usize) : + ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄ + (x -? y) + ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub] + +instance instHaxMul : HaxMul USize where + mul x y := + if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x * y) + +@[spec] +theorem HaxMul_spec_bv (x y: usize) : + ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄ + (x *? y) + ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul] + +instance instHaxShiftRight : HaxShiftRight USize where + shiftRight x y := + if (y ≤ USize.size) then pure (x >>> y) + else .fail .integerOverflow + +@[spec] +theorem HaxShiftRight_spec_bv (x y: usize) : + ⦃ y ≤ USize.size ⦄ + ( x >>>? y) + ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight] + +instance instHaxDiv : HaxDiv usize where + div x y := + if y = 0 then .fail .divisionByZero + else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x / y) + +@[spec] +theorem HaxDiv_spec_bv (x y : usize) : + ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄ + ( x /? y) + ⦃ ⇓ r => r = x / y ⦄ := by + mvcgen [instHaxDiv] <;> simp <;> try grind + have ⟨ _ , h ⟩ := h + apply h; assumption + +instance instHaxRem : HaxRem usize where + rem x y := + if y = 0 then .fail .divisionByZero + else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x % y) + +@[spec] +theorem HaxRem_spec_bv (x y : usize) : + ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄ + ( x %? y) + ⦃ ⇓ r => r = x % y ⦄ := by + mvcgen [instHaxRem] <;> simp <;> try grind + have ⟨ _ , h ⟩ := h + apply h; assumption + + +end USize + +namespace ISize + +instance instHaxAdd : HaxAdd ISize where + add x y := + if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x + y) + +@[spec] +theorem HaxAdd_spec_bv (x y: isize) : + ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄ + (x +? y) + ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ] + +instance instHaxSub : HaxSub ISize where + sub x y := + if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x - y) + +@[spec] +theorem HaxSub_spec_bv (x y: isize) : + ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄ + (x -? y) + ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub] + +instance instHaxMul : HaxMul ISize where + mul x y := + if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x * y) + +@[spec] +theorem HaxMul_spec_bv (x y: isize) : + ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄ + (x *? y) + ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul] + +instance instHaxShiftRight : HaxShiftRight ISize where + shiftRight x y := + if (y ≤ ISize.size.toISize) then pure (x >>> y) + else .fail .integerOverflow + +@[spec] +theorem HaxShiftRight_spec_bv (x y: isize) : + ⦃ y ≤ ISize.size.toISize ⦄ + ( x >>>? y) + ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight] + +end ISize namespace Int64 @@ -249,12 +422,12 @@ theorem HaxMul_spec_bv (x y: i64) : instance instHaxShiftRight : HaxShiftRight Int64 where shiftRight x y := - if (y ≤ 32) then pure (x >>> y) + if (y ≤ 64) then pure (x >>> y) else .fail .integerOverflow @[spec] theorem HaxShiftRight_spec_bv (x y: i64) : - ⦃ y ≤ 32 ⦄ + ⦃ y ≤ 64 ⦄ ( x >>>? y) ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight] @@ -308,37 +481,6 @@ theorem HaxMul_spec_bv (x y: i32) : end Int32 --- Overflowing operations -@[simp, spec] -def hax_machine_int_add {α} [HaxAdd α] (x y: α) : Result α := x +? y -@[simp, spec] -def hax_machine_int_sub {α} [HaxSub α] (x y: α) : Result α := x -? y -@[simp, spec] -def hax_machine_int_mul {α} [HaxMul α] (x y: α) : Result α := x *? y -@[simp] -def hax_machine_int_div {α} [Div α] (x y: α) : Result α := pure (x / y) -@[simp] -def hax_machine_int_rem {α} [Mod α] (x y: α) : Result α := pure (x % y) -@[simp, spec] -def hax_machine_int_shr {α} [HaxShiftRight α] (a b: α) : Result α := (a >>>? b) -@[simp] -def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := Result.pure (a ^^^ b) -@[simp] -def ops_arith_Neg_neg {α} [Neg α] (x:α) : Result α := pure (-x) - -@[simp] -def hax_machine_int_eq {α} (x y: α) [BEq α] : Bool := x == y -@[simp] -def hax_machine_int_ne {α} (x y: α) [BEq α] : Bool := x != y -@[simp] -def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Bool := x < y -@[simp] -def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Bool := x ≤ y -@[simp] -def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Bool := x ≥ y -@[simp] -def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Bool := x > y - abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize (lo: USize) (hi: USize) := USize @@ -369,6 +511,12 @@ set_option pp.coercions false @[simp] def num_impl_wrapping_add {α} [Add α] (x y: α) : Result α := pure (x + y) +@[spec] +theorem num_impl_wrapping_add_spec {α} [Add α] (x y : α) : + ⦃⌜True⌝⦄ + (num_impl_wrapping_add x y) + ⦃ ⇓ r => r = x + y ⦄ +:= by mvcgen [num_impl_wrapping_add] class RotateLeft (α: Type) where rotateLeft : α -> Nat -> α @@ -421,6 +569,10 @@ class Cast (α β: Type) where instance : Cast i64 i32 where cast x := pure (Int64.toInt32 x) +@[spec] +instance : Cast usize u32 where + cast x := pure (USize.toUInt32 x) + @[simp, spec] def hax_cast_op {α β} [c: Cast α β] (x:α) : (Result β) := c.cast x @@ -465,6 +617,7 @@ def hax_monomorphized_update_at_update_at_usize {α n} else .fail (.arrayOutOfBounds) +@[spec] def hax_update_at {α n} (m : Vector α n) (i : Nat) (v : α) : Result (Vector α n) := if i < n then pure ( Vector.setIfInBounds m i v) @@ -525,18 +678,20 @@ instance {α n} [tn: ToNat β]: else pure ( (Vector.extract xs s e ).toArray) - instance GetElemResult [tn: ToNat β] : GetElem (Array α) β (Result α) (fun _ _ => True) where getElem xs i _ := Result.ofOption (xs[tn.toNat i]?) .arrayOutOfBounds -instance : GetElem (Array α) usize (Result α) (fun _ _ => True) := +instance USize.instGetElemArrayResult {α} : GetElem (Array α) (usize) (Result α) (fun _ _ => True) := GetElemResult + instance : GetElem (Array α) Nat (Result α) (fun _ _ => True) := GetElemResult +@[simp] instance {α β : Type} {n : Nat} [tn: ToNat β]: GetElem (Vector α n) β (Result α) (fun _ _ => True) where getElem xs i _ := Result.ofOption (xs[tn.toNat i]?) .arrayOutOfBounds +@[simp] instance {α : Type} {n : Nat}: GetElem (Vector α n) Nat (Result α) (fun _ _ => True) where getElem xs i _ := Result.ofOption xs[i]? .arrayOutOfBounds From 629b57c4942a496cb02c8e3cb81cebf9840adc6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 11:53:27 +0200 Subject: [PATCH 11/44] Reorder imports + Credit Aeneas more clearly --- hax-lib/proof-libs/lean/Lib.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index d862f8e70..0bbdb723a 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -1,13 +1,14 @@ -- This library provides a monadic encoding over Hax primitives -import Std.Tactic.Do +import Std import Std.Do.Triple +import Std.Tactic.Do import Std.Tactic.Do.Syntax -import Std open Std.Do open Std.Tactic -- Aeneas errors +-- see https://github.com/AeneasVerif/aeneas/ inductive Error where | assertionFailure: Error | integerOverflow: Error From 2f0d4258ca7f1ece2d2e6883699492f53b2a9ebf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 11:54:28 +0200 Subject: [PATCH 12/44] Turn comparisons into functions returning Result Bool --- hax-lib/proof-libs/lean/Lib.lean | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 0bbdb723a..f44c73eb0 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -96,6 +96,7 @@ instance Result.instWPMonad : WPMonad Result (.except Error .pure) where ext Q cases x <;> simp [PredTrans.bind, PredTrans.const, Bind.bind] +@[default_instance] instance Result.instCoe {α} : Coe α (Result α) where coe x := pure x @@ -233,9 +234,9 @@ def hax_machine_int_add {α} [HaxAdd α] (x y: α) : Result α := x +? y def hax_machine_int_sub {α} [HaxSub α] (x y: α) : Result α := x -? y @[simp, spec] def hax_machine_int_mul {α} [HaxMul α] (x y: α) : Result α := x *? y -@[simp] +@[simp, spec] def hax_machine_int_div {α} [HaxDiv α] (x y: α) : Result α := x /? y -@[simp] +@[simp, spec] def hax_machine_int_rem {α} [HaxRem α] (x y: α) : Result α := x %? y @[simp, spec] def hax_machine_int_shr {α} [HaxShiftRight α] (a b: α) : Result α := a >>>? b @@ -245,17 +246,17 @@ def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := Result.pure (a def ops_arith_Neg_neg {α} [Neg α] (x:α) : Result α := pure (-x) @[simp] -def hax_machine_int_eq {α} (x y: α) [BEq α] : Bool := x == y +def hax_machine_int_eq {α} (x y: α) [BEq α] : Result Bool := pure (x == y) @[simp] -def hax_machine_int_ne {α} (x y: α) [BEq α] : Bool := x != y +def hax_machine_int_ne {α} (x y: α) [BEq α] : Result Bool := pure (x != y) @[simp] -def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Bool := x < y +def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Result Bool := pure (x < y) @[simp] -def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Bool := x ≤ y +def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Result Bool := pure (x ≤ y) @[simp] -def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Bool := x ≥ y +def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Result Bool := pure (x ≥ y) @[simp] -def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Bool := x > y +def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Result Bool := pure (x > y) From c961b5d9e856d9c8d0c753972faa908d5f9df989 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 11:54:59 +0200 Subject: [PATCH 13/44] Add instance for modulus of i32 --- hax-lib/proof-libs/lean/Lib.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index f44c73eb0..86248ca6f 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -481,6 +481,21 @@ theorem HaxMul_spec_bv (x y: i32) : (x *? y : Result i32) ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul] +instance instHaxRem : HaxRem i32 where + rem x y := + if y = 0 then .fail .divisionByZero + else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow + else pure (x % y) + +@[spec] +theorem HaxRem_spec_bv (x y : i32) : + ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄ + ( x %? y) + ⦃ ⇓ r => r = x % y ⦄ := by + mvcgen [instHaxRem] <;> simp <;> try grind + have ⟨ _ , h ⟩ := h + apply h; assumption + end Int32 From 953d2418ca87e283abecff3e78db6c0afab5f372 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 11:55:42 +0200 Subject: [PATCH 14/44] Display disambiguator in names --- hax-lib/proof-libs/lean/Lib.lean | 41 ++++++++---------------------- rust-engine/src/ast/identifiers.rs | 19 +++++++++----- 2 files changed, 24 insertions(+), 36 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 86248ca6f..3bef53041 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -525,31 +525,12 @@ set_option pp.coercions false -- #check (10: hax__autogenerated_refinement__BoundedUsize_BoundedUsize 0 10) -- Wrapping operations -@[simp] -def num_impl_wrapping_add {α} [Add α] (x y: α) : Result α := pure (x + y) - -@[spec] -theorem num_impl_wrapping_add_spec {α} [Add α] (x y : α) : - ⦃⌜True⌝⦄ - (num_impl_wrapping_add x y) - ⦃ ⇓ r => r = x + y ⦄ -:= by mvcgen [num_impl_wrapping_add] - -class RotateLeft (α: Type) where - rotateLeft : α -> Nat -> α - -instance {w} : RotateLeft (BitVec w) where - rotateLeft x n := BitVec.rotateLeft x n - -instance : RotateLeft usize where - rotateLeft x n := USize.ofBitVec (BitVec.rotateLeft x.toBitVec n) - -instance : RotateLeft u32 where - rotateLeft x n := UInt32.ofBitVec (BitVec.rotateLeft x.toBitVec n) +@[simp, spec] +def num_8_impl_wrapping_add (x y: u32) : Result u32 := pure (x + y) @[simp] -def num_impl_rotate_left {α} [r: RotateLeft α] (x: α) (n: Nat) : Result α := - pure (r.rotateLeft x n) +def num_8_impl_rotate_left (x: u32) (n: Nat) : Result u32 := + pure (UInt32.ofBitVec (BitVec.rotateLeft x.toBitVec n)) end Arithmetic @@ -573,7 +554,7 @@ def constr_hax_Tuple2 {α β} {hax_Tuple2_Tuple0: α} {hax_Tuple2_Tuple1 : β} : -- Nums -- TO remove once name display is fixed -def num_impl_from_le_bytes {α} (x: Vector α n) : u32 := (0: u32) -- TOFIX +def num_8_impl_from_le_bytes (x: Vector u8 n) : u32 := (0: u32) -- TOFIX -- Casts @[simp, spec] @@ -729,23 +710,24 @@ end Arrays -- Slices def alloc_Global : Type := Unit +@[spec] def unsize {α n} (a: Vector α n) : Result (Array α) := pure (a.toArray) -def slice_impl_len α (a: Array α) : Nat := a.size +def slice_impl_len α (a: Array α) : Result usize := pure a.size def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α def vec_impl_new (α: Type) (Allocator:Type) : Result (vec_Vec α Allocator) := pure ((List.nil).toArray) -def vec_impl_len (α: Type) (Allocator:Type) (x: vec_Vec α Allocator) : Result Nat := +def vec_1_impl_len (α: Type) (Allocator:Type) (x: vec_Vec α Allocator) : Result Nat := pure x.size -def vec_impl_extend_from_slice (α Allocator) (x: vec_Vec α Allocator) (y: Array α) +def vec_2_impl_extend_from_slice (α Allocator) (x: vec_Vec α Allocator) (y: Array α) : Result (vec_Vec α Allocator):= pure (x.append y) -def slice_impl_to_vec {β} α (a: Array α) : Result (vec_Vec α β) := +def slice_impl_to_vec α (a: Array α) : Result (vec_Vec α alloc_Global) := pure a -- For @@ -759,8 +741,7 @@ instance {α n} : Coe (Array α) (Result (Vector α n)) where -- Bytes -def num_impl_to_le_bytes (_:u32) : Result (Vector u8 4) := - pure (#v[0, 0, 0, 0]) -- TOFIX +def num_8_impl_to_le_bytes (_:u32) : Result (Vector u8 4) := pure (#v[0, 0, 0, 0]) -- TOFIX -- Closures diff --git a/rust-engine/src/ast/identifiers.rs b/rust-engine/src/ast/identifiers.rs index 957755201..d8392dd79 100644 --- a/rust-engine/src/ast/identifiers.rs +++ b/rust-engine/src/ast/identifiers.rs @@ -116,12 +116,19 @@ pub mod global_id { .clone() .path .into_iter() - .map(|def| match def.clone().data { - hax_frontend_exporter::DefPathItem::ValueNs(s) - | hax_frontend_exporter::DefPathItem::MacroNs(s) - | hax_frontend_exporter::DefPathItem::TypeNs(s) => s.clone(), - hax_frontend_exporter::DefPathItem::Impl => "impl".to_string(), - other => unimplemented!("{other:?}"), + .map(|def| { + let data = match def.clone().data { + hax_frontend_exporter::DefPathItem::ValueNs(s) + | hax_frontend_exporter::DefPathItem::MacroNs(s) + | hax_frontend_exporter::DefPathItem::TypeNs(s) => s.clone(), + hax_frontend_exporter::DefPathItem::Impl => "impl".to_string(), + other => unimplemented!("{other:?}"), + }; + if def.disambiguator != 0 { + format!("{}_{}", def.disambiguator, data) + } else { + data + } }) .collect::>() .join("_"), From c9a95c4450a3ca55a8610b6fd2e3167279ab51c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 11:56:28 +0200 Subject: [PATCH 15/44] Pretty print additions as +? --- rust-engine/src/lean.rs | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 4c48801a6..4e2b2cdb3 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -290,6 +290,29 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { .group(), None => print_todo!(allocator), }, + ExprKind::App { + head, + args, + generic_args: _, + bounds_impls: _, + trait_: _, + } if match &*head.kind { + ExprKind::GlobalId(name) => { + *name == crate::names::rust_primitives::hax::machine_int::add() + } + _ => false, + } && args.len() == 2 => + { + docs![ + allocator, + "← ", + args.get(0), + allocator.reflow(" +? "), + args.get(1), + ] + .parens() + .group() + } ExprKind::App { head, args, From b8397885b7120182bf5bc67fda71c0f3343c138d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 11:57:21 +0200 Subject: [PATCH 16/44] No monadic encoding for consts of litterals --- rust-engine/src/lean.rs | 117 +++++++++++++++++++++++----------------- 1 file changed, 68 insertions(+), 49 deletions(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 4e2b2cdb3..d41fed4be 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -26,7 +26,10 @@ pub struct Lean; impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Item { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - self.kind.pretty(allocator) + self.kind + .pretty(allocator) + .append(allocator.hardline()) + .append(allocator.hardline()) } } @@ -51,62 +54,77 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { params, safety: _, } => { - let generics = if generics.params.is_empty() { - None - } else { - Some( + match &*body.kind { + ExprKind::Literal(l) => { + // Literal consts, printed without monadic encoding + // Todo: turn it into a proper refactor (see Hax issue #1542) docs![ allocator, + "def ", + name, + allocator.reflow(" : "), + &body.ty, + allocator.reflow(" :="), allocator.line(), - allocator - .intersperse(&generics.params, allocator.softline()) - .braces() - .group() + l ] - .group(), - ) - }; - let args = if params.is_empty() { - allocator.nil() - } else { - docs![ - allocator, - allocator.line(), - allocator.intersperse(params, allocator.softline()), - ] - .nest(INDENT) - .group() - }; - docs![ - allocator, - "def ", - name, - generics, - args, - docs![ - allocator, - allocator.line(), - ": ", - docs![allocator, "Result ", &body.ty].group() - ] - .group(), - " := do", - allocator.line(), - docs![allocator, &*body.kind].group() - ] - .nest(INDENT) - .group() - .append(allocator.hardline()) - .append(allocator.hardline()) + .group() + } + _ => { + // Normal definition + let generics = if generics.params.is_empty() { + None + } else { + Some( + docs![ + allocator, + allocator.line(), + allocator + .intersperse(&generics.params, allocator.softline()) + .braces() + .group() + ] + .group(), + ) + }; + let args = if params.is_empty() { + allocator.nil() + } else { + docs![ + allocator, + allocator.line(), + allocator.intersperse(params, allocator.softline()), + ] + .nest(INDENT) + .group() + }; + docs![ + allocator, + "def ", + name, + generics, + args, + docs![ + allocator, + allocator.line(), + ": ", + docs![allocator, "Result ", &body.ty].group() + ] + .group(), + " := do", + allocator.line(), + docs![allocator, &*body.kind].group() + ] + .nest(INDENT) + .group() + } + } } ItemKind::TyAlias { name, generics: _, ty, - } => docs![allocator, "abbrev ", name, allocator.reflow(" := "), ty] - .group() - .append(allocator.hardline()) - .append(allocator.hardline()), + } => docs![allocator, "abbrev ", name, allocator.reflow(" := "), ty].group(), ItemKind::Type { name: _, generics: _, @@ -422,7 +440,8 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { "let ", lhs, " ←", - docs![allocator, allocator.line(), "pure", allocator.line(), rhs] + allocator.softline(), + docs![allocator, "pure", allocator.line(), rhs] .group() .nest(INDENT), ";", From c86b686e9964be15ae8b0b90bea18b9c65d70c4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 12:00:04 +0200 Subject: [PATCH 17/44] Add spec to hax_fold_range (loops) --- hax-lib/proof-libs/lean/Lib.lean | 137 +++++++++++++++++++++++++++---- 1 file changed, 123 insertions(+), 14 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 3bef53041..e01f5537b 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -598,13 +598,75 @@ def prop_constructors_from_bool (b :Bool) : Prop := (b = true) -- Hax --- To extend with invariants def hax_folds_fold_range {α} (s e : Nat) - (_inv : α -> Nat -> Result Bool) + (inv : α -> Nat -> Result Bool) (init: α) - (f : α -> Nat -> Result α) : Result α := - Array.foldlM f init (Array.range e) s e + (f : α -> Nat -> Result α) : Result α := do + if e ≤ s then pure init + else hax_folds_fold_range (s+1) e inv (← f init s) f + +theorem induction_decreasing {e} {P: Nat → Prop} + (init: P e) + (rec: ∀ n, n < e → P (n+1) → P n) : + ∀ n, n ≤ e → P n +:= by + intros n h + by_cases (n = 0) + . subst_vars + induction e <;> try grind + generalize h: (e - n) = d + have : n = e - d := by omega + have hlt : d < e := by omega + rw [this] ; clear h this + induction d with + | zero => simp ; grind + | succ d ih => + apply rec <;> try omega + suffices e - (d + 1) + 1 = e - d by grind + omega + +def induction_decreasing_range {s e} {P: Nat → Nat → Prop} : + s ≤ e → + (init: P e e) → + (rec: ∀ (n : Nat), n < e → s ≤ n → P (n + 1) e → P n e) → + P s e +:= by intros; apply induction_decreasing (P := fun n => (s ≤ n → P n e)) (e := e) <;> try grind + +@[spec] +theorem hax_folds_fold_range_spec {α} + (s e : Nat) + (inv : α -> Nat -> Result Bool) + (init: α) + (f : α -> Nat -> Result α) : + ⦃ inv init s = pure true ∧ + s ≤ e ∧ + ∀ (acc:α) (i:Nat), s ≤ i → i < e → + ⦃ inv acc i = pure true ⦄ + (f acc i) + ⦃ ⇓ res => inv res (i+1) = pure true ⦄ + ⦄ + (hax_folds_fold_range s e inv init f) + ⦃ ⇓ r => inv r e = pure true ⦄ +:= by + intro ⟨ h_inv_s, h_s_le_e , h_f ⟩ + revert h_inv_s init + have := induction_decreasing_range (s := s) (e := e) + (P := fun s e => + ∀ acc, inv acc s = pure true → + wp⟦hax_folds_fold_range s e inv acc f⟧ ⇓ r => inv r e = pure true) + apply this <;> clear this <;> try omega + . simp [hax_folds_fold_range] + . intros n _ _ ih acc h_acc + unfold hax_folds_fold_range + mvcgen <;> try grind + specialize h_f acc n (by omega) (by omega) + mspec h_f + intro h_r + apply (ih _ h_r) + +instance : Coe USize Nat where + coe x := x.toNat -- Arrays @@ -629,45 +691,45 @@ def result_impl_unwrap (α: Type) (β:Type) (x: result_Result α β) : (Result | .err _ => .fail .panic -- Vectors +@[spec] def hax_repeat {α} (v:α) (n:Nat) : Result (Vector α n) := - pure (Eq.mp (congrArg (Vector α) (@Array.size_replicate α n v)) - (Array.replicate n v).toVector) + pure (Vector.replicate n v) -- Ranges inductive ops_range_Range (α: Type) where -| constr_ops_range_Range - {ops_range_Range_start: α} - {ops_range_Range_end: α} : ops_range_Range α +| range (r_start r_end : α) : ops_range_Range α +@[simp, spec] def constr_ops_range_Range {α} {ops_range_Range_start : α} {ops_range_Range_end : α} := - ops_range_Range.constr_ops_range_Range - (ops_range_Range_start := ops_range_Range_start) - (ops_range_Range_end := ops_range_Range_end) + ops_range_Range.range ops_range_Range_start ops_range_Range_end +@[simp, spec] def ops_index_Index_index {α β γ} (a: α) (i:β) [GetElem α β (Result γ) (fun _ _ => True) ] : (Result γ) := a[i] +@[simp] instance : GetElem (Array α) (ops_range_Range usize) (Result (Array α)) (fun _ _ => True) where getElem xs i _ := match i with - | @ops_range_Range.constr_ops_range_Range _ s e => + | ops_range_Range.range s e => let size := xs.size; if (s > e || e > size || s > size) then Result.fail Error.arrayOutOfBounds else pure ( xs.extract s e ) +@[simp] instance {α n} [tn: ToNat β]: GetElem (Vector α n) (ops_range_Range β) (Result (Array α)) (fun _ _ => True) where getElem xs i _ := match i with - | @ops_range_Range.constr_ops_range_Range _ s e => + | ops_range_Range.range s e => let e := tn.toNat e; let s := tn.toNat s; let size := xs.size; @@ -693,6 +755,53 @@ instance {α β : Type} {n : Nat} [tn: ToNat β]: GetElem (Vector α n) β (Resu instance {α : Type} {n : Nat}: GetElem (Vector α n) Nat (Result α) (fun _ _ => True) where getElem xs i _ := Result.ofOption xs[i]? .arrayOutOfBounds +@[spec] +theorem ops_index_Index_index_usize_range_vector_spec + (α : Type) (v: Vector α n ) (s e: usize) : + ⦃ s ≤ e ∧ e < n ⦄ + ( v[ ops_range_Range.range s e] : Result (Array α)) + ⦃ ⇓ r => r = (Vector.extract v s e).toArray ⦄ +:= by + mvcgen + simp + split <;> try split at * <;> try grind + all_goals simp [Vector.size] at * <;> try grind + intros + expose_names + cases h + . expose_names + cases h <;> try omega + . rw [← USize.lt_iff_toNat_lt] at * ; bv_decide + . sorry + . sorry + +@[spec] +theorem ops_index_Index_index_usize_range_array_spec + (α : Type) (a: Array α) (s e: usize) : + ⦃ s ≤ e ∧ e ≤ a.size ⦄ + (a[ (ops_range_Range.range s e)]) + ⦃ ⇓ r => r = Array.extract a s e ⦄ +:= by + mvcgen [ops_index_Index_index, + USize.instGetElemArrayResult, + GetElemResult, Result.ofOption] <;> expose_names + simp [GetElem.getElem] + intros + split <;> try simp + . split at * + . grind + injections + subst_eqs + constructor + . split at * <;> injections + subst_eqs + expose_names + cases h_2 <;> try bv_decide + simp [USize.le_iff_toNat_le, USize.lt_iff_toNat_lt] at * + omega + . split at * <;> try grind + + -- Arrays section Arrays From 2263424d42d90e58f9494f9cd3de0394c0d2efd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 15:51:38 +0200 Subject: [PATCH 18/44] Improved the treatment of closure --- hax-lib/proof-libs/lean/Lib.lean | 21 +++++++++--- .../toolchain__lean-tests into-lean.snap | 33 ++++++++++--------- tests/lean-tests/src/lib.rs | 5 +-- 3 files changed, 38 insertions(+), 21 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index e01f5537b..21f03eeb6 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -149,6 +149,10 @@ instance : Coe u32 Nat where instance : Coe Nat usize where coe x := USize.ofNat x +@[simp] +instance : Coe Nat i32 where + coe x := Int32.ofNat x + @[simp] instance : Coe USize UInt32 where coe x := x.toUInt32 @@ -536,16 +540,16 @@ end Arithmetic -- Tuples -def hax_Tuple0 : Type := Unit +abbrev hax_Tuple0 : Type := Unit def constr_hax_Tuple0 : hax_Tuple0 := () instance : Coe hax_Tuple0 Unit where coe _ := () -def hax_Tuple1 (α: Type) : Type := α × Unit +abbrev hax_Tuple1 (α: Type) : Type := α × Unit def constr_hax_Tuple1 {hax_Tuple1_Tuple0: α} : hax_Tuple1 α := (hax_Tuple1_Tuple0, ()) -def hax_Tuple2 (α β: Type) : Type := α × β +abbrev hax_Tuple2 (α β: Type) : Type := α × β def constr_hax_Tuple2 {α β} {hax_Tuple2_Tuple0: α} {hax_Tuple2_Tuple1 : β} : hax_Tuple2 α β := (hax_Tuple2_Tuple0, hax_Tuple2_Tuple1) @@ -854,7 +858,16 @@ def num_8_impl_to_le_bytes (_:u32) : Result (Vector u8 4) := pure (#v[0, 0, 0, 0 -- Closures -def ops_function_Fn_call {α β} (f: α -> β) (x: α) := f x +class Fn α (β : outParam Type) γ where + call : α → β → γ + +instance {α β} : Fn (α → β) (hax_Tuple1 α) β where + call f x := f x.fst + +instance {α β γ} : Fn (α → β → γ) (hax_Tuple2 α β) γ where + call f x := f x.fst x.snd + +def ops_function_Fn_call {α β γ} [Fn α β γ] (f: α) (x: β) : γ := Fn.call f x -- Miscellaneous diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index de38d8c02..ad14dcfbd 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -34,24 +34,27 @@ import Lib --- unimplemented yet -def FORTYTWO : usize := 42 -def returns42 (_ : hax_Tuple0) : usize := FORTYTWO +def FORTYTWO : usize := 42 -def add_two_numbers (x : usize) (y : usize) : usize := (hax_machine_int_add x y) +def returns42 (_ : hax_Tuple0) : Result usize := do FORTYTWO -def letBinding (x : usize) (y : usize) : usize := - let useless := (.constr_hax_Tuple0 : hax_Tuple0); - let result1 := (hax_machine_int_add x y); - let result2 := (hax_machine_int_add result1 2); - (hax_machine_int_add result2 1) +def add_two_numbers (x : usize) (y : usize) : Result usize := do (← x +? y) -def closure (_ : hax_Tuple0) : i32 := - let x := 41; - let f := (fun y => (hax_machine_int_add y x)); - (ops_function_Fn_call f - (.constr_hax_Tuple1 {hax_Tuple1_Tuple0 := 1} : (hax_Tuple1 i32))) +def letBinding (x : usize) (y : usize) : Result usize := do + let (useless : hax_Tuple0) ← pure (constr_hax_Tuple0 ); + let (result1 : usize) ← pure (← x +? y); + let (result2 : usize) ← pure (← result1 +? 2); (← result2 +? 1) -abbrev UsizeAlias := usize''' +def closure (_ : hax_Tuple0) : Result i32 := do + let (x : i32) ← pure 41; + let (f1 : (i32 -> Result i32)) ← pure (fun (y : i32)=> do (← y +? x)); + let (f2 : (i32 -> i32 -> Result i32)) ← pure + (fun (y : i32) (z : i32)=> do (← (← y +? x) +? z)); + (← (← ops_function_Fn_call f1 (constr_hax_Tuple1 (hax_Tuple1_Tuple0 := 1))) + +? (← ops_function_Fn_call + f2 + (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) + +''' diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index 51d89a6b8..2c5040302 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -19,8 +19,9 @@ fn letBinding(x: usize, y: usize) -> usize { fn closure() -> i32 { let x = 41; - let f = |y| y + x; - f(1) + let f1 = |y| y + x ; + let f2 = |y, z| y + x + z; + f1(1) + f2(2,3) } type UsizeAlias = usize; From c6db79157ef7d6df8cfbb2fc79e181a00fa9dd5a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Thu, 31 Jul 2025 16:23:03 +0200 Subject: [PATCH 19/44] Update header in Lean file --- rust-engine/src/main.rs | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index bef92c75a..c11284791 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -21,11 +21,18 @@ fn lean_backend(items: Vec) { let header = allocator .intersperse( - vec![ - "-- Experimental lean backend for Hax", - "-- Comment the following line to not import the prelude (requires the Lib.lean file) : ", - "import Lib", - ], + " +-- Experimental lean backend for Hax +-- Comment the following line to not import the prelude (requires the Lib.lean file) : +import Lib +import Std.Tactic.Do +import Std.Do.Triple +import Std.Tactic.Do.Syntax +open Std.Do +open Std.Tactic + +set_option linter.unusedVariables false" + .lines(), allocator.hardline(), ) .append(allocator.hardline()) From 8bb4268a2d9e8d8c2d474d467d8423792b184f77 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 09:46:52 +0200 Subject: [PATCH 20/44] Add a lean macro for backporting lean inside rust code --- hax-lib/build.rs | 1 + hax-lib/macros/src/implementation.rs | 2 +- rust-engine/src/lean.rs | 27 +++++++++++++++---- .../toolchain__lean-tests into-lean.snap | 24 ++++++++++++++++- tests/lean-tests/src/lib.rs | 16 +++++------ 5 files changed, 53 insertions(+), 17 deletions(-) diff --git a/hax-lib/build.rs b/hax-lib/build.rs index eb4850605..90931618d 100644 --- a/hax-lib/build.rs +++ b/hax-lib/build.rs @@ -43,6 +43,7 @@ pub mod {backend} {{ code("fstar", FSTAR_EXTRA), code("proverif", ""), code("coq", ""), + code("lean", ""), ] .join("\n"), ) diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index 2374db617..7a2040ffc 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -989,7 +989,7 @@ macro_rules! make_quoting_proc_macro { } } -make_quoting_proc_macro!(fstar coq proverif); +make_quoting_proc_macro!(fstar coq proverif lean); /// Marks a newtype `struct RefinedT(T);` as a refinement type. The /// struct should have exactly one unnamed private field. diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index d41fed4be..adce2e923 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -151,9 +151,9 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { rename: _, } => allocator.nil(), ItemKind::Quote { - quote: _, + quote, origin: _, - } => print_todo!(allocator), + } => quote.pretty(allocator), ItemKind::Error(_diagnostic) => print_todo!(allocator), ItemKind::Resugared(_resugared_ty_kind) => print_todo!(allocator), ItemKind::NotImplementedYet => allocator.nil(), @@ -185,8 +185,8 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b TyKind { } TyKind::Arrow { inputs, output } => docs![ allocator, - allocator.intersperse(inputs.into_iter(), allocator.reflow(" -> ")), - "Result", + allocator.concat(inputs.into_iter().map(|input| docs![allocator, input, allocator.reflow(" -> ")] )), + "Result ", output ] .parens(), @@ -492,7 +492,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { body: _, safety_mode: _, } => print_todo!(allocator), - ExprKind::Quote { contents: _ } => print_todo!(allocator), + ExprKind::Quote { contents } => allocator.concat(&contents.0), ExprKind::Resugared(_resugared_expr_kind) => print_todo!(allocator), ExprKind::Error(_diagnostic) => print_todo!(allocator), } @@ -588,3 +588,20 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b GenericParam { self.ident.pretty(allocator) } } + +impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Quote { + fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { + allocator.concat(&self.0) + } +} + +impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b QuoteContent { + fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { + match self { + QuoteContent::Verbatim(s) => allocator.intersperse(s.lines().map(|x| x.to_string()), allocator.hardline()), + QuoteContent::Expr(expr) => expr.pretty(allocator), + QuoteContent::Pattern(pat) => pat.pretty(allocator), + QuoteContent::Ty(ty) => ty.pretty(allocator), + } + } +} diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index ad14dcfbd..1f9106ee8 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -28,9 +28,17 @@ diagnostics = [] [stdout.files] "lean_tests.lean" = ''' + -- Experimental lean backend for Hax --- Comment the following line to not import the prelude (requires the Lib.lean file) : +-- Comment the following line to not import the prelude (requires the Lib.lean file) : import Lib +import Std.Tactic.Do +import Std.Do.Triple +import Std.Tactic.Do.Syntax +open Std.Do +open Std.Tactic + +set_option linter.unusedVariables false @@ -57,4 +65,18 @@ def closure (_ : hax_Tuple0) : Result i32 := do f2 (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) + + +@[spec] + +def test_before_verbatime_single_line : u8 := 42 + +def 1__ : Result hax_Tuple0 := do hax_Tuple0 + + +def multiline : Unit := () + + +def test_before_verbatim_multi_line : u8 := 32 + ''' diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index 2c5040302..f98bc471b 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -24,15 +24,11 @@ fn closure() -> i32 { f1(1) + f2(2,3) } -type UsizeAlias = usize; +#[hax_lib::lean::before("@[spec]")] +fn test_before_verbatime_single_line(x: u8) -> u8 { 42 } -// Hello world example from https://hacspec.zulipchat.com/#narrow/channel/269544-general/topic/hax.20.2B.20coq/with/528801096 -fn main() { - let x = square(10u8); - println!("{}", x); -} +#[hax_lib::lean::before(" +def multiline : Unit := () -#[hax_lib::requires(n < 16u8)] -fn square(n: u8) -> u8 { - n * n -} +")] +fn test_before_verbatim_multi_line(x: u8) -> u8 { 32 } From 88008e6015b9dca22dc596f458bddc6f41ac46a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 11:20:08 +0200 Subject: [PATCH 21/44] Filter items with empty names + remove spurious empty lines in lean --- rust-engine/src/ast/identifiers.rs | 5 ++- rust-engine/src/lean.rs | 61 ++++++++++++++++++++---------- rust-engine/src/main.rs | 20 ++++++---- 3 files changed, 55 insertions(+), 31 deletions(-) diff --git a/rust-engine/src/ast/identifiers.rs b/rust-engine/src/ast/identifiers.rs index d8392dd79..8282bd5c5 100644 --- a/rust-engine/src/ast/identifiers.rs +++ b/rust-engine/src/ast/identifiers.rs @@ -124,8 +124,9 @@ pub mod global_id { hax_frontend_exporter::DefPathItem::Impl => "impl".to_string(), other => unimplemented!("{other:?}"), }; - if def.disambiguator != 0 { - format!("{}_{}", def.disambiguator, data) + if def.disambiguator != 0 && !data.is_empty() && data != "_" { + // Don't print disambiguator of empty data + format!("_{}_{}", def.disambiguator, data) } else { data } diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index adce2e923..3651c988f 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -24,29 +24,44 @@ const INDENT: isize = 2; /// Placeholder structure for lean printer pub struct Lean; +impl Lean { + /// A filter for items blacklisted by the Lean backend : returns false if + /// the item is definitely not printable, but might return true on + /// unsupported items + pub fn printable_item(item: &Item) -> bool { + match &item.kind { + // Anonymous consts + ItemKind::Fn { + name, + generics: _, + body: _, + params: _, + safety: _, + } if name.is_empty() => false, + // Other unprintable items + ItemKind::Error(_) | ItemKind::NotImplementedYet | ItemKind::Use { .. } => false, + // Printable items + ItemKind::Fn { .. } + | ItemKind::TyAlias { .. } + | ItemKind::Type { .. } + | ItemKind::Trait { .. } + | ItemKind::Impl { .. } + | ItemKind::Alias { .. } + | ItemKind::Resugared(_) + | ItemKind::Quote { .. } => true, + } + } +} + impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Item { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { - self.kind - .pretty(allocator) - .append(allocator.hardline()) - .append(allocator.hardline()) + self.kind.pretty(allocator) } } impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { match self { - ItemKind::Fn { - name, - generics: _, - body: _, - params, - safety: _, - } if name.is_empty() && params.is_empty() => { - // Anonymous const, ignored - // Todo: turn it into a proper refactor (see Hax issue #1542) - allocator.nil() - } ItemKind::Fn { name, generics, @@ -117,6 +132,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { ] .nest(INDENT) .group() + .append(allocator.hardline()) } } } @@ -150,10 +166,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { is_external: _, rename: _, } => allocator.nil(), - ItemKind::Quote { - quote, - origin: _, - } => quote.pretty(allocator), + ItemKind::Quote { quote, origin: _ } => quote.pretty(allocator), ItemKind::Error(_diagnostic) => print_todo!(allocator), ItemKind::Resugared(_resugared_ty_kind) => print_todo!(allocator), ItemKind::NotImplementedYet => allocator.nil(), @@ -185,7 +198,11 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b TyKind { } TyKind::Arrow { inputs, output } => docs![ allocator, - allocator.concat(inputs.into_iter().map(|input| docs![allocator, input, allocator.reflow(" -> ")] )), + allocator.concat(inputs.into_iter().map(|input| docs![ + allocator, + input, + allocator.reflow(" -> ") + ])), "Result ", output ] @@ -598,7 +615,9 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b Quote { impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b QuoteContent { fn pretty(self, allocator: &'a Allocator) -> DocBuilder<'a, Allocator, Span> { match self { - QuoteContent::Verbatim(s) => allocator.intersperse(s.lines().map(|x| x.to_string()), allocator.hardline()), + QuoteContent::Verbatim(s) => { + allocator.intersperse(s.lines().map(|x| x.to_string()), allocator.hardline()) + } QuoteContent::Expr(expr) => expr.pretty(allocator), QuoteContent::Pattern(pat) => pat.pretty(allocator), QuoteContent::Ty(ty) => ty.pretty(allocator), diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index c11284791..8d8dea7f3 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -6,7 +6,7 @@ use hax_rust_engine::{ }; use hax_types::{cli_options::Backend, engine_api::File}; -use pretty::{DocAllocator, DocBuilder}; +use pretty::{docs, DocAllocator, DocBuilder}; fn krate_name(items: &Vec) -> String { let head_item = items.get(0).unwrap(); @@ -17,10 +17,11 @@ fn lean_backend(items: Vec) { let krate = krate_name(&items); // For now, the main function always calls the Lean backend - let allocator = Allocator::new(Lean); + let allocator = &Allocator::new(Lean); - let header = allocator - .intersperse( + let header = docs![ + allocator, + allocator.intersperse( " -- Experimental lean backend for Hax -- Comment the following line to not import the prelude (requires the Lib.lean file) : @@ -34,11 +35,14 @@ open Std.Tactic set_option linter.unusedVariables false" .lines(), allocator.hardline(), - ) - .append(allocator.hardline()) - .append(allocator.hardline()); + ), + allocator.hardline(), + allocator.hardline() + ]; - let item_docs: DocBuilder<_, Span> = header.append(allocator.concat(items.iter())); + let items = items.iter().filter(|item: &&hax_rust_engine::ast::Item| Lean::printable_item(*item)); + let item_docs: DocBuilder<_, Span> = + header.append(allocator.intersperse(items, allocator.hardline())); hax_rust_engine::hax_io::write(&hax_types::engine_api::protocol::FromEngine::File(File { path: krate + ".lean", From 8f7dab41cbc4b983cefe4849b24e8959ae16e3f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 16:58:19 +0200 Subject: [PATCH 22/44] Document the Lib.lean file --- hax-lib/proof-libs/lean/Lib.lean | 475 +++++++++++++++++++++---------- 1 file changed, 331 insertions(+), 144 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 21f03eeb6..f9a105a33 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -1,4 +1,13 @@ --- This library provides a monadic encoding over Hax primitives +/- +Hax Lean Backend - Cryspen + +This library provides the Lean prelude for hax extracted rust-code. It contains +the lean definition of rust (and hax) primitives and intrinsics. + +It borrows some definitions from the Aeneas project +(https://github.com/AeneasVerif/aeneas/) +-/ + import Std import Std.Do.Triple import Std.Tactic.Do @@ -7,8 +16,18 @@ import Std.Tactic.Do.Syntax open Std.Do open Std.Tactic --- Aeneas errors --- see https://github.com/AeneasVerif/aeneas/ + +/- +# Monadic encoding + +The encoding is based on the `Result` monad: all rust computations are wrapped +in the monad, representing the fact that they are not total. + +-/ + +/-- + (Aeneas) Error cases +-/ inductive Error where | assertionFailure: Error | integerOverflow: Error @@ -18,94 +37,111 @@ inductive Error where | panic: Error | undef: Error deriving Repr, BEq - open Error +/-- (Aeneas) Result monad, representing possible results of rust computations -/ inductive Result.{u} (α : Type u) where | ok (v: α): Result α | fail (e: Error): Result α | div deriving Repr, BEq +namespace Result + @[simp] -instance Result.instPure: Pure Result where +instance instPure: Pure Result where pure x := .ok x -@[simp, spec] -def Result.pure (x: α) : Result α := (Result.instPure.pure x) - @[simp] -def Result.bind (x: Result α) (f: α -> Result β) := match x with +def bind (x: Result α) (f: α -> Result β) := match x with | .ok v => f v | .fail e => .fail e | .div => .div @[simp] -def Result.ofOption {α} (x:Option α) (e: Error) : Result α := match x with +def ofOption {α} (x:Option α) (e: Error) : Result α := match x with | .some v => pure v | .none => .fail e @[simp] -instance Result.instMonad : Monad Result where +instance instMonad : Monad Result where pure := pure bind := Result.bind @[simp] -instance Result.instLawfulMonad : LawfulMonad Result where +instance instLawfulMonad : LawfulMonad Result where id_map x := by - dsimp [id, Functor.map, Result.pure] + dsimp [id, Functor.map] cases x; all_goals grind map_const := by intros α β dsimp [Functor.map, Functor.mapConst] seqLeft_eq x y := by - dsimp [Functor.map, SeqLeft.seqLeft, Seq.seq, Result.pure] + dsimp [Functor.map, SeqLeft.seqLeft, Seq.seq] cases x ; all_goals cases y all_goals try simp seqRight_eq x y := by - dsimp [Functor.map, SeqRight.seqRight, Seq.seq, Result.pure] + dsimp [Functor.map, SeqRight.seqRight, Seq.seq] cases x ; all_goals cases y all_goals try simp pure_seq g x := by - dsimp [Functor.map, Seq.seq, pure, Result.pure] + dsimp [Functor.map, Seq.seq, pure] bind_pure_comp f x := by dsimp [Functor.map] bind_map f x := by - dsimp [Functor.map, bind, pure, Seq.seq, Result.pure] + dsimp [Functor.map, bind, pure, Seq.seq] pure_bind x f := by - dsimp [pure, bind, Result.pure] + dsimp [pure, bind, pure] bind_assoc x f g := by dsimp [pure, bind] cases x; all_goals simp --- set_option pp.coercions false @[simp] -instance Result.instWP : WP Result (.except Error .pure) where +instance instWP : WP Result (.except Error .pure) where wp x := match x with | .ok v => wp (Pure.pure v : Except Error _) | .fail e => wp (throw e : Except Error _) | .div => PredTrans.const ⌜False⌝ --- set_option pp.raw true @[simp] -instance Result.instWPMonad : WPMonad Result (.except Error .pure) where - wp_pure := by intros; ext Q; simp [wp, PredTrans.pure, Pure.pure, Except.pure, Id.run, Result.pure] +instance instWPMonad : WPMonad Result (.except Error .pure) where + wp_pure := by intros; ext Q; simp [wp, PredTrans.pure, Pure.pure, Except.pure, Id.run] wp_bind x f := by simp only [instWP] ext Q cases x <;> simp [PredTrans.bind, PredTrans.const, Bind.bind] @[default_instance] -instance Result.instCoe {α} : Coe α (Result α) where +instance instCoe {α} : Coe α (Result α) where coe x := pure x --- Logic +end Result + + +/- + Logic predicates introduced by Hax (in pre/post conditions) +-/ +section Logic + +@[simp, spec] abbrev hax_logical_op_and := (fun a b => a && b) +@[simp, spec] abbrev hax_logical_op_or := (fun a b => a || b) --- Integer types +abbrev assert (b:Bool) : Result Unit := + if b then pure () + else .fail (Error.assertionFailure) + +abbrev assume : Prop -> Result Unit := fun _ => pure () +abbrev prop_constructors_from_bool (b :Bool) : Prop := (b = true) + +end Logic + +/- + Integer types are represented as the corresponding type in Lean +-/ abbrev u8 := UInt8 abbrev u16 := UInt16 abbrev u32 := UInt32 @@ -117,10 +153,10 @@ abbrev i32 := Int32 abbrev i64 := Int64 abbrev isize := ISize +/-- Class of objects that can be transformed into Nat -/ class ToNat (α: Type) where toNat : α -> Nat --- should use a macro here @[simp] instance : ToNat USize where toNat x := x.toNat @@ -137,10 +173,18 @@ instance : ToNat u16 where instance : ToNat Nat where toNat x := x +/- + Coercions between integer types +-/ +-- TODO : make sure all are necessary, document their use-cases @[simp, spec] instance : Coe i32 (Result i64) where coe x := pure (x.toInt64) +@[simp] +instance : Coe USize Nat where + coe x := x.toNat + @[simp] instance : Coe u32 Nat where coe x := x.toNat @@ -159,7 +203,7 @@ instance : Coe USize UInt32 where @[simp] instance : Coe USize (Result u32) where - coe x := if h: x.toNat < UInt32.size then pure (x.toUInt32) + coe x := if x.toNat < UInt32.size then pure (x.toUInt32) else Result.fail .integerOverflow @[simp] @@ -175,7 +219,14 @@ instance : OfNat (Result Nat) n where ofNat := pure (n) --- Arithmetic +/- + +# Arithmetic operations + +The Rust arithmetic operations have their own notations, using a `?`. They +return a `Result`, that is `.fail` when arithmetic overflows occur. + +-/ section Arithmetic /-- The notation typeclass for homogeneous addition that returns a Result. This @@ -231,7 +282,8 @@ class HaxRem α where @[inherit_doc] infixl:70 " %? " => HaxRem.rem @[inherit_doc] infixl:70 " /? " => HaxDiv.div --- Overflowing operations +/- Until notations are not introduced by the Lean backend, explicit hax-names + are also provided -/ @[simp, spec] def hax_machine_int_add {α} [HaxAdd α] (x y: α) : Result α := x +? y @[simp, spec] @@ -245,7 +297,7 @@ def hax_machine_int_rem {α} [HaxRem α] (x y: α) : Result α := x %? y @[simp, spec] def hax_machine_int_shr {α} [HaxShiftRight α] (a b: α) : Result α := a >>>? b @[simp] -def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := Result.pure (a ^^^ b) +def hax_machine_int_bitxor {α} [Xor α] (a b: α) : Result α := pure (a ^^^ b) @[simp] def ops_arith_Neg_neg {α} [Neg α] (x:α) : Result α := pure (-x) @@ -254,68 +306,94 @@ def hax_machine_int_eq {α} (x y: α) [BEq α] : Result Bool := pure (x == y) @[simp] def hax_machine_int_ne {α} (x y: α) [BEq α] : Result Bool := pure (x != y) @[simp] -def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Result Bool := pure (x < y) +def hax_machine_int_lt {α} (x y: α) [(LT α)] [Decidable (x < y)] : Result Bool := + pure (x < y) @[simp] -def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Result Bool := pure (x ≤ y) +def hax_machine_int_le {α} (x y: α) [(LE α)] [Decidable (x ≤ y)] : Result Bool := + pure (x ≤ y) @[simp] -def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Result Bool := pure (x ≥ y) +def hax_machine_int_gt {α} (x y: α) [(LE α)] [Decidable (x ≥ y)] : Result Bool := + pure (x ≥ y) @[simp] -def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Result Bool := pure (x > y) +def hax_machine_int_ge {α} (x y: α) [(LT α)] [Decidable (x > y)] : Result Bool := + pure (x > y) + +/- +# Properties + +For each integer types, instances of typeclasses for arithmetic operations are +given, along with hoare-triple specifications (to be used by mvcgen) + +-/ namespace USize +/-- Partial addition on usize -/ instance instHaxAdd : HaxAdd USize where add x y := if (BitVec.saddOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow else pure (x + y) +/-- Bitvec-based specification for rust addition on usize -/ @[spec] theorem HaxAdd_spec_bv (x y: usize) : ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄ (x +? y) ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ] + +/-- Partial substraction on usize -/ instance instHaxSub : HaxSub USize where sub x y := if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow else pure (x - y) +/-- Bitvec-based specification for rust substraction on usize -/ @[spec] theorem HaxSub_spec_bv (x y: usize) : ⦃ ¬ (BitVec.ssubOverflow x.toBitVec y.toBitVec) ⦄ (x -? y) ⦃ ⇓ r => r = x - y ⦄ := by mvcgen [instHaxSub] + +/-- Partial multiplication on usize -/ instance instHaxMul : HaxMul USize where mul x y := if (BitVec.smulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow else pure (x * y) +/-- Bitvec-based specification for rust multiplication on usize -/ @[spec] theorem HaxMul_spec_bv (x y: usize) : ⦃ ¬ (BitVec.smulOverflow x.toBitVec y.toBitVec) ⦄ (x *? y) ⦃ ⇓ r => r = x * y ⦄ := by mvcgen [instHaxMul] + +/-- Partial right shift on usize -/ instance instHaxShiftRight : HaxShiftRight USize where shiftRight x y := if (y ≤ USize.size) then pure (x >>> y) else .fail .integerOverflow +/-- Bitvec-based specification for rust right-shift on usize -/ @[spec] theorem HaxShiftRight_spec_bv (x y: usize) : ⦃ y ≤ USize.size ⦄ ( x >>>? y) ⦃ ⇓ r => r = x >>> y ⦄ := by mvcgen [instHaxShiftRight] + +/-- Partial division on usize -/ instance instHaxDiv : HaxDiv usize where div x y := if y = 0 then .fail .divisionByZero else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow else pure (x / y) +/-- Bitvec-based specification for rust division on usize -/ @[spec] theorem HaxDiv_spec_bv (x y : usize) : ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄ @@ -325,12 +403,14 @@ theorem HaxDiv_spec_bv (x y : usize) : have ⟨ _ , h ⟩ := h apply h; assumption +/-- Partial remainder on usize -/ instance instHaxRem : HaxRem usize where rem x y := if y = 0 then .fail .divisionByZero else if (BitVec.sdivOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow else pure (x % y) +/-- Bitvec-based specification for rust remainder on usize -/ @[spec] theorem HaxRem_spec_bv (x y : usize) : ⦃ y != 0 ∧ ¬ BitVec.sdivOverflow x.toBitVec y.toBitVec⦄ @@ -340,9 +420,9 @@ theorem HaxRem_spec_bv (x y : usize) : have ⟨ _ , h ⟩ := h apply h; assumption - end USize + namespace ISize instance instHaxAdd : HaxAdd ISize where @@ -391,6 +471,7 @@ theorem HaxShiftRight_spec_bv (x y: isize) : end ISize + namespace Int64 instance instHaxAdd : HaxAdd Int64 where @@ -439,6 +520,7 @@ theorem HaxShiftRight_spec_bv (x y: i64) : end Int64 + namespace Int32 instance instHaxAdd : HaxAdd Int32 where @@ -452,17 +534,6 @@ theorem HaxAdd_spec_bv (x y: i32) : (x +? y) ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ] --- @[spec] --- theorem HaxAdd_spec_Int (x y: i32) : --- ⦃ x.toInt + y.toInt < Int32.maxValue.toInt ⦄ --- (x +? y : Result i32) --- ⦃ ⇓ r => r = x + y ⦄ --- := by --- mvcgen [Int32.instHaxAdd ] --- cases h__overflow : ((toBitVec x).saddOverflow (toBitVec y)) <;> try simp --- have := @BitVec.toInt_add_of_not_saddOverflow _ (x.toBitVec) (y.toBitVec) --- simp [] - instance instHaxSub : HaxSub Int32 where sub x y := if (BitVec.ssubOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow @@ -502,33 +573,15 @@ theorem HaxRem_spec_bv (x y : i32) : end Int32 +/- -abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize - (lo: USize) (hi: USize) := USize --- {u : usize // lo ≤ u ∧ u ≤ hi} - --- #check hax__autogenerated_refinement__BoundedUsize_BoundedUsize 0 19 --- #check fun (x: {usize // True}) => x.val - -set_option pp.coercions false - --- instance {n lo hi : Nat} {hlo: lo ≤ x} {hhi: x ≤ hi}: --- OfNat (hax__autogenerated_refinement__BoundedUsize_BoundedUsize lo hi) x where --- ofNat := { --- val := x , --- property := by --- constructor --- . unfold Nat.cast +# Wrapping operations --- apply USize.le_iff_toNat_le.mp +Rust also has total arithmetic operations, renamed by hax (with disambiguator) +for each implementation of typeclasses --- . apply USize.le_iff_toNat_le.mp --- grind +-/ --- } --- #check (10: hax__autogenerated_refinement__BoundedUsize_BoundedUsize 0 10) - --- Wrapping operations @[simp, spec] def num_8_impl_wrapping_add (x y: u32) : Result u32 := pure (x + y) @@ -536,14 +589,37 @@ def num_8_impl_wrapping_add (x y: u32) : Result u32 := pure (x + y) def num_8_impl_rotate_left (x: u32) (n: Nat) : Result u32 := pure (UInt32.ofBitVec (BitVec.rotateLeft x.toBitVec n)) + +/-- Hax-generated bounded integers -/ +abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize + (lo: USize) (hi: USize) := USize +-- {u : usize // lo ≤ u ∧ u ≤ hi} +-- Todo : make it into a proper subtype + +/-- [Warning] unimplemented yet -/ +noncomputable +def num_8_impl_from_le_bytes (x: Vector u8 n) : u32 := sorry + +/-- [Warning] unimplemented yet -/ +noncomputable +def num_8_impl_to_le_bytes (_:u32) : Result (Vector u8 4) := sorry + + end Arithmetic --- Tuples + + +/- + +# Tuples + +-/ +section Tuples abbrev hax_Tuple0 : Type := Unit def constr_hax_Tuple0 : hax_Tuple0 := () -instance : Coe hax_Tuple0 Unit where - coe _ := () +instance : CoeDep Type hax_Tuple0 (Result hax_Tuple0) where + coe := pure () abbrev hax_Tuple1 (α: Type) : Type := α × Unit @@ -553,24 +629,33 @@ abbrev hax_Tuple2 (α β: Type) : Type := α × β def constr_hax_Tuple2 {α β} {hax_Tuple2_Tuple0: α} {hax_Tuple2_Tuple1 : β} : hax_Tuple2 α β := (hax_Tuple2_Tuple0, hax_Tuple2_Tuple1) +end Tuples + +/- --- Nums --- TO remove once name display is fixed +# Casts -def num_8_impl_from_le_bytes (x: Vector u8 n) : u32 := (0: u32) -- TOFIX +-/ +section Cast --- Casts +/-- Hax-introduced explicit cast. It is partial (returns a `Result`) -/ @[simp, spec] def convert_From_from {α β} [Coe α (Result β)] (x:α) : (Result β) := x +/-- Rust-supported casts on base types -/ class Cast (α β: Type) where cast : α → Result β +/-- Wrapping cast, does not fail on overflow -/ @[spec] instance : Cast i64 i32 where cast x := pure (Int64.toInt32 x) +@[spec] +instance : Cast i64 (Result i32) where + cast x := pure (x.toInt32) + @[spec] instance : Cast usize u32 where cast x := pure (USize.toUInt32 x) @@ -578,7 +663,19 @@ instance : Cast usize u32 where @[simp, spec] def hax_cast_op {α β} [c: Cast α β] (x:α) : (Result β) := c.cast x --- Results +end Cast + + +/- + +# Results + +Not to be confused with the underlying `Result` monad of the Lean encoding, the +`result_Result` type models the rust `Result`. + +-/ +section RustResult + inductive result_Result α β | ok : α -> result_Result α β | err : β -> result_Result α β @@ -589,27 +686,41 @@ instance {β : Type} : Monad (fun α => result_Result α β) where | .ok v => f v | .err e => .err e -inductive array_TryFromSliceError where - | array_TryFromSliceError +/-- Rust unwrapping, panics if `x` is not `result_Result.ok _` -/ +def result_impl_unwrap (α: Type) (β:Type) (x: result_Result α β) : (Result α) := + match x with + | .ok v => pure v + | .err _ => .fail .panic --- Assert -def assert (b:Bool) : Result Unit := - if b then pure () - else .fail (Error.assertionFailure) +end RustResult + + +/- -def assume : Prop -> Result Unit := fun _ => pure () -def prop_constructors_from_bool (b :Bool) : Prop := (b = true) +# Folds --- Hax +Hax represents for-loops as folds over a range +-/ +section Fold + +/-- + +Hax-introduced function for for-loops, represented as a fold of the body of the +loop `body` from index `e` to `s`. If the invariant is not checked at runtime, +only passed around + +-/ def hax_folds_fold_range {α} (s e : Nat) (inv : α -> Nat -> Result Bool) (init: α) - (f : α -> Nat -> Result α) : Result α := do + (body : α -> Nat -> Result α) : Result α := do if e ≤ s then pure init - else hax_folds_fold_range (s+1) e inv (← f init s) f + else hax_folds_fold_range (s+1) e inv (← body init s) body +-- Lemma for proof of hax_folds_fold_range property +private theorem induction_decreasing {e} {P: Nat → Prop} (init: P e) (rec: ∀ n, n < e → P (n+1) → P n) : @@ -630,6 +741,8 @@ theorem induction_decreasing {e} {P: Nat → Prop} suffices e - (d + 1) + 1 = e - d by grind omega +-- Lemma for proof of hax_folds_fold_range property +private def induction_decreasing_range {s e} {P: Nat → Nat → Prop} : s ≤ e → (init: P e e) → @@ -637,42 +750,60 @@ def induction_decreasing_range {s e} {P: Nat → Nat → Prop} : P s e := by intros; apply induction_decreasing (P := fun n => (s ≤ n → P n e)) (e := e) <;> try grind +/-- + +Nat-based specification for hax_folds_fold_range. It requires that the invariant +holds on the initial value, and that for any index `i` between the start and end +values, executing body of the loop on a value that satisfies the invariant +produces a result that also satisfies the invariant. + +-/ @[spec] theorem hax_folds_fold_range_spec {α} (s e : Nat) (inv : α -> Nat -> Result Bool) (init: α) - (f : α -> Nat -> Result α) : + (body : α -> Nat -> Result α) : ⦃ inv init s = pure true ∧ s ≤ e ∧ ∀ (acc:α) (i:Nat), s ≤ i → i < e → ⦃ inv acc i = pure true ⦄ - (f acc i) + (body acc i) ⦃ ⇓ res => inv res (i+1) = pure true ⦄ ⦄ - (hax_folds_fold_range s e inv init f) + (hax_folds_fold_range s e inv init body) ⦃ ⇓ r => inv r e = pure true ⦄ := by - intro ⟨ h_inv_s, h_s_le_e , h_f ⟩ + intro ⟨ h_inv_s, h_s_le_e , h_body ⟩ revert h_inv_s init have := induction_decreasing_range (s := s) (e := e) (P := fun s e => ∀ acc, inv acc s = pure true → - wp⟦hax_folds_fold_range s e inv acc f⟧ ⇓ r => inv r e = pure true) + wp⟦hax_folds_fold_range s e inv acc body⟧ ⇓ r => inv r e = pure true) apply this <;> clear this <;> try omega . simp [hax_folds_fold_range] . intros n _ _ ih acc h_acc unfold hax_folds_fold_range mvcgen <;> try grind - specialize h_f acc n (by omega) (by omega) - mspec h_f + specialize h_body acc n (by omega) (by omega) + mspec h_body intro h_r apply (ih _ h_r) -instance : Coe USize Nat where - coe x := x.toNat --- Arrays +end Fold + +/- + +# Arrays + +Rust arrays, are represented as Lean `Vector` (Lean Arrays of known size) + +-/ +section Array + +inductive array_TryFromSliceError where + | array_TryFromSliceError def hax_monomorphized_update_at_update_at_usize {α n} (a: Vector α n) (i:Nat) (v:α) : Result (Vector α n) := @@ -688,26 +819,53 @@ def hax_update_at {α n} (m : Vector α n) (i : Nat) (v : α) : Result (Vector else .fail (.arrayOutOfBounds) - -def result_impl_unwrap (α: Type) (β:Type) (x: result_Result α β) : (Result α) := - match x with - | .ok v => pure v - | .err _ => .fail .panic - --- Vectors @[spec] def hax_repeat {α} (v:α) (n:Nat) : Result (Vector α n) := pure (Vector.replicate n v) --- Ranges +def convert_TryInto_try_into {α n} (a: Array α) : + Result (result_Result (Vector α n) array_TryFromSliceError) := + pure ( + if h: a.size = n then + result_Result.ok (Eq.mp (congrArg _ h) a.toVector) + else + .err .array_TryFromSliceError + ) + +end Array + +/- + +# Ranges + +-/ +/-- Type of ranges -/ inductive ops_range_Range (α: Type) where | range (r_start r_end : α) : ops_range_Range α @[simp, spec] -def constr_ops_range_Range {α} {ops_range_Range_start : α} {ops_range_Range_end : α} := +def constr_ops_range_Range {α} (ops_range_Range_start : α) (ops_range_Range_end : α) := ops_range_Range.range ops_range_Range_start ops_range_Range_end + +/- + +# Polymorphic index access + +Hax introduces polymorphic index accesses, for any integer type (returning a +single value) and for ranges (returning an array of values) + +-/ +section PolymorphicIndexing + +/-- + +Until the backend introduces notations, a definition for the explicit name +`ops_index_index_index` is provided as a proxy + +-/ + @[simp, spec] def ops_index_Index_index {α β γ} (a: α) (i:β) [GetElem α β (Result γ) (fun _ _ => True) ] : (Result γ) := a[i] @@ -759,25 +917,25 @@ instance {α β : Type} {n : Nat} [tn: ToNat β]: GetElem (Vector α n) β (Resu instance {α : Type} {n : Nat}: GetElem (Vector α n) Nat (Result α) (fun _ _ => True) where getElem xs i _ := Result.ofOption xs[i]? .arrayOutOfBounds -@[spec] -theorem ops_index_Index_index_usize_range_vector_spec - (α : Type) (v: Vector α n ) (s e: usize) : - ⦃ s ≤ e ∧ e < n ⦄ - ( v[ ops_range_Range.range s e] : Result (Array α)) - ⦃ ⇓ r => r = (Vector.extract v s e).toArray ⦄ -:= by - mvcgen - simp - split <;> try split at * <;> try grind - all_goals simp [Vector.size] at * <;> try grind - intros - expose_names - cases h - . expose_names - cases h <;> try omega - . rw [← USize.lt_iff_toNat_lt] at * ; bv_decide - . sorry - . sorry +-- @[spec] +-- theorem ops_index_Index_index_usize_range_vector_spec +-- (α : Type) (v: Vector α n ) (s e: usize) : +-- ⦃ s ≤ e ∧ e < n ⦄ +-- ( v[ ops_range_Range.range s e] : Result (Array α)) +-- ⦃ ⇓ r => r = (Vector.extract v s e).toArray ⦄ +-- := by +-- mvcgen +-- simp +-- split <;> try split at * <;> try grind +-- all_goals simp [Vector.size] at * <;> try grind +-- intros +-- expose_names +-- cases h +-- . expose_names +-- cases h <;> try omega +-- . rw [← USize.lt_iff_toNat_lt] at * ; bv_decide +-- . sorry +-- . sorry @[spec] theorem ops_index_Index_index_usize_range_array_spec @@ -805,29 +963,35 @@ theorem ops_index_Index_index_usize_range_array_spec omega . split at * <;> try grind +end PolymorphicIndexing --- Arrays -section Arrays -def convert_TryInto_try_into {α n} (a: Array α) : - Result (result_Result (Vector α n) array_TryFromSliceError) := - pure ( - if h: a.size = n then - result_Result.ok (Eq.mp (congrArg _ h) a.toVector) - else - .err .array_TryFromSliceError - ) -end Arrays +/- + +# Slices + +Rust slices are represented as Lean Arrays (variable size) + +-/ --- Slices -def alloc_Global : Type := Unit @[spec] def unsize {α n} (a: Vector α n) : Result (Array α) := pure (a.toArray) def slice_impl_len α (a: Array α) : Result usize := pure a.size + +/- + +# Vectors + +Rust vectors are represented as Lean Arrays (variable size) + +-/ +section RustVectors + +def alloc_Global : Type := Unit def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α def vec_impl_new (α: Type) (Allocator:Type) : Result (vec_Vec α Allocator) := @@ -848,16 +1012,24 @@ instance {α n} : Coe (Array α) (Result (Vector α n)) where coe x := if h: x.size = n then by rw [←h] - apply Result.pure + apply pure apply (Array.toVector x) else .fail (.arrayOutOfBounds) +end RustVectors + + --- Bytes -def num_8_impl_to_le_bytes (_:u32) : Result (Vector u8 4) := pure (#v[0, 0, 0, 0]) -- TOFIX +/- +# Closures + +Rust closures are represented as regular Lean functions. Yet, Rust uses a +typeclass `Fn` when calling a closure, which uncurrifies the arguments. This is +taken care of by the `Fn` class + +-/ --- Closures class Fn α (β : outParam Type) γ where call : α → β → γ @@ -874,3 +1046,18 @@ def ops_function_Fn_call {α β γ} [Fn α β γ] (f: α) (x: β) : γ := Fn.cal def ops_deref_Deref_deref {α Allocator} (v: vec_Vec α Allocator) : Result (Array α) := pure v + + +-- Tactics +macro "hax_bv_decide" : tactic => `(tactic| ( + any_goals (injections <;> subst_vars) + all_goals try ( + simp [Int32.eq_iff_toBitVec_eq, + Int32.lt_iff_toBitVec_slt, + Int32.le_iff_toBitVec_sle, + Int64.eq_iff_toBitVec_eq, + Int64.lt_iff_toBitVec_slt, + Int64.le_iff_toBitVec_sle] at * <;> + bv_decide; + done + ))) From a6028da104235cbb39d3a63601346943cba3e91a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 18:00:11 +0200 Subject: [PATCH 23/44] Added missing implementations in Lib.lean --- hax-lib/proof-libs/lean/Lib.lean | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index f9a105a33..b5cf08ccd 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -596,13 +596,20 @@ abbrev hax__autogenerated_refinement__BoundedUsize_BoundedUsize -- {u : usize // lo ≤ u ∧ u ≤ hi} -- Todo : make it into a proper subtype -/-- [Warning] unimplemented yet -/ -noncomputable -def num_8_impl_from_le_bytes (x: Vector u8 n) : u32 := sorry -/-- [Warning] unimplemented yet -/ -noncomputable -def num_8_impl_to_le_bytes (_:u32) : Result (Vector u8 4) := sorry +def num__8_impl_from_le_bytes (x: Vector u8 4) : u32 := + x[0].toUInt32 + + (x[1].toUInt32 <<< 8) + + (x[2].toUInt32 <<< 16) + + (x[3].toUInt32 <<< 24) + +def num__8_impl_to_le_bytes (x:u32) : Result (Vector u8 4) := + #v[ + (x % 256).toUInt8, + (x >>> 8 % 256).toUInt8, + (x >>> 16 % 256).toUInt8, + (x >>> 24 % 256).toUInt8, + ] end Arithmetic From f12aa851b218b71c0795fdca98d0c84f56e5f22e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 18:00:25 +0200 Subject: [PATCH 24/44] Correct formatting --- rust-engine/src/main.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index 8d8dea7f3..f4ddadf07 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -24,7 +24,7 @@ fn lean_backend(items: Vec) { allocator.intersperse( " -- Experimental lean backend for Hax --- Comment the following line to not import the prelude (requires the Lib.lean file) : +-- Lib.lean can be found in hax/proof-libs/lean : import Lib import Std.Tactic.Do import Std.Do.Triple @@ -40,7 +40,9 @@ set_option linter.unusedVariables false" allocator.hardline() ]; - let items = items.iter().filter(|item: &&hax_rust_engine::ast::Item| Lean::printable_item(*item)); + let items = items + .iter() + .filter(|item: &&hax_rust_engine::ast::Item| Lean::printable_item(*item)); let item_docs: DocBuilder<_, Span> = header.append(allocator.intersperse(items, allocator.hardline())); From 7d00eb16c3cf4eec9ae86eac91931540ee900589 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 18:23:09 +0200 Subject: [PATCH 25/44] proof-lib/Lean Fix wrong names --- hax-lib/proof-libs/lean/Lib.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index b5cf08ccd..07caffedd 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -1004,10 +1004,10 @@ def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α def vec_impl_new (α: Type) (Allocator:Type) : Result (vec_Vec α Allocator) := pure ((List.nil).toArray) -def vec_1_impl_len (α: Type) (Allocator:Type) (x: vec_Vec α Allocator) : Result Nat := +def vec__1_impl_len (α: Type) (Allocator:Type) (x: vec_Vec α Allocator) : Result Nat := pure x.size -def vec_2_impl_extend_from_slice (α Allocator) (x: vec_Vec α Allocator) (y: Array α) +def vec__2_impl_extend_from_slice (α Allocator) (x: vec_Vec α Allocator) (y: Array α) : Result (vec_Vec α Allocator):= pure (x.append y) From 09b9268667136175323233da18420484d33c1739 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 19:13:36 +0200 Subject: [PATCH 26/44] Remove link to Lib.lean file --- examples/barrett/proofs/lean/extraction/Lib.lean | 1 - 1 file changed, 1 deletion(-) delete mode 120000 examples/barrett/proofs/lean/extraction/Lib.lean diff --git a/examples/barrett/proofs/lean/extraction/Lib.lean b/examples/barrett/proofs/lean/extraction/Lib.lean deleted file mode 120000 index e758df14c..000000000 --- a/examples/barrett/proofs/lean/extraction/Lib.lean +++ /dev/null @@ -1 +0,0 @@ -../../../../../proof-libs/lean/Lib.lean \ No newline at end of file From 7b664fa1518e53f42712487a99f3ab207151c482 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 1 Aug 2025 19:15:20 +0200 Subject: [PATCH 27/44] Promote test --- .../toolchain__lean-tests into-lean.snap | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index 1f9106ee8..d0e64f46f 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -30,7 +30,7 @@ diagnostics = [] "lean_tests.lean" = ''' -- Experimental lean backend for Hax --- Comment the following line to not import the prelude (requires the Lib.lean file) : +-- Lib.lean can be found in hax/proof-libs/lean : import Lib import Std.Tactic.Do import Std.Do.Triple @@ -40,12 +40,7 @@ open Std.Tactic set_option linter.unusedVariables false - - - - def FORTYTWO : usize := 42 - def returns42 (_ : hax_Tuple0) : Result usize := do FORTYTWO def add_two_numbers (x : usize) (y : usize) : Result usize := do (← x +? y) @@ -65,18 +60,9 @@ def closure (_ : hax_Tuple0) : Result i32 := do f2 (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) - - @[spec] - def test_before_verbatime_single_line : u8 := 42 -def 1__ : Result hax_Tuple0 := do hax_Tuple0 - - def multiline : Unit := () - -def test_before_verbatim_multi_line : u8 := 32 - -''' +def test_before_verbatim_multi_line : u8 := 32''' From 9d6b0a03d7f0dd5aae9b5bb4d6a44d10fa37024d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Sun, 3 Aug 2025 22:38:32 +0200 Subject: [PATCH 28/44] Remove spurious space at the end of lines --- rust-engine/src/lean.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 3651c988f..95a30d22b 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -431,7 +431,6 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { allocator, "constr_", constructor, - allocator.softline(), record_args ] .parens() From e9e0f51bd09b4f57f209196fdf34cfd840678637 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 4 Aug 2025 15:24:22 +0200 Subject: [PATCH 29/44] Remove warnings about [mvcgen] --- hax-lib/proof-libs/lean/Lib.lean | 2 ++ rust-engine/src/main.rs | 1 + 2 files changed, 3 insertions(+) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 07caffedd..6ad1cf625 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -16,6 +16,8 @@ import Std.Tactic.Do.Syntax open Std.Do open Std.Tactic +set_option mvcgen.warning false +set_option linter.unusedVariables false /- # Monadic encoding diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index f4ddadf07..080f91913 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -32,6 +32,7 @@ import Std.Tactic.Do.Syntax open Std.Do open Std.Tactic +set_option mvcgen.warning false set_option linter.unusedVariables false" .lines(), allocator.hardline(), From a1637dda1776c082a2f761b637209f7bc145acb1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 4 Aug 2025 15:25:10 +0200 Subject: [PATCH 30/44] Fix disambiguated name --- hax-lib/proof-libs/lean/Lib.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 6ad1cf625..0d08e6a45 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -585,10 +585,10 @@ for each implementation of typeclasses -/ @[simp, spec] -def num_8_impl_wrapping_add (x y: u32) : Result u32 := pure (x + y) +def num__8_impl_wrapping_add (x y: u32) : Result u32 := pure (x + y) -@[simp] -def num_8_impl_rotate_left (x: u32) (n: Nat) : Result u32 := +@[simp, spec] +def num__8_impl_rotate_left (x: u32) (n: Nat) : Result u32 := pure (UInt32.ofBitVec (BitVec.rotateLeft x.toBitVec n)) @@ -627,8 +627,8 @@ section Tuples abbrev hax_Tuple0 : Type := Unit def constr_hax_Tuple0 : hax_Tuple0 := () -instance : CoeDep Type hax_Tuple0 (Result hax_Tuple0) where - coe := pure () +instance : CoeDep Type hax_Tuple0 (hax_Tuple0) where + coe := () abbrev hax_Tuple1 (α: Type) : Type := α × Unit From ae6c26dbbe2959594360ee12b4a7c9befcc0bb5b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 4 Aug 2025 17:12:34 +0200 Subject: [PATCH 31/44] Introduce new notation for indexing --- hax-lib/proof-libs/lean/Lib.lean | 196 ++++++++++++++++++------------- 1 file changed, 117 insertions(+), 79 deletions(-) diff --git a/hax-lib/proof-libs/lean/Lib.lean b/hax-lib/proof-libs/lean/Lib.lean index 0d08e6a45..e82ea89f8 100644 --- a/hax-lib/proof-libs/lean/Lib.lean +++ b/hax-lib/proof-libs/lean/Lib.lean @@ -436,7 +436,13 @@ instance instHaxAdd : HaxAdd ISize where theorem HaxAdd_spec_bv (x y: isize) : ⦃ ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) ⦄ (x +? y) - ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd ] + ⦃ ⇓ r => r = x + y ⦄ := by mvcgen [instHaxAdd] + +theorem HaxAdd_spec_bv_rw (x y: isize) : + ¬ (BitVec.saddOverflow x.toBitVec y.toBitVec) → + x +? y = Result.ok (x + y) +:= by simp [instHaxAdd] + instance instHaxSub : HaxSub ISize where sub x y := @@ -863,10 +869,31 @@ def constr_ops_range_Range {α} (ops_range_Range_start : α) (ops_range_Range_en # Polymorphic index access Hax introduces polymorphic index accesses, for any integer type (returning a -single value) and for ranges (returning an array of values) +single value) and for ranges (returning an array of values). A typeclass-based +notation `a[i]_?` is introduced to support panicking lookups -/ -section PolymorphicIndexing +section Lookup + +/-- +The classes `GetElemResult` implement lookup notation `xs[i]_?`. +-/ +class GetElemResult (coll : Type u) (idx : Type v) (elem : outParam (Type w)) where + /-- + The syntax `arr[i]_?` gets the `i`'th element of the collection `arr`. It + can panic if the index is out of bounds. + -/ + getElemResult (xs : coll) (i : idx) : Result elem + +export GetElemResult (getElemResult) + +@[inherit_doc getElemResult] +syntax:max term noWs "[" withoutPosition(term) "]" noWs "_?": term +macro_rules | `($x[$i]_?) => `(getElemResult $x $i) + +@[app_unexpander getElemResult] meta def unexpandGetElemResult : Lean.PrettyPrinter.Unexpander + | `($_ $array $index) => `($array[$index]_?) + | _ => throw () /-- @@ -874,105 +901,116 @@ Until the backend introduces notations, a definition for the explicit name `ops_index_index_index` is provided as a proxy -/ - @[simp, spec] -def ops_index_Index_index {α β γ} (a: α) (i:β) - [GetElem α β (Result γ) (fun _ _ => True) ] : (Result γ) := a[i] +def ops_index_Index_index {α β γ} (a: α) (i:β) [GetElemResult α β γ] : (Result γ) := a[i]_? -@[simp] -instance : - GetElem + +instance Range.instGetElemResultArrayUSize : + GetElemResult (Array α) (ops_range_Range usize) - (Result (Array α)) (fun _ _ => True) where - getElem xs i _ := match i with + (Array α) where + getElemResult xs i := match i with | ops_range_Range.range s e => let size := xs.size; - if (s > e || e > size || s > size) then - Result.fail Error.arrayOutOfBounds - else + if s ≤ e && e ≤ size then pure ( xs.extract s e ) + else + Result.fail Error.arrayOutOfBounds -@[simp] -instance {α n} [tn: ToNat β]: - GetElem +instance Range.instGetElemResultVectorUSize : + GetElemResult (Vector α n) - (ops_range_Range β) - (Result (Array α)) (fun _ _ => True) where - getElem xs i _ := match i with + (ops_range_Range usize) + (Array α) where + getElemResult xs i := match i with | ops_range_Range.range s e => - let e := tn.toNat e; - let s := tn.toNat s; - let size := xs.size; - if (s > e || e > size || s > size) then - Result.fail Error.arrayOutOfBounds + if s ≤ e && e ≤ n then + pure (xs.extract s e).toArray else - pure ( (Vector.extract xs s e ).toArray) + Result.fail Error.arrayOutOfBounds -instance GetElemResult [tn: ToNat β] : GetElem (Array α) β (Result α) (fun _ _ => True) where - getElem xs i _ := Result.ofOption (xs[tn.toNat i]?) .arrayOutOfBounds -instance USize.instGetElemArrayResult {α} : GetElem (Array α) (usize) (Result α) (fun _ _ => True) := - GetElemResult +instance USize.instGetElemResultArray {α} : GetElemResult (Array α) usize α where + getElemResult xs i := + if h: i.toNat < xs.size then pure (xs[i]) + else .fail arrayOutOfBounds -instance : GetElem (Array α) Nat (Result α) (fun _ _ => True) := - GetElemResult +instance USize.instGetElemResultVector {α n} : GetElemResult (Vector α n) usize α where + getElemResult xs i := + if h: i.toNat < n then pure (xs[i.toNat]) + else .fail arrayOutOfBounds -@[simp] -instance {α β : Type} {n : Nat} [tn: ToNat β]: GetElem (Vector α n) β (Result α) (fun _ _ => True) where - getElem xs i _ := Result.ofOption (xs[tn.toNat i]?) .arrayOutOfBounds +instance Nat.instGetElemResultArray {α} : GetElemResult (Array α) Nat α where + getElemResult xs i := + if h: i < xs.size then pure (xs[i]) + else .fail arrayOutOfBounds -@[simp] -instance {α : Type} {n : Nat}: GetElem (Vector α n) Nat (Result α) (fun _ _ => True) where - getElem xs i _ := Result.ofOption xs[i]? .arrayOutOfBounds - --- @[spec] --- theorem ops_index_Index_index_usize_range_vector_spec --- (α : Type) (v: Vector α n ) (s e: usize) : --- ⦃ s ≤ e ∧ e < n ⦄ --- ( v[ ops_range_Range.range s e] : Result (Array α)) --- ⦃ ⇓ r => r = (Vector.extract v s e).toArray ⦄ --- := by --- mvcgen --- simp --- split <;> try split at * <;> try grind --- all_goals simp [Vector.size] at * <;> try grind --- intros --- expose_names --- cases h --- . expose_names --- cases h <;> try omega --- . rw [← USize.lt_iff_toNat_lt] at * ; bv_decide --- . sorry --- . sorry +instance Nat.instGetElemResultVector {α n} : GetElemResult (Vector α n) Nat α where + getElemResult xs i := + if h: i < n then pure (xs[i]) + else .fail arrayOutOfBounds + +@[spec] +theorem Nat.getElemArrayResult_spec + (α : Type) (a: Array α) (i: Nat): + ⦃ i < a.size ⦄ + ( a[i]_? ) + ⦃ ⇓ r => a[i]? = some r ⦄ +:= by + mvcgen [Result.ofOption, Nat.instGetElemResultArray] + simp + +@[spec] +theorem Nat.getElemVectorResult_spec + (α : Type) (n:Nat) (a: Vector α n) (i: Nat): + ⦃ i < n ⦄ + ( a[i]_? ) + ⦃ ⇓ r => a[i]? = some r ⦄ +:= by + mvcgen [Nat.instGetElemResultVector] + simp @[spec] -theorem ops_index_Index_index_usize_range_array_spec +theorem USize.getElemArrayResult_spec + (α : Type) (a: Array α) (i: usize): + ⦃ i.toNat < a.size ⦄ + ( a[i]_? ) + ⦃ ⇓ r => a[i.toNat]? = some r ⦄ +:= by + mvcgen [USize.instGetElemResultArray] + simp + +@[spec] +theorem USize.getElemVectorResult_spec + (α : Type) (n:Nat) (a: Vector α n) (i: usize): + ⦃ i.toNat < n ⦄ + ( a[i]_? ) + ⦃ ⇓ r => a[i.toNat]? = some r ⦄ +:= by + mvcgen [USize.instGetElemResultVector] + simp + +@[spec] +theorem Range.getElemArrayUSize_spec (α : Type) (a: Array α) (s e: usize) : ⦃ s ≤ e ∧ e ≤ a.size ⦄ - (a[ (ops_range_Range.range s e)]) + ( a[(ops_range_Range.range s e)]_? ) ⦃ ⇓ r => r = Array.extract a s e ⦄ := by - mvcgen [ops_index_Index_index, - USize.instGetElemArrayResult, - GetElemResult, Result.ofOption] <;> expose_names - simp [GetElem.getElem] - intros - split <;> try simp - . split at * - . grind - injections - subst_eqs - constructor - . split at * <;> injections - subst_eqs - expose_names - cases h_2 <;> try bv_decide - simp [USize.le_iff_toNat_le, USize.lt_iff_toNat_lt] at * - omega - . split at * <;> try grind + mvcgen [ops_index_Index_index, Range.instGetElemResultArrayUSize] <;> grind + +@[spec] +theorem Range.getElemVectorUSize_spec + (α : Type) (n: Nat) (a: Vector α n) (s e: usize) : + ⦃ s ≤ e ∧ e ≤ n ⦄ + ( a[(ops_range_Range.range s e)]_? ) + ⦃ ⇓ r => r = (Vector.extract a s e).toArray ⦄ +:= by + mvcgen [ops_index_Index_index, Range.instGetElemResultVectorUSize] <;> grind + -end PolymorphicIndexing +end Lookup From fd4def3d0951904c4804787bf95be29c87f5a55d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 4 Aug 2025 17:17:38 +0200 Subject: [PATCH 32/44] Update test snapshot --- .../src/snapshots/toolchain__lean-tests into-lean.snap | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index d0e64f46f..870526afd 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -38,6 +38,7 @@ import Std.Tactic.Do.Syntax open Std.Do open Std.Tactic +set_option mvcgen.warning false set_option linter.unusedVariables false def FORTYTWO : usize := 42 @@ -46,7 +47,7 @@ def returns42 (_ : hax_Tuple0) : Result usize := do FORTYTWO def add_two_numbers (x : usize) (y : usize) : Result usize := do (← x +? y) def letBinding (x : usize) (y : usize) : Result usize := do - let (useless : hax_Tuple0) ← pure (constr_hax_Tuple0 ); + let (useless : hax_Tuple0) ← pure (constr_hax_Tuple0); let (result1 : usize) ← pure (← x +? y); let (result2 : usize) ← pure (← result1 +? 2); (← result2 +? 1) @@ -55,10 +56,10 @@ def closure (_ : hax_Tuple0) : Result i32 := do let (f1 : (i32 -> Result i32)) ← pure (fun (y : i32)=> do (← y +? x)); let (f2 : (i32 -> i32 -> Result i32)) ← pure (fun (y : i32) (z : i32)=> do (← (← y +? x) +? z)); - (← (← ops_function_Fn_call f1 (constr_hax_Tuple1 (hax_Tuple1_Tuple0 := 1))) - +? (← ops_function_Fn_call + (← (← ops_function_Fn_call f1 (constr_hax_Tuple1 (hax_Tuple1_Tuple0 := 1))) +? + (← ops_function_Fn_call f2 - (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) + (constr_hax_Tuple2 (hax_Tuple2_Tuple0 := 2) (hax_Tuple2_Tuple1 := 3)))) @[spec] def test_before_verbatime_single_line : u8 := 42 From ac5f531d1e4d7d2087377ad55b6cc7b899726190 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 4 Aug 2025 17:31:07 +0200 Subject: [PATCH 33/44] Rust formatting --- rust-engine/src/lean.rs | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 95a30d22b..273b48938 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -427,15 +427,10 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { } else { None }; - docs![ - allocator, - "constr_", - constructor, - record_args - ] - .parens() - .group() - .nest(INDENT) + docs![allocator, "constr_", constructor, record_args] + .parens() + .group() + .nest(INDENT) } ExprKind::Match { scrutinee: _, From cbb4388344cc2df98a3da561bb85115b37e5edb7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 4 Aug 2025 18:44:25 +0200 Subject: [PATCH 34/44] OCaml formatting --- engine/backends/lean/lean_backend.ml | 1 - engine/bin/lib.ml | 10 ++-------- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/engine/backends/lean/lean_backend.ml b/engine/backends/lean/lean_backend.ml index cee16f2a2..8ade0879b 100644 --- a/engine/backends/lean/lean_backend.ml +++ b/engine/backends/lean/lean_backend.ml @@ -73,7 +73,6 @@ module BackendOptions = struct end open Ast - module U = Ast_utils.Make (InputLanguage) module Visitors = Ast_visitors.Make (InputLanguage) open AST diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index 8a8252270..e1fb08c52 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -259,7 +259,6 @@ let engine () = module ExportRustAst = Export_ast.Make (Features.Rust) module ExportLeanAst = Export_ast.Make (Lean_backend.InputLanguage) - (** Entry point for interacting with the Rust hax engine *) let driver_for_rust_engine () : unit = let query : Rust_engine_types.query = @@ -273,14 +272,9 @@ let driver_for_rust_engine () : unit = match query.kind with | Types.ImportThir { input } -> let imported_items = import_thir_items [] input in - let imported_items = - (* TODO: this let binding is applying the phases from the F* backend *) - Lean_backend.apply_phases imported_items - in + let imported_items = Lean_backend.apply_phases imported_items in let rust_ast_items = - List.concat_map - ~f:(fun item -> ExportLeanAst.ditem item) - imported_items + List.concat_map ~f:(fun item -> ExportLeanAst.ditem item) imported_items in let response = Rust_engine_types.ImportThir { output = rust_ast_items } in Hax_io.write_json ([%yojson_of: Rust_engine_types.response] response); From 766d7a0b6ddc9f8f523ddcfa021aaae85981b36d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 5 Aug 2025 15:20:43 +0200 Subject: [PATCH 35/44] Add missing dummy macros --- hax-lib/macros/src/dummy.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs index c89ce4e0a..57a5f4676 100644 --- a/hax-lib/macros/src/dummy.rs +++ b/hax-lib/macros/src/dummy.rs @@ -36,15 +36,19 @@ identity_proc_macro_attribute!( refinement_type, fstar_replace, coq_replace, + lean_replace, proverif_replace, fstar_replace_body, coq_replace_body, + lean_replace_body, proverif_replace_body, fstar_before, coq_before, + lean_before, proverif_before, fstar_after, coq_after, + lean_after, proverif_after, fstar_smt_pat, fstar_postprocess_with, @@ -59,6 +63,10 @@ pub fn coq_expr(_payload: TokenStream) -> TokenStream { quote! { () }.into() } #[proc_macro] +pub fn lean_expr(_payload: TokenStream) -> TokenStream { + quote! { () }.into() +} +#[proc_macro] pub fn proverif_expr(_payload: TokenStream) -> TokenStream { quote! { () }.into() } @@ -84,6 +92,10 @@ pub fn coq_unsafe_expr(_payload: TokenStream) -> TokenStream { unsafe_expr() } #[proc_macro] +pub fn lean_unsafe_expr(_payload: TokenStream) -> TokenStream { + unsafe_expr() +} +#[proc_macro] pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream { unsafe_expr() } @@ -97,6 +109,10 @@ pub fn coq_prop_expr(_payload: TokenStream) -> TokenStream { quote! {::hax_lib::Prop::from_bool(true)}.into() } #[proc_macro] +pub fn lean_prop_expr(_payload: TokenStream) -> TokenStream { + quote! {::hax_lib::Prop::from_bool(true)}.into() +} +#[proc_macro] pub fn proverif_prop_expr(_payload: TokenStream) -> TokenStream { quote! {::hax_lib::Prop::from_bool(true)}.into() } From e1c93f990ba5fd060331519751988d4c18a8cee2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 5 Aug 2025 17:10:25 +0200 Subject: [PATCH 36/44] Add missing entry for lean macros --- hax-lib/macros/src/utils.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs index 1dbc003d8..237b669af 100644 --- a/hax-lib/macros/src/utils.rs +++ b/hax-lib/macros/src/utils.rs @@ -10,6 +10,7 @@ impl ToTokens for HaxQuantifiers { quote! { use ::hax_lib::fstar::prop as fstar; use ::hax_lib::coq::prop as coq; + use ::hax_lib::lean::prop as lean; use ::hax_lib::proverif::prop as proverif; } .to_tokens(tokens) From 0176e015754c677cf48ee9bda6459c8efed35687 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 5 Aug 2025 17:13:16 +0200 Subject: [PATCH 37/44] Ocaml formatting --- engine/backends/lean/lean_backend.ml | 51 ++++++++++++++-------------- 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/engine/backends/lean/lean_backend.ml b/engine/backends/lean/lean_backend.ml index 8ade0879b..c838d95f1 100644 --- a/engine/backends/lean/lean_backend.ml +++ b/engine/backends/lean/lean_backend.ml @@ -20,31 +20,32 @@ include end) module SubtypeToInputLanguage - (FA : Features.T - with type mutable_reference = Features.Off.mutable_reference - and type continue = Features.Off.continue - and type break = Features.Off.break - and type mutable_reference = Features.Off.mutable_reference - and type mutable_pointer = Features.Off.mutable_pointer - and type mutable_variable = Features.Off.mutable_variable - and type reference = Features.Off.reference - and type raw_pointer = Features.Off.raw_pointer - and type early_exit = Features.Off.early_exit - and type question_mark = Features.Off.question_mark - and type as_pattern = Features.Off.as_pattern - and type lifetime = Features.Off.lifetime - and type monadic_action = Features.Off.monadic_action - and type arbitrary_lhs = Features.Off.arbitrary_lhs - and type nontrivial_lhs = Features.Off.nontrivial_lhs - and type loop = Features.Off.loop - and type block = Features.Off.block - and type for_loop = Features.Off.for_loop - and type while_loop = Features.Off.while_loop - and type for_index_loop = Features.Off.for_index_loop - and type state_passing_loop = Features.Off.state_passing_loop - and type fold_like_loop = Features.Off.fold_like_loop - and type match_guard = Features.Off.match_guard - and type trait_item_default = Features.Off.trait_item_default) = + (FA : + Features.T + with type mutable_reference = Features.Off.mutable_reference + and type continue = Features.Off.continue + and type break = Features.Off.break + and type mutable_reference = Features.Off.mutable_reference + and type mutable_pointer = Features.Off.mutable_pointer + and type mutable_variable = Features.Off.mutable_variable + and type reference = Features.Off.reference + and type raw_pointer = Features.Off.raw_pointer + and type early_exit = Features.Off.early_exit + and type question_mark = Features.Off.question_mark + and type as_pattern = Features.Off.as_pattern + and type lifetime = Features.Off.lifetime + and type monadic_action = Features.Off.monadic_action + and type arbitrary_lhs = Features.Off.arbitrary_lhs + and type nontrivial_lhs = Features.Off.nontrivial_lhs + and type loop = Features.Off.loop + and type block = Features.Off.block + and type for_loop = Features.Off.for_loop + and type while_loop = Features.Off.while_loop + and type for_index_loop = Features.Off.for_index_loop + and type state_passing_loop = Features.Off.state_passing_loop + and type fold_like_loop = Features.Off.fold_like_loop + and type match_guard = Features.Off.match_guard + and type trait_item_default = Features.Off.trait_item_default) = struct module FB = InputLanguage From 066beb445021f36527e1c863240da12af8179242 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 12 Aug 2025 14:59:39 +0200 Subject: [PATCH 38/44] Improve todo messages in the lean backend --- rust-engine/src/lean.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 273b48938..4c9a740df 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -15,7 +15,7 @@ use crate::ast::*; macro_rules! print_todo { ($allocator:ident) => { - $allocator.text(format!("Todo at {}", line!())).parens() + $allocator.text(format!("/- Unsupported by the Lean Backend (line {}) -/", line!())).parens() }; } @@ -169,7 +169,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ItemKind { ItemKind::Quote { quote, origin: _ } => quote.pretty(allocator), ItemKind::Error(_diagnostic) => print_todo!(allocator), ItemKind::Resugared(_resugared_ty_kind) => print_todo!(allocator), - ItemKind::NotImplementedYet => allocator.nil(), + ItemKind::NotImplementedYet => allocator.text("/- unsupported by Hax engine (yet) -/"), } } } From dba4160bad8aced3bf3472064dd87ab528bd8e32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 12 Aug 2025 16:31:53 +0200 Subject: [PATCH 39/44] Turned if-then Some else None into then_some() --- rust-engine/src/lean.rs | 79 ++++++++++++++++++++--------------------- 1 file changed, 38 insertions(+), 41 deletions(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 4c9a740df..cbfb011ef 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -15,7 +15,12 @@ use crate::ast::*; macro_rules! print_todo { ($allocator:ident) => { - $allocator.text(format!("/- Unsupported by the Lean Backend (line {}) -/", line!())).parens() + $allocator + .text(format!( + "/- Unsupported by the Lean Backend (line {}) -/", + line!() + )) + .parens() }; } @@ -355,20 +360,16 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { bounds_impls: _, trait_: _, } => { - let generic_args = if generic_args.is_empty() { - None - } else { - Some( - allocator - .line() - .append( - allocator - .intersperse(generic_args, allocator.line()) - .nest(INDENT), - ) - .group(), - ) - }; + let generic_args = !generic_args.is_empty().then_some( + allocator + .line() + .append( + allocator + .intersperse(generic_args, allocator.line()) + .nest(INDENT), + ) + .group(), + ); let args = if args.is_empty() { None } else { @@ -401,32 +402,28 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { base: _, } => { // Should be turned into a resugaring once https://github.com/cryspen/hax/pull/1528 have been merged - let record_args = if fields.len() > 0 { - Some( - allocator - .line() - .append( - allocator - .intersperse( - fields.iter().map(|field: &(GlobalId, Expr)| { - docs![ - allocator, - &field.0, - allocator.reflow(" := "), - &field.1 - ] - .parens() - .group() - }), - allocator.line(), - ) - .group(), - ) - .group(), - ) - } else { - None - }; + let record_args = (fields.len() > 0).then_some( + allocator + .line() + .append( + allocator + .intersperse( + fields.iter().map(|field: &(GlobalId, Expr)| { + docs![ + allocator, + &field.0, + allocator.reflow(" := "), + &field.1 + ] + .parens() + .group() + }), + allocator.line(), + ) + .group(), + ) + .group(), + ); docs![allocator, "constr_", constructor, record_args] .parens() .group() From 397c91ac5e8a1db021f2ec62004361740d08a242 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 12 Aug 2025 16:33:37 +0200 Subject: [PATCH 40/44] Remove commented-out code --- rust-engine/src/lean.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index cbfb011ef..95a9b9f2b 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -465,7 +465,6 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { _ => Some("← "), }; docs![allocator, monadic_encoding, e, allocator.reflow(" : "), ty] - //.nest(INDENT) .parens() .group() } @@ -492,7 +491,6 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { allocator.line(), body ] - //.nest(INDENT) .parens() .group() .nest(INDENT), From 667db1ba91025863e7ed4754b7cc6af5d3ef57d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 12 Aug 2025 16:36:47 +0200 Subject: [PATCH 41/44] Rewrote the If-Then-Else case for readability --- rust-engine/src/lean.rs | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 95a9b9f2b..43a9222b0 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -317,13 +317,23 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { } => match else_ { Some(else_branch) => docs![ allocator, - docs![allocator, "if", allocator.line(), condition].group(), + allocator + .text("if") + .append(allocator.line()) + .append(condition) + .group(), allocator.line(), - docs![allocator, "then", allocator.line(), then] + allocator + .text("then") + .append(allocator.line()) + .append(then) .group() .nest(INDENT), allocator.line(), - docs![allocator, "else", allocator.line(), else_branch] + allocator + .text("else") + .append(allocator.line()) + .append(else_branch) .group() .nest(INDENT), ] From 05dbc132cb61ded3a1e246406a250658ed9702b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Tue, 12 Aug 2025 17:45:03 +0200 Subject: [PATCH 42/44] Added documentation on debug printing functions for GlobalIds --- rust-engine/src/ast/identifiers.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/rust-engine/src/ast/identifiers.rs b/rust-engine/src/ast/identifiers.rs index 8282bd5c5..f4fa381ea 100644 --- a/rust-engine/src/ast/identifiers.rs +++ b/rust-engine/src/ast/identifiers.rs @@ -102,12 +102,14 @@ pub mod global_id { } } - /// Returns true if the GlobalId is actually empty (reduced to "_") + /// Tests if the raw output is reduced to "_". Should be used only for + /// testing. See https://github.com/cryspen/hax/issues/1599 pub fn is_empty(&self) -> bool { self.to_debug_string() == "_".to_string() } - /// Raw printing of identifier separated by underscore. Used for testing + /// Raw printing of identifier separated by underscore. Should be used + /// only for testing. See https://github.com/cryspen/hax/issues/1599 pub fn to_debug_string(&self) -> String { match self { GlobalId::Concrete(concrete_id) => concrete_id From 273073193080f683e90d664a900491f7c65c69c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 13 Aug 2025 09:19:10 +0200 Subject: [PATCH 43/44] Update CI job --- examples/default.nix | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/examples/default.nix b/examples/default.nix index 29f68c404..392536e44 100644 --- a/examples/default.nix +++ b/examples/default.nix @@ -8,6 +8,7 @@ hax-env, jq, proverif, + lean4, }: let commonArgs = import ./commonArgs.nix {inherit craneLib lib;}; cargoArtifacts = craneLib.buildDepsOnly commonArgs; @@ -29,7 +30,7 @@ in make ''; buildInputs = [ - hax hax-env fstar jq + hax hax-env fstar jq lean4 (proverif.overrideDerivation (_: { patches = [ ./proverif-psk/pv_div_by_zero_fix.diff ]; })) From 2b22eb107bbefbd8593368fa4c068240a97f7238 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 13 Aug 2025 09:45:52 +0200 Subject: [PATCH 44/44] Typo --- rust-engine/src/lean.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-engine/src/lean.rs b/rust-engine/src/lean.rs index 43a9222b0..45d1680e7 100644 --- a/rust-engine/src/lean.rs +++ b/rust-engine/src/lean.rs @@ -370,7 +370,7 @@ impl<'a, 'b> Pretty<'a, Allocator, Span> for &'b ExprKind { bounds_impls: _, trait_: _, } => { - let generic_args = !generic_args.is_empty().then_some( + let generic_args = (!generic_args.is_empty()).then_some( allocator .line() .append(