feat(bounded-ints): add refinement_int macro

hacspec · Jun 18, 2024 · 07660f8 · 07660f8
1 parent 0547d73
commit 07660f8
Show file tree

Hide file tree

Showing 8 changed files with 219 additions and 68 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/engine/lib/phases/phase_newtype_as_refinement.ml b/engine/lib/phases/phase_newtype_as_refinement.ml
@@ -25,6 +25,7 @@ module Make (F : Features.T) =
             | 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__into_checked f
+                   || Ast.Global_ident.eq_name Hax_lib__Refinement__get_mut f
                    || Ast.Global_ident.eq_name Hax_lib__Refinement__get f ->
                 { e with e = Ascription { typ = e.typ; e = inner } }
             | _ -> super#visit_expr () e

diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs
@@ -51,6 +51,7 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     use hax_lib::{RefineAs, Refinement};
 
     fn refinements<T: Refinement, U: RefineAs<T>>(x: T, y: U) -> T {
+        let _ = x.get_mut();
         T::new(x.get());
         y.into_checked()
     }

diff --git a/hax-bounded-integers/Cargo.toml b/hax-bounded-integers/Cargo.toml
@@ -9,4 +9,6 @@ repository.workspace = true
 readme.workspace = true
 
 [dependencies]
+duplicate = "1.0.0"
 hax-lib.workspace = true
+paste = "1.0.15"