From 985057ad7f6f6058d8c2644de2e6bf23dcd1a486 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 28 Nov 2024 13:52:16 +0100 Subject: [PATCH] chore: udpate test snapshots --- .../toolchain__attributes into-fstar.snap | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index e65784071..f4b80beb2 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -338,6 +338,26 @@ let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_Bounded let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) = x +! x <: t_Even + +let t_BoundedAbsI16 (v_B: usize) = + x: + i16 + { (Rust_primitives.Hax.Int.from_machine v_B <: Hax_lib.Int.t_Int) < (32768 <: Hax_lib.Int.t_Int) && + (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) >= + (- (Rust_primitives.Hax.Int.from_machine v_B <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int) && + (Rust_primitives.Hax.Int.from_machine x <: Hax_lib.Int.t_Int) <= + (Rust_primitives.Hax.Int.from_machine v_B <: Hax_lib.Int.t_Int) } + +let double_abs_i16 (v_N v_M: usize) (x: t_BoundedAbsI16 v_N) + : Prims.Pure (t_BoundedAbsI16 v_M) + (requires + (Rust_primitives.Hax.Int.from_machine v_M <: Hax_lib.Int.t_Int) < + (32768 <: Hax_lib.Int.t_Int) && + (Rust_primitives.Hax.Int.from_machine v_M <: Hax_lib.Int.t_Int) = + ((Rust_primitives.Hax.Int.from_machine v_N <: Hax_lib.Int.t_Int) * (2 <: Hax_lib.Int.t_Int) + <: + Hax_lib.Int.t_Int)) + (fun _ -> Prims.l_True) = x *! 2s <: t_BoundedAbsI16 v_M ''' "Attributes.Requires_mut.fst" = ''' module Attributes.Requires_mut