Add invariants for while loops.

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,8 +75,41 @@ struct
             body;
           }
         when Global_ident.eq_name Hax_lib___internal_loop_invariant f ->
-          { body; invariant = Some (pat, invariant) }
-      | _ -> { body; invariant = None }
+          {
+            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;
+          }
+        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; annotation = Some (LoopVariant invariant) }
+      | _ -> { body; annotation = None }
 
     type iterator =
       | Range of { start : B.expr; end_ : B.expr }
@@ -144,6 +181,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
@@ -206,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
@@ -220,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 ])
@@ -259,6 +312,39 @@ struct
                 (M.pat_PWild ~span ~typ:unit.typ, unit)
           in
           let body = dexpr 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:[]
@@ -276,8 +362,13 @@ 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 =
+            UB.make_closure [ bpat ] invariant invariant.span
+          in
+          let variant = UB.make_closure [ bpat ] variant variant.span in
+          UB.call fold_operator
+            [ condition; invariant; variant; init; body ]
+            span (dty span expr.typ)
       | Loop { state = None; _ } ->
           Error.unimplemented ~issue_id:405 ~details:"Loop without mutation"
             span

engine/names/src/lib.rs

@@ -30,6 +30,8 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(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() {
         use hax_lib::prop::*;
@@ -221,6 +223,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() {}
     }

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()
+}

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
             })
@@ -77,6 +86,28 @@ 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
+                use ::hax_lib::int::ToInt;
+                (#predicate).to_int()
+            })
+        }
+    }
+    .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`.

hax-lib/src/dummy.rs

@@ -44,7 +44,13 @@ pub fn inline_unsafe<T>(_: &str) -> T {
 }
 
 #[doc(hidden)]
-pub fn _internal_loop_invariant<T, R: Into<Prop>, P: FnOnce(T) -> R>(_: P) {}
+pub const fn _internal_loop_invariant<T, R: Into<Prop>, 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) {}
 
 pub trait Refinement {
     type InnerType;

hax-lib/src/implementation.rs

@@ -143,6 +143,14 @@ pub fn any_to_unit<T>(_: T) -> () {
 #[doc(hidden)]
 pub fn _internal_loop_invariant<T, R: Into<Prop>, 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) {}
+
 /// 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

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::{

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.

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);
 }