Merge pull request #643 from hacspec/refinements

Refinements

engine/backends/fstar/fstar_ast.ml

@@ -95,7 +95,8 @@ let parse_string f s =
     }
   in
   match parse (f (frag_of_text s)) with
-  | ParseError (_, err, _) -> failwith ("string_of_term: got error " ^ err)
+  | ParseError (_, err, _) ->
+      failwith ("string_of_term: got error [" ^ err ^ "] on input: [" ^ s ^ "]")
   | x -> x
 
 let term_of_string s =

engine/backends/fstar/fstar_backend.ml

@@ -197,15 +197,15 @@ struct
           ("pglobal_ident: expected to be handled somewhere else: "
          ^ show_global_ident id)
 
-  let plocal_ident (e : Local_ident.t) =
-    (* let name = U.Concrete_ident_view.local_ident e.name in *)
-    F.id
-    @@ U.Concrete_ident_view.local_ident
-         (match String.chop_prefix ~prefix:"impl " e.name with
-         | Some name ->
-             let name = "impl_" ^ Int.to_string ([%hash: string] name) in
-             { e with name }
-         | _ -> e)
+  let plocal_ident_str (e : Local_ident.t) =
+    U.Concrete_ident_view.local_ident
+      (match String.chop_prefix ~prefix:"impl " e.name with
+      | Some name ->
+          let name = "impl_" ^ Int.to_string ([%hash: string] name) in
+          { e with name }
+      | _ -> e)
+
+  let plocal_ident = plocal_ident_str >> F.id
 
   let pfield_ident span (f : global_ident) : F.Ident.lident =
     match f with
@@ -943,7 +943,21 @@ struct
           @@ F.AST.PatVar
                (F.id @@ U.Concrete_ident_view.to_definition_name name, None, [])
         in
-        F.decls ~quals:[ F.AST.Unfold_for_unification_and_vcgen ]
+        let ty, quals =
+          (* Adds a refinement if a refinement attribute is detected *)
+          match Attrs.associated_expr ~keep_last_args:1 Ensures e.attrs with
+          | Some { e = Closure { params = [ binder ]; body; _ }; _ } ->
+              let binder, _ =
+                U.Expect.pbinding_simple binder |> Option.value_exn
+              in
+              let ty =
+                F.mk_refined (plocal_ident_str binder) (pty e.span ty)
+                  (fun ~x -> pexpr body)
+              in
+              (ty, [])
+          | _ -> (pty e.span ty, [ F.AST.Unfold_for_unification_and_vcgen ])
+        in
+        F.decls ~quals
         @@ F.AST.TopLevelLet
              ( NoLetQualifier,
                [
@@ -953,7 +967,7 @@ struct
                           FStarBinder.(
                             of_generics e.span generics
                             |> List.map ~f:to_pattern) ),
-                   pty e.span ty );
+                   ty );
                ] )
     | Type { name; generics; _ }
       when Attrs.find_unique_attr e.attrs
@@ -1526,6 +1540,7 @@ module TransformToInputLanguage =
   |> Phases.Reject.As_pattern
   |> Phases.Traits_specs
   |> Phases.Simplify_hoisting
+  |> Phases.Newtype_as_refinement
   |> SubtypeToInputLanguage
   |> Identity
   ]

engine/lib/concrete_ident/concrete_ident.ml

@@ -338,6 +338,11 @@ module View = struct
       List.filter_map ~f:string_of_disambiguated_def_path_item def_id.path
       |> last_init |> Option.value_exn
     in
+    let path =
+      List.filter
+        ~f:(String.is_prefix ~prefix:"hax__autogenerated_refinement__" >> not)
+        path
+    in
     let sep = "__" in
     let subst = String.substr_replace_all ~pattern:sep ~with_:(sep ^ "_") in
     let fake_path, real_path =

engine/lib/diagnostics.ml

@@ -46,6 +46,7 @@ module Phase = struct
     | SimplifyHoisting
     | DropNeedlessReturns
     | TransformHaxLibInline
+    | NewtypeAsRefinement
     | DummyA
     | DummyB
     | DummyC

engine/lib/phases/phase_newtype_as_refinement.ml

@@ -0,0 +1,51 @@
+open! Prelude
+
+module Make (F : Features.T) =
+  Phase_utils.MakeMonomorphicPhase
+    (F)
+    (struct
+      let phase_id = Diagnostics.Phase.NewtypeAsRefinement
+
+      module A = Ast.Make (F)
+      module Visitors = Ast_visitors.Make (F)
+      open A
+
+      module Error = Phase_utils.MakeError (struct
+        let ctx = Diagnostics.Context.Phase phase_id
+      end)
+
+      module Attrs = Attr_payloads.MakeBase (Error)
+
+      let visitor =
+        object
+          inherit [_] Visitors.map as super
+
+          method! visit_expr () e =
+            match e.e with
+            | App { f = { e = GlobalVar f; _ }; args = [ inner ]; _ }
+              when Ast.Global_ident.eq_name Hax_lib__Refinement__new f
+                   || Ast.Global_ident.eq_name Hax_lib__RefineAs__refine f
+                   || Ast.Global_ident.eq_name Hax_lib__Refinement__get f ->
+                { e with e = Ascription { typ = e.typ; e = inner } }
+            | _ -> super#visit_expr () e
+
+          method! visit_item () i =
+            match i.v with
+            | Type
+                {
+                  name;
+                  generics;
+                  variants = [ { arguments = [ (_, ty, _) ]; _ } ];
+                  _;
+                }
+              when Attrs.find_unique_attr i.attrs
+                     ~f:
+                       ([%eq: Types.ha_payload] NewtypeAsRefinement
+                       >> Fn.flip Option.some_if ())
+                   |> Option.is_some ->
+                { i with v = TyAlias { name; generics; ty } }
+            | _ -> super#visit_item () i
+        end
+
+      let ditems = List.map ~f:(visitor#visit_item ())
+    end)

engine/lib/phases/phase_newtype_as_refinement.mli

@@ -0,0 +1,4 @@
+(** This phase transforms annotated struct definitions into (refined)
+type aliases. *)
+
+module Make : Phase_utils.UNCONSTRAINTED_MONOMORPHIC_PHASE

engine/names/src/lib.rs

@@ -48,6 +48,12 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     }
 
     let _ = hax_lib::inline("");
+    use hax_lib::{RefineAs, Refinement};
+
+    fn refinements<T: Refinement, U: RefineAs<T>>(x: T, y: U) -> T {
+        T::new(x.get());
+        y.refine()
+    }
 
     const _: () = {
         use core::{cmp::*, ops::*};

hax-lib-macros/src/lib.rs

@@ -690,3 +690,147 @@ macro_rules! make_quoting_proc_macro {
 make_quoting_proc_macro!(fstar(fstar_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar)
                          coq(coq_expr, coq_before, coq_after, coq_replace, hax_backend_coq)
                          proverif(proverif_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif));
+
+/// Marks a newtype `struct RefinedT(T);` as a refinement type. The
+/// struct should have exactly one unnamed private field.
+///
+/// This macro takes one argument: a boolean predicate that refines
+/// values of type `SomeType`.
+///
+/// For example, the following type defines bounded `u64` integers.
+///
+/// ```
+/// #[hax_lib::refinement_type(|x| x >= MIN && x <= MAX)]
+/// pub struct BoundedU64<const MIN: u64, const MAX: u64>(u64);
+/// ```
+///
+/// This macro will generate an implementation of the [`Deref`] trait
+/// and of the [`hax_lib::Refinement`] type. Those two traits are
+/// the only interface to this newtype: one is allowed only to
+/// construct or destruct refined type via those smart constructors
+/// and destructors, ensuring the abstraction.
+///
+/// A refinement of a type `T` with a formula `f` can be seen as a box
+/// that contains a value of type `T` and a proof that this value
+/// satisfies the formula `f`.
+///
+/// When extracted via hax, this is interpreted in the backend as a
+/// refinement type: the use of such a type yields static proof
+/// obligations.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn refinement_type(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let mut item = parse_macro_input!(item as syn::ItemStruct);
+
+    let syn::Fields::Unnamed(fields) = &item.fields else {
+        proc_macro_error::abort!(
+            item.generics.span(),
+            "Expected a newtype (a struct with one unnamed field), got one or more named field"
+        );
+    };
+    let paren_token = fields.paren_token;
+    let fields = fields.unnamed.iter().collect::<Vec<_>>();
+    let [field] = &fields[..] else {
+        proc_macro_error::abort!(
+            item.generics.span(),
+            "Expected a newtype (a struct with one unnamed field), got {} fields",
+            fields.len()
+        );
+    };
+    if field.vis != syn::Visibility::Inherited {
+        proc_macro_error::abort!(field.vis.span(), "This field was expected to be private");
+    }
+
+    let ExprClosure1 {
+        arg: ret_binder,
+        body: phi,
+    } = parse_macro_input!(attr);
+
+    let kind = FnDecorationKind::Ensures {
+        ret_binder: ret_binder.clone(),
+    };
+    let sig = syn::Signature {
+        constness: None,
+        asyncness: None,
+        unsafety: None,
+        abi: None,
+        variadic: None,
+        fn_token: syn::Token![fn](item.span()),
+        ident: parse_quote! {dummy},
+        generics: item.generics.clone(),
+        paren_token,
+        inputs: syn::punctuated::Punctuated::new(),
+        output: syn::ReturnType::Type(parse_quote! {->}, Box::new(field.ty.clone())),
+    };
+    let ident = &item.ident;
+    let generics = &item.generics;
+    let vis = item.vis.clone();
+    let generics_args: syn::punctuated::Punctuated<_, syn::token::Comma> = item
+        .generics
+        .params
+        .iter()
+        .map(|g| match g {
+            syn::GenericParam::Lifetime(p) => {
+                let i = &p.lifetime;
+                quote! { #i }
+            }
+            syn::GenericParam::Type(p) => {
+                let i = &p.ident;
+                quote! { #i }
+            }
+            syn::GenericParam::Const(p) => {
+                let i = &p.ident;
+                quote! { #i }
+            }
+        })
+        .collect();
+    let inner_ty = &field.ty;
+    let (refinement_item, refinement_attr) = make_fn_decoration(phi.clone(), sig, kind, None, None);
+    let module_ident = syn::Ident::new(
+        &format!("hax__autogenerated_refinement__{}", ident),
+        ident.span(),
+    );
+
+    item.vis = parse_quote! {pub};
+    let newtype_as_ref_attr = AttrPayload::NewtypeAsRefinement;
+    quote! {
+        #[allow(non_snake_case)]
+        mod #module_ident {
+            #refinement_item
+
+            #newtype_as_ref_attr
+            #refinement_attr
+            #item
+
+            #[::hax_lib::exclude]
+            impl #generics ::hax_lib::Refinement for #ident <#generics_args> {
+                type InnerType = #inner_ty;
+                fn new(x: Self::InnerType) -> Self {
+                    Self(x)
+                }
+                fn get(self) -> Self::InnerType {
+                    self.0
+                }
+            }
+
+            #[::hax_lib::exclude]
+            impl #generics ::std::ops::Deref for #ident <#generics_args> {
+                type Target = #inner_ty;
+                fn deref(&self) -> &Self::Target {
+                    &self.0
+                }
+            }
+
+            #[::hax_lib::exclude]
+            impl #generics ::hax_lib::RefineAs<#ident <#generics_args>> for #inner_ty {
+                fn refine(self) -> #ident <#generics_args> {
+                    use ::hax_lib::Refinement;
+                    #ident::new(self)
+                }
+            }
+        }
+        #vis use #module_ident::#ident;
+
+    }
+    .into()
+}

hax-lib-macros/types/src/lib.rs

@@ -119,6 +119,7 @@ pub enum AttrPayload {
     /// for pre- and post- conditions of a function we dropped the
     /// body of: pre and post are part of type signature)
     NeverDropBody,
+    NewtypeAsRefinement,
     /// Mark an item as a lemma statement to prove in the backend
     Lemma,
     Language,

hax-lib/src/lib.rs

@@ -140,3 +140,32 @@ pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
 /// Dummy function that carries a string to be printed as such in the output language
 #[doc(hidden)]
 pub fn inline(_: &str) {}
+
+/// 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
+/// type.
+///
+/// Please never implement this trait yourself, use the
+/// `refinement_type` macro instead.
+pub trait Refinement {
+    /// The base type
+    type InnerType;
+    /// Smart constructor capturing an invariant. Its extraction will
+    /// yield a proof obligation.
+    fn new(x: Self::InnerType) -> Self;
+    /// Destructor for the refined type
+    fn get(self) -> Self::InnerType;
+}
+
+/// A utilitary trait that provides a `refine` methods on traits that
+/// have a refined counter part. This trait is parametrized by a type
+/// `Target`: a base type can be refined in multiple ways.
+///
+/// Please never implement this trait yourself, use the
+/// `refinement_type` macro instead.
+pub trait RefineAs<Target> {
+    /// Smart constructor for `Target`. Its extraction will yield a
+    /// proof obligation.
+    fn refine(self) -> Target;
+}

hax-lib/src/proc_macros.rs

@@ -2,7 +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, requires,
+    attributes, ensures, exclude, impl_fn_decoration, include, lemma, opaque_type, refinement_type,
+    requires,
 };
 
 pub use hax_lib_macros::{