From 1ffca88a2321c475ebffc8dfcd432998d98dcb49 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 25 Mar 2025 17:36:16 +0100 Subject: [PATCH 1/9] Add invariants for while loops. --- .../lib/phases/phase_functionalize_loops.ml | 21 +++++++++++++++-- hax-lib/src/dummy.rs | 2 +- .../rust_primitives/Rust_primitives.Hax.fst | 23 +++++++++++++++---- 3 files changed, 39 insertions(+), 7 deletions(-) diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index a583cbc6e..b125a913a 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -259,6 +259,7 @@ struct (M.pat_PWild ~span ~typ:unit.typ, unit) in let body = dexpr body in + let { body; invariant } = extract_loop_invariant body in let condition = dexpr condition in let condition : B.expr = M.expr_Closure ~params:[ bpat ] ~body:condition ~captures:[] @@ -276,8 +277,24 @@ struct | Some (BreakOnly, _) -> Rust_primitives__hax__while_loop_cf | None -> Rust_primitives__hax__while_loop in - UB.call fold_operator [ condition; init; body ] span - (dty span expr.typ) + let invariant : B.expr = + let default = MS.expr_Literal ~typ:TBool (Bool true) in + let invariant = + invariant |> Option.map ~f:snd |> Option.value ~default + in + UB.make_closure [ bpat ] invariant invariant.span + in + let fuel = + let kind = { size = S32; signedness = Unsigned } in + let e = + MS.expr_Literal ~typ:(TInt kind) + (Int { value = "0"; negative = false; kind }) + in + UB.make_closure [ bpat ] e e.span + in + UB.call fold_operator + [ condition; invariant; fuel; init; body ] + span (dty span expr.typ) | Loop { state = None; _ } -> Error.unimplemented ~issue_id:405 ~details:"Loop without mutation" span diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index fec739180..34977fbc0 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -44,7 +44,7 @@ pub fn inline_unsafe(_: &str) -> T { } #[doc(hidden)] -pub fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} +pub const fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} pub trait Refinement { type InnerType; diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst index cec5e6303..bdaa678d6 100644 --- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst +++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst @@ -63,7 +63,22 @@ class iterator_return (self: Type u#0): Type u#1 = { parent_iterator: Core.Iter.Traits.Iterator.t_Iterator self; f_fold_return: #b:Type0 -> s:self -> b -> (b -> i:parent_iterator.f_Item{parent_iterator.f_contains s i} -> Core.Ops.Control_flow.t_ControlFlow b b) -> Core.Ops.Control_flow.t_ControlFlow b b; } -let rec while_loop #s (condition: s -> bool) (init: s) (f: (i:s -> o:s{o << i})): s - = if condition init - then while_loop #s condition (f init) f - else init +let while_loop #acc_t + (condition: acc_t -> bool) + (inv: acc_t -> Type0) + (fuel: (a:acc_t{inv a} -> nat)) + (init: acc_t {inv init}) + (f: (i:acc_t{condition i /\ inv i} -> o:acc_t{inv o /\ fuel o < fuel i})): + (res: acc_t {inv res /\ not (condition res)}) + = + let rec while_loop_internal + (current: acc_t {inv current}): + Tot (res: acc_t {inv res /\ not (condition res)}) (decreases (fuel current)) + = if condition current + then + let next = f current in + assert (fuel next < fuel current); + while_loop_internal next + else current in + while_loop_internal init + From f19d80e85e70c5dc1e6f54b2f361ada52b3c50c9 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 26 Mar 2025 16:05:47 +0100 Subject: [PATCH 2/9] Add a macro to annotate while loops for termination proofs. --- .../lib/phases/phase_functionalize_loops.ml | 41 +++++++++++++++---- engine/names/src/lib.rs | 4 ++ hax-lib/macros/src/dummy.rs | 5 +++ hax-lib/macros/src/implementation.rs | 21 ++++++++++ hax-lib/src/dummy.rs | 3 ++ hax-lib/src/implementation.rs | 4 ++ hax-lib/src/proc_macros.rs | 5 ++- .../Rust_primitives.Hax.Folds.fsti | 20 +++++++++ 8 files changed, 92 insertions(+), 11 deletions(-) diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index b125a913a..5d7accd62 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -74,6 +74,25 @@ struct { body; invariant = Some (pat, invariant) } | _ -> { body; invariant = None } + let extract_loop_variant (body : B.expr) : B.expr * B.expr = + match body.e with + | Let + { + monadic = None; + lhs = { p = PWild; _ }; + rhs = { e = App { f = { e = GlobalVar f; _ }; args = [ e ]; _ }; _ }; + body; + } + when Global_ident.eq_name Hax_lib___internal_loop_decreases f -> + (body, e) + | _ -> + let kind = { size = S32; signedness = Unsigned } in + let e = + UB.M.expr_Literal ~typ:(TInt kind) ~span:body.span + (Int { value = "0"; negative = false; kind }) + in + (body, e) + type iterator = | Range of { start : B.expr; end_ : B.expr } | Slice of B.expr @@ -144,6 +163,16 @@ struct | None -> Rust_primitives__hax__folds__fold_enumerated_chunked_slice in Some (fold_op, [ size; slice ], usize) + | ChunksExact { size; slice } -> + let fold_op = + match cf with + | Some BreakOrReturn -> + Rust_primitives__hax__folds__fold_chunked_slice_return + | Some BreakOnly -> + Rust_primitives__hax__folds__fold_chunked_slice_cf + | None -> Rust_primitives__hax__folds__fold_chunked_slice + in + Some (fold_op, [ size; slice ], usize) | Enumerate (Slice slice) -> let fold_op = match cf with @@ -260,6 +289,7 @@ struct in let body = dexpr body in let { body; invariant } = extract_loop_invariant body in + let body, variant = extract_loop_variant body in let condition = dexpr condition in let condition : B.expr = M.expr_Closure ~params:[ bpat ] ~body:condition ~captures:[] @@ -284,16 +314,9 @@ struct in UB.make_closure [ bpat ] invariant invariant.span in - let fuel = - let kind = { size = S32; signedness = Unsigned } in - let e = - MS.expr_Literal ~typ:(TInt kind) - (Int { value = "0"; negative = false; kind }) - in - UB.make_closure [ bpat ] e e.span - in + let variant = UB.make_closure [ bpat ] variant variant.span in UB.call fold_operator - [ condition; invariant; fuel; init; body ] + [ condition; invariant; variant; init; body ] span (dty span expr.typ) | Loop { state = None; _ } -> Error.unimplemented ~issue_id:405 ~details:"Loop without mutation" diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index 0798c5902..f4730656d 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -30,6 +30,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu assert_eq!(1, 1); hax_lib::assert!(true); hax_lib::_internal_loop_invariant(|_: usize| true); + hax_lib::_internal_loop_decreases(hax_lib::Int::_unsafe_from_str("0")); fn props() { use hax_lib::prop::*; @@ -221,6 +222,9 @@ mod hax { fn fold_enumerated_chunked_slice() {} fn fold_enumerated_chunked_slice_cf() {} fn fold_enumerated_chunked_slice_return() {} + fn fold_chunked_slice() {} + fn fold_chunked_slice_cf() {} + fn fold_chunked_slice_return() {} fn fold_cf() {} fn fold_return() {} } diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs index 470d9e9b4..dab22dc70 100644 --- a/hax-lib/macros/src/dummy.rs +++ b/hax-lib/macros/src/dummy.rs @@ -188,3 +188,8 @@ pub fn trait_fn_decoration(_attr: TokenStream, _item: TokenStream) -> TokenStrea pub fn loop_invariant(_predicate: TokenStream) -> TokenStream { quote! {}.into() } + +#[proc_macro] +pub fn loop_decreases(_predicate: TokenStream) -> TokenStream { + quote! {}.into() +} diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index 7eec0184b..799a21807 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -77,6 +77,27 @@ pub fn loop_invariant(predicate: pm::TokenStream) -> pm::TokenStream { ts } +/// Must be used to prove termination of while loops. This takes an +/// expression that should be a usize that decreases at every iteration +/// +/// This function must be called just after `loop_invariant`, or at the first +/// line of the loop if there is no invariant. +#[proc_macro] +pub fn loop_decreases(predicate: pm::TokenStream) -> pm::TokenStream { + let predicate: TokenStream = predicate.into(); + let ts: pm::TokenStream = quote! { + #[cfg(#HaxCfgOptionName)] + { + hax_lib::_internal_loop_decreases({ + #HaxQuantifiers + #predicate + }) + } + } + .into(); + ts +} + /// When extracting to F*, inform about what is the current /// verification status for an item. It can either be `lax` or /// `panic_free`. diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 34977fbc0..0347759de 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -46,6 +46,9 @@ pub fn inline_unsafe(_: &str) -> T { #[doc(hidden)] pub const fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} +#[doc(hidden)] +pub const fn _internal_loop_decreases(_: ::hax_lib::Int) {} + pub trait Refinement { type InnerType; fn new(x: Self::InnerType) -> Self; diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index 17394252f..a307a8752 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -143,6 +143,10 @@ pub fn any_to_unit(_: T) -> () { #[doc(hidden)] pub fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} +/// A dummy function that holds a loop variant. +#[doc(hidden)] +pub fn _internal_loop_decreases(_: Int) {} + /// A type that implements `Refinement` should be a newtype for a /// type `T`. The field holding the value of type `T` should be /// private, and `Refinement` should be the only interface to the diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index 2d4cb0328..51d140602 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -2,8 +2,9 @@ //! proc-macro crate cannot export anything but procedural macros. pub use hax_lib_macros::{ - attributes, decreases, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, - opaque, opaque_type, refinement_type, requires, trait_fn_decoration, transparent, + attributes, decreases, ensures, exclude, impl_fn_decoration, include, lemma, loop_decreases, + loop_invariant, opaque, opaque_type, refinement_type, requires, trait_fn_decoration, + transparent, }; pub use hax_lib_macros::{ diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Folds.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Folds.fsti index 1b2602965..e5faa46ad 100644 --- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Folds.fsti +++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Folds.fsti @@ -37,6 +37,26 @@ val fold_enumerated_chunked_slice ) : result: acc_t {inv result (mk_int (Seq.length s / v chunk_size))} +/// Fold function that is generated for `for` loops iterating on +/// `s.chunks_exact(chunk_size)`-like iterators +val fold_chunked_slice + (#t: Type0) (#acc_t: Type0) + (chunk_size: usize {v chunk_size > 0}) + (s: t_Slice t) + (inv: acc_t -> (i:usize) -> Type0) + (init: acc_t {inv init (sz 0)}) + (f: ( acc:acc_t + -> item:(t_Slice t) { + length item == chunk_size /\ + inv acc (sz 0) + } + -> acc':acc_t { + inv acc' (sz 0) + } + ) + ) + : result: acc_t {inv result (mk_int 0)} + (**** `s.enumerate()` *) /// Fold function that is generated for `for` loops iterating on /// `s.enumerate()`-like iterators From 2fdca356f17ad1ad994ea35d505f0ac75d983d34 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Thu, 27 Mar 2025 17:59:23 +0100 Subject: [PATCH 3/9] Fix default case for loop variant. --- engine/lib/phases/phase_functionalize_loops.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index 5d7accd62..3bf2b4b1d 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -91,6 +91,16 @@ struct UB.M.expr_Literal ~typ:(TInt kind) ~span:body.span (Int { value = "0"; negative = false; kind }) in + let e = + UB.call Rust_primitives__hax__int__from_machine [ e ] e.span + (TApp + { + ident = + `Concrete + (Concrete_ident.of_name ~value:false Hax_lib__int__Int); + args = []; + }) + in (body, e) type iterator = From aa7b949f0c4c45da0e023ddc5fa98a86cd9976e0 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Mon, 31 Mar 2025 11:31:52 +0200 Subject: [PATCH 4/9] drive by arithmetic ops type fix --- proof-libs/fstar/core/Core.Ops.Arith.fsti | 34 +++++++++++------------ 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/proof-libs/fstar/core/Core.Ops.Arith.fsti b/proof-libs/fstar/core/Core.Ops.Arith.fsti index 9d4071fa0..1feb5123e 100644 --- a/proof-libs/fstar/core/Core.Ops.Arith.fsti +++ b/proof-libs/fstar/core/Core.Ops.Arith.fsti @@ -1,60 +1,60 @@ module Core.Ops.Arith open Rust_primitives - +open Hax_lib.Prop class t_Add self rhs = { [@@@ Tactics.Typeclasses.no_method] f_Output: Type; - f_add_pre: self -> rhs -> bool; - f_add_post: self -> rhs -> f_Output -> bool; + f_add_pre: self -> rhs -> t_Prop; + f_add_post: self -> rhs -> f_Output -> t_Prop; f_add: x:self -> y:rhs -> Pure f_Output (f_add_pre x y) (fun r -> f_add_post x y r); } class t_Sub self rhs = { [@@@ Tactics.Typeclasses.no_method] f_Output: Type; - f_sub_pre: self -> rhs -> bool; - f_sub_post: self -> rhs -> f_Output -> bool; + f_sub_pre: self -> rhs -> t_Prop; + f_sub_post: self -> rhs -> f_Output -> t_Prop; f_sub: x:self -> y:rhs -> Pure f_Output (f_sub_pre x y) (fun r -> f_sub_post x y r); } class t_Mul self rhs = { [@@@ Tactics.Typeclasses.no_method] f_Output: Type; - f_mul_pre: self -> rhs -> bool; - f_mul_post: self -> rhs -> f_Output -> bool; + f_mul_pre: self -> rhs -> t_Prop; + f_mul_post: self -> rhs -> f_Output -> t_Prop; f_mul: x:self -> y:rhs -> Pure f_Output (f_mul_pre x y) (fun r -> f_mul_post x y r); } class t_Div self rhs = { [@@@ Tactics.Typeclasses.no_method] f_Output: Type; - f_div_pre: self -> rhs -> bool; - f_div_post: self -> rhs -> f_Output -> bool; + f_div_pre: self -> rhs -> t_Prop; + f_div_post: self -> rhs -> f_Output -> t_Prop; f_div: x:self -> y:rhs -> Pure f_Output (f_div_pre x y) (fun r -> f_div_post x y r); } class t_AddAssign self rhs = { - f_add_assign_pre: self -> rhs -> bool; - f_add_assign_post: self -> rhs -> self -> bool; + f_add_assign_pre: self -> rhs -> t_Prop; + f_add_assign_post: self -> rhs -> self -> t_Prop; f_add_assign: x:self -> y:rhs -> Pure self (f_add_assign_pre x y) (fun r -> f_add_assign_post x y r); } class t_SubAssign self rhs = { - f_sub_assign_pre: self -> rhs -> bool; - f_sub_assign_post: self -> rhs -> self -> bool; + f_sub_assign_pre: self -> rhs -> t_Prop; + f_sub_assign_post: self -> rhs -> self -> t_Prop; f_sub_assign: x:self -> y:rhs -> Pure self (f_sub_assign_pre x y) (fun r -> f_sub_assign_post x y r); } class t_MulAssign self rhs = { - f_mul_assign_pre: self -> rhs -> bool; - f_mul_assign_post: self -> rhs -> self -> bool; + f_mul_assign_pre: self -> rhs -> t_Prop; + f_mul_assign_post: self -> rhs -> self -> t_Prop; f_mul_assign: x:self -> y:rhs -> Pure self (f_mul_assign_pre x y) (fun r -> f_mul_assign_post x y r); } class t_DivAssign self rhs = { - f_div_assign_pre: self -> rhs -> bool; - f_div_assign_post: self -> rhs -> self -> bool; + f_div_assign_pre: self -> rhs -> t_Prop; + f_div_assign_post: self -> rhs -> self -> t_Prop; f_div_assign: x:self -> y:rhs -> Pure self (f_div_assign_pre x y) (fun r -> f_div_assign_post x y r); } From 10882201ed39ce4f6a93210d76abb0994de550cf Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 31 Mar 2025 15:35:21 +0200 Subject: [PATCH 5/9] Fix for const fns in while loop. --- hax-lib/src/dummy.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 0347759de..7bb252952 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -44,10 +44,10 @@ pub fn inline_unsafe(_: &str) -> T { } #[doc(hidden)] -pub const fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} +pub const fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: &P) {} #[doc(hidden)] -pub const fn _internal_loop_decreases(_: ::hax_lib::Int) {} +pub const fn _internal_loop_decreases(_: int::Int) {} pub trait Refinement { type InnerType; From ffcd6b52df44e82965a759ed9657f10c3b9230ff Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 14 Apr 2025 09:31:16 +0200 Subject: [PATCH 6/9] Test for while loops with invariants. --- .../toolchain__loops into-fstar.snap | 32 +++++++++++++++++++ tests/loops/src/lib.rs | 10 ++++++ 2 files changed, 42 insertions(+) diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 4847191ef..c8268f3e7 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -208,6 +208,12 @@ let bigger_power_2_ (x: i32) : i32 = Rust_primitives.Hax.while_loop_cf (fun pow -> let pow:i32 = pow in pow <. mk_i32 1000000 <: bool) + (fun pow -> + let pow:i32 = pow in + true) + (fun pow -> + let pow:i32 = pow in + Rust_primitives.Hax.Int.from_machine (mk_u32 0) <: Hax_lib.Int.t_Int) pow (fun pow -> let pow:i32 = pow in @@ -842,6 +848,32 @@ let f (_: Prims.unit) : u8 = Rust_primitives.Hax.while_loop (fun x -> let x:u8 = x in x <. mk_u8 10 <: bool) + (fun x -> + let x:u8 = x in + true) + (fun x -> + let x:u8 = x in + Rust_primitives.Hax.Int.from_machine (mk_u32 0) <: Hax_lib.Int.t_Int) + x + (fun x -> + let x:u8 = x in + let x:u8 = x +! mk_u8 3 in + x) + in + x +! mk_u8 12 + +let while_invariant_decr (_: Prims.unit) : u8 = + let x:u8 = mk_u8 0 in + let x:u8 = + Rust_primitives.Hax.while_loop (fun x -> + let x:u8 = x in + x <. mk_u8 10 <: bool) + (fun x -> + let x:u8 = x in + x <=. mk_u8 10 <: bool) + (fun x -> + let x:u8 = x in + Rust_primitives.Hax.Int.from_machine (mk_u8 10 -! x <: u8) <: Hax_lib.Int.t_Int) x (fun x -> let x:u8 = x in diff --git a/tests/loops/src/lib.rs b/tests/loops/src/lib.rs index 143e7b86a..3cda49a22 100644 --- a/tests/loops/src/lib.rs +++ b/tests/loops/src/lib.rs @@ -138,6 +138,16 @@ mod while_loops { } x + 12 } + fn while_invariant_decr() -> u8 { + use hax_lib::ToInt; + let mut x = 0; + while x < 10 { + hax_lib::loop_invariant!(|_: usize| x <= 10); + hax_lib::loop_decreases!((10 - x).to_int()); + x = x + 3; + } + x + 12 + } } mod control_flow { From 4771791b90dbf19e30de38b8494282995e62b2d3 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 22 Apr 2025 17:04:34 +0200 Subject: [PATCH 7/9] While loops invariants improved. --- .../lib/phases/phase_functionalize_loops.ml | 111 ++++++++++++------ engine/names/src/lib.rs | 1 + hax-lib/macros/src/implementation.rs | 16 ++- hax-lib/src/dummy.rs | 3 + hax-lib/src/implementation.rs | 4 + .../toolchain__loops into-fstar.snap | 22 +++- tests/loops/src/lib.rs | 14 ++- 7 files changed, 129 insertions(+), 42 deletions(-) diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index 3bf2b4b1d..ee7decc19 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -39,12 +39,16 @@ struct include Features.SUBTYPE.Id end - type body_and_invariant = { + type loop_annotation_kind = + | LoopInvariant of { index_pat : B.pat option; invariant : B.expr } + | LoopVariant of B.expr + + type loop_annotation = { body : B.expr; - invariant : (B.pat * B.expr) option; + annotation : loop_annotation_kind option; } - let extract_loop_invariant (body : B.expr) : body_and_invariant = + let extract_loop_annotation (body : B.expr) : loop_annotation = match body.e with | Let { @@ -71,37 +75,41 @@ struct body; } when Global_ident.eq_name Hax_lib___internal_loop_invariant f -> - { body; invariant = Some (pat, invariant) } - | _ -> { body; invariant = None } - - let extract_loop_variant (body : B.expr) : B.expr * B.expr = - match body.e with + { + body; + annotation = + Some (LoopInvariant { index_pat = Some pat; invariant }); + } | Let { monadic = None; lhs = { p = PWild; _ }; - rhs = { e = App { f = { e = GlobalVar f; _ }; args = [ e ]; _ }; _ }; + rhs = + { + e = App { f = { e = GlobalVar f; _ }; args = [ invariant ]; _ }; + _; + }; + body; + } + when Global_ident.eq_name Hax_lib___internal_while_loop_invariant f -> + { + body; + annotation = Some (LoopInvariant { index_pat = None; invariant }); + } + | Let + { + monadic = None; + lhs = { p = PWild; _ }; + rhs = + { + e = App { f = { e = GlobalVar f; _ }; args = [ invariant ]; _ }; + _; + }; body; } when Global_ident.eq_name Hax_lib___internal_loop_decreases f -> - (body, e) - | _ -> - let kind = { size = S32; signedness = Unsigned } in - let e = - UB.M.expr_Literal ~typ:(TInt kind) ~span:body.span - (Int { value = "0"; negative = false; kind }) - in - let e = - UB.call Rust_primitives__hax__int__from_machine [ e ] e.span - (TApp - { - ident = - `Concrete - (Concrete_ident.of_name ~value:false Hax_lib__int__Int); - args = []; - }) - in - (body, e) + { body; annotation = Some (LoopVariant invariant) } + | _ -> { body; annotation = None } type iterator = | Range of { start : B.expr; end_ : B.expr } @@ -245,7 +253,7 @@ struct (M.pat_PWild ~span ~typ:unit.typ, unit) in let body = dexpr body in - let { body; invariant } = extract_loop_invariant body in + let { body; annotation } = extract_loop_annotation body in let it = dexpr it in let pat = dpat pat in let fn : B.expr = UB.make_closure [ bpat; pat ] body body.span in @@ -259,7 +267,13 @@ struct let pat = MS.pat_PWild ~typ in (pat, MS.expr_Literal ~typ:TBool (Bool true)) in - let pat, invariant = Option.value ~default invariant in + let pat, invariant = + match annotation with + | Some (LoopInvariant { index_pat = Some pat; invariant }) + -> + (pat, invariant) + | _ -> default + in UB.make_closure [ bpat; pat ] invariant invariant.span in (f, args @ [ invariant; init; fn ]) @@ -298,8 +312,39 @@ struct (M.pat_PWild ~span ~typ:unit.typ, unit) in let body = dexpr body in - let { body; invariant } = extract_loop_invariant body in - let body, variant = extract_loop_variant body in + let { body; annotation = annotation1 } = + extract_loop_annotation body + in + let { body; annotation = annotation2 } = + extract_loop_annotation body + in + let invariant = + match (annotation1, annotation2) with + | Some (LoopInvariant { index_pat = None; invariant }), _ + | _, Some (LoopInvariant { index_pat = None; invariant }) -> + invariant + | _ -> MS.expr_Literal ~typ:TBool (Bool true) + in + let variant = + match (annotation1, annotation2) with + | Some (LoopVariant variant), _ | _, Some (LoopVariant variant) -> + variant + | _ -> + let kind = { size = S32; signedness = Unsigned } in + let e = + UB.M.expr_Literal ~typ:(TInt kind) ~span:body.span + (Int { value = "0"; negative = false; kind }) + in + UB.call Rust_primitives__hax__int__from_machine [ e ] e.span + (TApp + { + ident = + `Concrete + (Concrete_ident.of_name ~value:false + Hax_lib__int__Int); + args = []; + }) + in let condition = dexpr condition in let condition : B.expr = M.expr_Closure ~params:[ bpat ] ~body:condition ~captures:[] @@ -318,10 +363,6 @@ struct | None -> Rust_primitives__hax__while_loop in let invariant : B.expr = - let default = MS.expr_Literal ~typ:TBool (Bool true) in - let invariant = - invariant |> Option.map ~f:snd |> Option.value ~default - in UB.make_closure [ bpat ] invariant invariant.span in let variant = UB.make_closure [ bpat ] variant variant.span in diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index f4730656d..12f1e98b9 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -30,6 +30,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu assert_eq!(1, 1); hax_lib::assert!(true); hax_lib::_internal_loop_invariant(|_: usize| true); + hax_lib::_internal_while_loop_invariant(hax_lib::Prop::from(true)); hax_lib::_internal_loop_decreases(hax_lib::Int::_unsafe_from_str("0")); fn props() { diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index 799a21807..0b157e31d 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -63,11 +63,20 @@ pub fn fstar_options(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenS /// `coq`...) are in scope. #[proc_macro] pub fn loop_invariant(predicate: pm::TokenStream) -> pm::TokenStream { - let predicate: TokenStream = predicate.into(); + let predicate2: TokenStream = predicate.clone().into(); + let predicate_expr: syn::Expr = parse_macro_input!(predicate); + + let (invariant_f, predicate) = match predicate_expr { + syn::Expr::Closure(_) => (quote!(hax_lib::_internal_loop_invariant), predicate2), + _ => ( + quote!(hax_lib::_internal_while_loop_invariant), + quote!(::hax_lib::Prop::from(#predicate2)), + ), + }; let ts: pm::TokenStream = quote! { #[cfg(#HaxCfgOptionName)] { - hax_lib::_internal_loop_invariant({ + #invariant_f({ #HaxQuantifiers #predicate }) @@ -90,7 +99,8 @@ pub fn loop_decreases(predicate: pm::TokenStream) -> pm::TokenStream { { hax_lib::_internal_loop_decreases({ #HaxQuantifiers - #predicate + use ::hax_lib::int::ToInt; + (#predicate).to_int() }) } } diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 7bb252952..27f58241d 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -46,6 +46,9 @@ pub fn inline_unsafe(_: &str) -> T { #[doc(hidden)] pub const fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: &P) {} +#[doc(hidden)] +pub const fn _internal_while_loop_invariant(_: Prop) {} + #[doc(hidden)] pub const fn _internal_loop_decreases(_: int::Int) {} diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index a307a8752..2ad484eca 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -143,6 +143,10 @@ pub fn any_to_unit(_: T) -> () { #[doc(hidden)] pub fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} +/// A dummy function that holds a while loop invariant. +#[doc(hidden)] +pub const fn _internal_while_loop_invariant(_: Prop) {} + /// A dummy function that holds a loop variant. #[doc(hidden)] pub fn _internal_loop_decreases(_: Int) {} diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index c8268f3e7..99ff3df1e 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -870,7 +870,27 @@ let while_invariant_decr (_: Prims.unit) : u8 = x <. mk_u8 10 <: bool) (fun x -> let x:u8 = x in - x <=. mk_u8 10 <: bool) + b2t (x <=. mk_u8 10 <: bool)) + (fun x -> + let x:u8 = x in + Rust_primitives.Hax.Int.from_machine (mk_u8 10 -! x <: u8) <: Hax_lib.Int.t_Int) + x + (fun x -> + let x:u8 = x in + let x:u8 = x +! mk_u8 3 in + x) + in + x +! mk_u8 12 + +let while_invariant_decr_rev (_: Prims.unit) : u8 = + let x:u8 = mk_u8 0 in + let x:u8 = + Rust_primitives.Hax.while_loop (fun x -> + let x:u8 = x in + x <. mk_u8 10 <: bool) + (fun x -> + let x:u8 = x in + b2t (x <=. mk_u8 10 <: bool)) (fun x -> let x:u8 = x in Rust_primitives.Hax.Int.from_machine (mk_u8 10 -! x <: u8) <: Hax_lib.Int.t_Int) diff --git a/tests/loops/src/lib.rs b/tests/loops/src/lib.rs index 3cda49a22..53f77ce4e 100644 --- a/tests/loops/src/lib.rs +++ b/tests/loops/src/lib.rs @@ -139,11 +139,19 @@ mod while_loops { x + 12 } fn while_invariant_decr() -> u8 { - use hax_lib::ToInt; let mut x = 0; while x < 10 { - hax_lib::loop_invariant!(|_: usize| x <= 10); - hax_lib::loop_decreases!((10 - x).to_int()); + hax_lib::loop_invariant!(x <= 10); + hax_lib::loop_decreases!(10 - x); + x = x + 3; + } + x + 12 + } + fn while_invariant_decr_rev() -> u8 { + let mut x = 0; + while x < 10 { + hax_lib::loop_decreases!(10 - x); + hax_lib::loop_invariant!(x <= 10); x = x + 3; } x + 12 From ea5463249c2b2963a00e9e4798d337d8f72aa925 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 22 Apr 2025 17:41:29 +0200 Subject: [PATCH 8/9] Make from_bool const. --- hax-lib/src/prop.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib/src/prop.rs b/hax-lib/src/prop.rs index 8d3ee3d93..599b640b9 100644 --- a/hax-lib/src/prop.rs +++ b/hax-lib/src/prop.rs @@ -9,7 +9,7 @@ pub struct Prop(bool); /// Hax rewrite more elaborated versions (see `forall` or `AndBit` below) to those monomorphic constructors. pub mod constructors { use super::Prop; - pub fn from_bool(b: bool) -> Prop { + pub const fn from_bool(b: bool) -> Prop { Prop(b) } pub fn and(lhs: Prop, other: Prop) -> Prop { @@ -46,7 +46,7 @@ pub mod constructors { impl Prop { /// Lifts a boolean to a logical proposition. - pub fn from_bool(b: bool) -> Self { + pub const fn from_bool(b: bool) -> Self { constructors::from_bool(b) } /// Conjuction of two propositions. From 3d2ff045c9e2738c20127fb396a90d2231dfd242 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 23 Apr 2025 15:18:26 +0200 Subject: [PATCH 9/9] Improve style for while loops invariants. --- .../lib/phases/phase_functionalize_loops.ml | 83 +++++++------------ 1 file changed, 29 insertions(+), 54 deletions(-) diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index ee7decc19..2c57940cf 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -49,68 +49,43 @@ struct } let extract_loop_annotation (body : B.expr) : loop_annotation = - match body.e with - | Let - { - monadic = None; - lhs = { p = PWild; _ }; - rhs = - { - e = - App - { - f = { e = GlobalVar f; _ }; - args = - [ - { - e = - Closure { params = [ pat ]; body = invariant; _ }; - _; - }; - ]; - _; - }; - _; - }; - body; - } + let rhs_body = + let* (e_let : UB.D.expr_Let) = UB.D.expr_Let body in + let*? _ = Option.is_none e_let.monadic in + let* _ = UB.D.pat_PWild e_let.lhs in + let* app = UB.D.expr_App e_let.rhs in + let* f = UB.D.expr_GlobalVar app.f in + Some (f, app.args, e_let.body) + in + match rhs_body with + | Some + ( f, + [ { e = Closure { params = [ pat ]; body = invariant; _ }; _ } ], + body ) when Global_ident.eq_name Hax_lib___internal_loop_invariant f -> { body; annotation = Some (LoopInvariant { index_pat = Some pat; invariant }); } - | Let - { - monadic = None; - lhs = { p = PWild; _ }; - rhs = - { - e = App { f = { e = GlobalVar f; _ }; args = [ invariant ]; _ }; - _; - }; - body; - } + | Some (f, [ invariant ], body) when Global_ident.eq_name Hax_lib___internal_while_loop_invariant f -> { body; annotation = Some (LoopInvariant { index_pat = None; invariant }); } - | Let - { - monadic = None; - lhs = { p = PWild; _ }; - rhs = - { - e = App { f = { e = GlobalVar f; _ }; args = [ invariant ]; _ }; - _; - }; - body; - } + | Some (f, [ invariant ], body) when Global_ident.eq_name Hax_lib___internal_loop_decreases f -> { body; annotation = Some (LoopVariant invariant) } | _ -> { body; annotation = None } + let expect_invariant_variant (annotation1 : loop_annotation_kind option) + (annotation2 : loop_annotation_kind option) : + loop_annotation_kind option * loop_annotation_kind option = + match annotation1 with + | Some (LoopVariant _) -> (annotation2, annotation1) + | _ -> (annotation1, annotation2) + type iterator = | Range of { start : B.expr; end_ : B.expr } | Slice of B.expr @@ -318,17 +293,17 @@ struct let { body; annotation = annotation2 } = extract_loop_annotation body in + let invariant, variant = + expect_invariant_variant annotation1 annotation2 + in let invariant = - match (annotation1, annotation2) with - | Some (LoopInvariant { index_pat = None; invariant }), _ - | _, Some (LoopInvariant { index_pat = None; invariant }) -> - invariant + match invariant with + | Some (LoopInvariant { index_pat = None; invariant }) -> invariant | _ -> MS.expr_Literal ~typ:TBool (Bool true) in let variant = - match (annotation1, annotation2) with - | Some (LoopVariant variant), _ | _, Some (LoopVariant variant) -> - variant + match variant with + | Some (LoopVariant variant) -> variant | _ -> let kind = { size = S32; signedness = Unsigned } in let e =