Loop invariants

.utils/list-names.sh

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+function pager() {
+ if command -v bat &> /dev/null; then
+ bat -l ml
+ else
+ less
+ fi
+}
+
+hax-engine-names-extract | sed '/include .val/,$d' | pager

engine/lib/ast_utils.ml

@@ -905,6 +905,13 @@ module Make (F : Features.T) = struct
  (`Concrete (Concrete_ident.of_name kind f_name))
  args span ret_typ
 
+ let make_closure (params : pat list) (body : expr) (span : span) : expr =
+ let params =
+ match params with [] -> [ make_wild_pat unit_typ span ] | _ -> params
+ in
+ let e = Closure { params; body; captures = [] } in
+ { e; typ = TArrow (List.map ~f:(fun p -> p.typ) params, body.typ); span }
+
  let string_lit span (s : string) : expr =
  { span; typ = TStr; e = Literal (String s) }
 
@@ -927,6 +934,23 @@ module Make (F : Features.T) = struct
  let item : AST.item -> Ast.Full.item = Stdlib.Obj.magic
  end
 
+ module Debug : sig
+ val expr : ?label:string -> AST.expr -> unit
+ (** Prints an expression pretty-printed as Rust, with its full
+ AST encoded as JSON, available as a file, so that one can
+ `jless` or `jq` into it. *)
+ end = struct
+ let expr ?(label = "") (e : AST.expr) : unit =
+ let path = tempfile_path ~suffix:".json" in
+ Core.Out_channel.write_all path
+ ~data:([%yojson_of: AST.expr] e |> Yojson.Safe.pretty_to_string);
+ let e = LiftToFullAst.expr e in
+ "```rust " ^ label ^ "\n" ^ Print_rust.pexpr_str e
+ ^ "\n```\x1b[34m JSON-encoded AST available at \x1b[1m" ^ path
+ ^ "\x1b[0m (hint: use `jless " ^ path ^ "`)"
+ |> Stdio.prerr_endline
+ end
+
  let unbox_expr' (next : expr -> expr) (e : expr) : expr =
  match e.e with
  | App { f = { e = GlobalVar f; _ }; args = [ e ]; _ }

engine/lib/phases/phase_functionalize_loops.ml

@@ -33,6 +33,127 @@ struct
  include Features.SUBTYPE.Id
  end
 
+ type body_and_invariant = {
+ body : B.expr;
+ invariant : (B.pat * B.expr) option;
+ }
+
+ let extract_loop_invariant (body : B.expr) : body_and_invariant =
+ 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;
+ }
+ when Global_ident.eq_name Hax_lib___internal_loop_invariant f ->
+ { body; invariant = Some (pat, invariant) }
+ | _ -> { body; invariant = None }
+
+ type iterator =
+ | Range of { start : B.expr; end_ : B.expr }
+ | Slice of B.expr
+ | ChunksExact of { size : B.expr; slice : B.expr }
+ | Enumerate of iterator
+ | StepBy of { n : B.expr; it : iterator }
+ [@@deriving show]
+
+ let rec as_iterator' (e : B.expr) : iterator option =
+ match e.e with
+ | Construct
+ {
+ constructor = `Concrete range_ctor;
+ is_record = true;
+ is_struct = true;
+ fields =
+ [ (`Concrete start_field, start); (`Concrete end_field, end_) ];
+ base = None;
+ }
+ when Concrete_ident.eq_name Core__ops__range__Range__start start_field
+ && Concrete_ident.eq_name Core__ops__range__Range range_ctor
+ && Concrete_ident.eq_name Core__ops__range__Range__end end_field ->
+ Some (Range { start; end_ })
+ | _ -> meth_as_iterator e
+
+ and as_iterator (e : B.expr) : iterator option =
+ let result = as_iterator' e in
+ (* UB.Debug.expr ~label:"as_iterator" e; *)
+ (* " = " ^ [%show: iterator option] result |> Stdio.prerr_endline; *)
+ result
+
+ and meth_as_iterator (e : B.expr) : iterator option =
+ let* f, args =
+ match e.e with
+ | App { f = { e = GlobalVar f; _ }; args; _ } -> Some (f, args)
+ | _ -> None
+ in
+ let f_eq n = Global_ident.eq_name n f in
+ let one_arg () = match args with [ x ] -> Some x | _ -> None in
+ let two_args () = match args with [ x; y ] -> Some (x, y) | _ -> None in
+ if f_eq Core__iter__traits__iterator__Iterator__step_by then
+ let* it, n = two_args () in
+ let* it = as_iterator it in
+ Some (StepBy { n; it })
+ else if
+ f_eq Core__iter__traits__collect__IntoIterator__into_iter
+ || f_eq Core__slice__Impl__iter
+ then
+ let* iterable = one_arg () in
+ match iterable.typ with
+ | TSlice _ | TArray _ -> Some (Slice iterable)
+ | _ -> as_iterator iterable
+ else if f_eq Core__iter__traits__iterator__Iterator__enumerate then
+ let* iterable = one_arg () in
+ let* iterator = as_iterator iterable in
+ Some (Enumerate iterator)
+ else if f_eq Core__slice__Impl__chunks_exact then
+ let* slice, size = two_args () in
+ Some (ChunksExact { size; slice })
+ else None
+
+ let fn_args_of_iterator (it : iterator) :
+ (Concrete_ident.name * B.expr list * B.ty) option =
+ let open Concrete_ident_generated in
+ let usize = B.TInt { size = SSize; signedness = Unsigned } in
+ match it with
+ | Enumerate (ChunksExact { size; slice }) ->
+ Some
+ ( Rust_primitives__hax__folds__fold_enumerated_chunked_slice,
+ [ size; slice ],
+ usize )
+ | Enumerate (Slice slice) ->
+ Some
+ ( Rust_primitives__hax__folds__fold_enumerated_slice,
+ [ slice ],
+ usize )
+ | StepBy { n; it = Range { start; end_ } } ->
+ Some
+ ( Rust_primitives__hax__folds__fold_range_step_by,
+ [ start; end_; n ],
+ start.typ )
+ | Range { start; end_ } ->
+ Some
+ (Rust_primitives__hax__folds__fold_range, [ start; end_ ], start.typ)
+ | _ -> None
+
  [%%inline_defs dmutability]
 
  let rec dexpr_unwrapped (expr : A.expr) : B.expr =
@@ -46,23 +167,31 @@ struct
  _;
  } ->
  let body = dexpr body in
+ let { body; invariant } = extract_loop_invariant body in
  let it = dexpr it in
  let pat = dpat pat in
  let bpat = dpat bpat in
- let fn : B.expr' =
- Closure { params = [ bpat; pat ]; body; captures = [] }
- in
- let fn : B.expr =
- {
- e = fn;
- typ = TArrow ([ bpat.typ; pat.typ ], body.typ);
- span = body.span;
- }
+ let fn : B.expr = UB.make_closure [ bpat; pat ] body body.span in
+ let init = dexpr init in
+ let f, kind, args =
+ match as_iterator it |> Option.bind ~f:fn_args_of_iterator with
+ | Some (f, args, typ) ->
+ let invariant : B.expr =
+ let default =
+ let span = expr.span in
+ let pat = UB.make_wild_pat typ span in
+ (pat, B.{ e = Literal (Bool true); typ = TBool; span })
+ in
+ let pat, invariant = Option.value ~default invariant in
+ UB.make_closure [ bpat; pat ] invariant invariant.span
+ in
+ (f, Concrete_ident.Kind.Value, args @ [ invariant; init; fn ])
+ | None ->
+ ( Core__iter__traits__iterator__Iterator__fold,
+ AssociatedItem Value,
+ [ it; init; fn ] )
  in
- UB.call ~kind:(AssociatedItem Value)
- Core__iter__traits__iterator__Iterator__fold
- [ it; dexpr init; fn ]
- span (dty span expr.typ)
+ UB.call ~kind f args span (dty span expr.typ)
  | Loop
  {
  body;

engine/lib/utils.ml

@@ -93,3 +93,17 @@ module MyInt64 = struct
 
  let yojson_of_t (int64 : t) : Yojson.Safe.t = `Intlit (to_string int64)
 end
+
+include (
+ struct
+ let id = ref 0
+
+ let tempfile_path ~suffix =
+ id := !id + 1;
+ Core.Filename.(
+ concat temp_dir_name ("hax-debug-" ^ Int.to_string !id ^ suffix))
+ end :
+ sig
+ val tempfile_path : suffix:string -> string
+ (** Generates a temporary file path that ends with `suffix` *)
+ end)

engine/names/src/lib.rs

@@ -29,6 +29,7 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
  assert!(true);
  assert_eq!(1, 1);
  hax_lib::assert!(true);
+ hax_lib::_internal_loop_invariant(|_: usize| true);
 
  let _ = [()].into_iter();
  let _: u16 = 6u8.into();
@@ -37,6 +38,14 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
  let _ = ..;
  let _ = ..1;
 
+ fn iterator_functions<It: Iterator + Clone>(it: It) {
+ let _ = it.clone().step_by(2);
+ let _ = it.clone().enumerate();
+ let _ = [()].chunks_exact(2);
+ let _ = [()].iter();
+ let _ = (&[()] as &[()]).iter();
+ }
+
  {
  use hax_lib::int::*;
  let a: Int = 3u8.lift();
@@ -163,6 +172,13 @@ mod hax {
  fn array_of_list() {}
  fn never_to_any() {}
 
+ mod folds {
+ fn fold_range() {}
+ fn fold_range_step_by() {}
+ fn fold_enumerated_slice() {}
+ fn fold_enumerated_chunked_slice() {}
+ }
+
  /// The engine uses this `dropped_body` symbol as a marker value
  /// to signal that a item was extracted without body.
  fn dropped_body() {}

flake.nix

@@ -152,6 +152,15 @@
  })
  ];
  in let
+ utils = pkgs.stdenv.mkDerivation {
+ name = "hax-dev-scripts";
+ phases = ["installPhase"];
+ installPhase = ''
+ mkdir -p $out/bin
+ cp ${./.utils/rebuild.sh} $out/bin/rebuild
+ cp ${./.utils/list-names.sh} $out/bin/list-names
+ '';
+ };
  packages = [
  ocamlformat
  pkgs.ocamlPackages.ocaml-lsp
@@ -168,14 +177,7 @@
  rustfmt
  rustc
 
- (pkgs.stdenv.mkDerivation {
- name = "rebuild-script";
- phases = ["installPhase"];
- installPhase = ''
- mkdir -p $out/bin
- cp ${./.utils/rebuild.sh} $out/bin/rebuild
- '';
- })
+ utils
  ];
  LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib";
  in {
@@ -191,6 +193,7 @@
  };
  default = pkgs.mkShell {
  inherit packages inputsFrom LIBCLANG_PATH;
+ shellHook = ''echo "Commands available: $(ls ${utils}/bin | tr '\n' ' ')"'';
  };
  };
  }

hax-lib-macros/src/lib.rs

@@ -40,6 +40,41 @@ pub fn fstar_options(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenS
  .into()
 }
 
+/// Add an invariant to a loop which deals with an index. The
+/// invariant cannot refer to any variable introduced within the
+/// loop. An invariant is a closure that takes one argument, the
+/// index, and returns a boolean.
+///
+/// Note that loop invariants are unstable (this will be handled in a
+/// better way in the future, see
+/// https://github.com/hacspec/hax/issues/858) and only supported on
+/// specific `for` loops with specific iterators:
+///
+/// - `for i in start..end {...}`
+/// - `for i in (start..end).step_by(n) {...}`
+/// - `for i in slice.enumerate() {...}`
+/// - `for i in slice.chunks_exact(n).enumerate() {...}`
+///
+/// This function must be called on the first line of a loop body to
+/// be effective. Note that in the invariant expression, `forall`,
+/// `exists`, and `BACKEND!` (`BACKEND` can be `fstar`, `proverif`,
+/// `coq`...) are in scope.
+#[proc_macro]
+pub fn loop_invariant(predicate: pm::TokenStream) -> pm::TokenStream {
+ let predicate: TokenStream = predicate.into();
+ let ts: pm::TokenStream = quote! {
+ #[cfg(#HaxCfgOptionName)]
+ {
+ hax_lib::_internal_loop_invariant({
+ #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`.

hax-lib/src/lib.rs

@@ -147,6 +147,10 @@ pub fn inline_unsafe<T>(_: &str) -> T {
  unreachable!()
 }
 
+/// A dummy function that holds a loop invariant.
+#[doc(hidden)]
+pub fn _internal_loop_invariant<T, P: FnOnce(T) -> bool>(_: P) {}
+
 /// 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,8 @@
 //! proc-macro crate cannot export anything but procedural macros.
 
 pub use hax_lib_macros::{
- attributes, ensures, exclude, impl_fn_decoration, include, lemma, opaque_type, refinement_type,
- requires, trait_fn_decoration,
+ attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type,
+ refinement_type, requires, trait_fn_decoration,
 };
 
 pub use hax_lib_macros::{