refactor(refinements): rename check to into_checked

engine/lib/phases/phase_newtype_as_refinement.ml

@@ -24,7 +24,7 @@ module Make (F : Features.T) =
             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__check f
+                   || Ast.Global_ident.eq_name Hax_lib__RefineAs__into_checked f
                    || Ast.Global_ident.eq_name Hax_lib__Refinement__get f ->
                 { e with e = Ascription { typ = e.typ; e = inner } }
             | _ -> super#visit_expr () e

engine/names/src/lib.rs

@@ -52,7 +52,7 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
 
     fn refinements<T: Refinement, U: RefineAs<T>>(x: T, y: U) -> T {
         T::new(x.get());
-        y.check()
+        y.into_checked()
     }
 
     const _: () = {

examples/chacha20/src/lib.rs

@@ -34,15 +34,63 @@ pub fn chacha20_quarter_round(
 use hax_lib::*;
 
 fn chacha20_double_round(state: State) -> State {
-    let state = chacha20_quarter_round(0.check(), 4.check(), 8.check(), 12.check(), state);
-    let state = chacha20_quarter_round(1.check(), 5.check(), 9.check(), 13.check(), state);
-    let state = chacha20_quarter_round(2.check(), 6.check(), 10.check(), 14.check(), state);
-    let state = chacha20_quarter_round(3.check(), 7.check(), 11.check(), 15.check(), state);
-
-    let state = chacha20_quarter_round(0.check(), 5.check(), 10.check(), 15.check(), state);
-    let state = chacha20_quarter_round(1.check(), 6.check(), 11.check(), 12.check(), state);
-    let state = chacha20_quarter_round(2.check(), 7.check(), 8.check(), 13.check(), state);
-    chacha20_quarter_round(3.check(), 4.check(), 9.check(), 14.check(), state)
+    let state = chacha20_quarter_round(
+        0.into_checked(),
+        4.into_checked(),
+        8.into_checked(),
+        12.into_checked(),
+        state,
+    );
+    let state = chacha20_quarter_round(
+        1.into_checked(),
+        5.into_checked(),
+        9.into_checked(),
+        13.into_checked(),
+        state,
+    );
+    let state = chacha20_quarter_round(
+        2.into_checked(),
+        6.into_checked(),
+        10.into_checked(),
+        14.into_checked(),
+        state,
+    );
+    let state = chacha20_quarter_round(
+        3.into_checked(),
+        7.into_checked(),
+        11.into_checked(),
+        15.into_checked(),
+        state,
+    );
+
+    let state = chacha20_quarter_round(
+        0.into_checked(),
+        5.into_checked(),
+        10.into_checked(),
+        15.into_checked(),
+        state,
+    );
+    let state = chacha20_quarter_round(
+        1.into_checked(),
+        6.into_checked(),
+        11.into_checked(),
+        12.into_checked(),
+        state,
+    );
+    let state = chacha20_quarter_round(
+        2.into_checked(),
+        7.into_checked(),
+        8.into_checked(),
+        13.into_checked(),
+        state,
+    );
+    chacha20_quarter_round(
+        3.into_checked(),
+        4.into_checked(),
+        9.into_checked(),
+        14.into_checked(),
+        state,
+    )
 }
 
 pub fn chacha20_rounds(state: State) -> State {

hax-bounded-integers/src/lib.rs

@@ -241,8 +241,8 @@ const _: () = {
 fn tests() {
     use hax_lib::*;
 
-    let x: BoundedU8<0, 5> = 2.check();
-    let y: BoundedU8<5, 10> = (x + x).check();
+    let x: BoundedU8<0, 5> = 2.into_checked();
+    let y: BoundedU8<5, 10> = (x + x).into_checked();
 
     let _ = x >> 3;
     let _ = x >> BoundedU8::<0, 5>::new(3);

hax-lib-macros/src/lib.rs

@@ -851,7 +851,7 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::
 
             #[::hax_lib::exclude]
             impl #generics ::hax_lib::RefineAs<#ident <#generics_args>> for #inner_ty {
-                fn check(self) -> #ident <#generics_args> {
+                fn into_checked(self) -> #ident <#generics_args> {
                     use ::hax_lib::Refinement;
                     #ident::new(self)
                 }

hax-lib/src/lib.rs

@@ -160,9 +160,9 @@ pub trait Refinement {
     fn invariant(value: Self::InnerType) -> bool;
 }
 
-/// A utilitary trait that provides a `check` method 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.
+/// A utilitary trait that provides a `into_checked` method 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.
@@ -176,5 +176,5 @@ pub trait RefineAs<RefinedType> {
     /// run-time, unless this behavior was disabled when defining the
     /// refinement type `RefinedType` with the `refinement_type` macro
     /// and its `no_debug_runtime_check` option.
-    fn check(self) -> RefinedType;
+    fn into_checked(self) -> RefinedType;
 }

tests/attributes/src/lib.rs

@@ -204,7 +204,7 @@ mod refinement_types {
 
     #[hax_lib::requires(x < 127)]
     pub fn double_refine(x: u8) -> Even {
-        (x + x).check()
+        (x + x).into_checked()
     }
 
     /// A string that contains no space.