Skip to content

Commit

Permalink
Test snapshots for new naming.
Browse files Browse the repository at this point in the history
  • Loading branch information
@maximebuyse
maximebuyse committed Jan 30, 2025
1 parent 2a3e840 commit 4e8dcb0
Show file tree
Hide file tree
Showing 27 changed files with 1,594 additions and 483 deletions.
6 changes: 3 additions & 3 deletions test-harness/src/snapshots/toolchain__assert into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,14 +45,14 @@ Import RecordSetNotations.

Definition asserts (_ : unit) : unit :=
let _ := assert (true) in
let _ := assert (t_PartialEq_f_eq (1) (1)) in
let _ := assert (f_eq (1) (1)) in
let _ := match (2,2) with
| (left_val,right_val) =>
assert (t_PartialEq_f_eq (left_val) (right_val))
assert (f_eq (left_val) (right_val))
end in
let _ := match (1,2) with
| (left_val,right_val) =>
assert (negb (t_PartialEq_f_eq (left_val) (right_val)))
assert (f_not (f_eq (left_val) (right_val)))
end in
tt.
'''
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__assert into-ssprove.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ Equations asserts {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit)
end in
letb _ := matchb prod_b (ret_both (1 : int32),ret_both (2 : int32)) with
| '(left_val,right_val) =>
solve_lift (assert (not (left_val =.? right_val)))
solve_lift (assert (f_not (left_val =.? right_val)))
end in
solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
Fail Next Obligation.
Expand Down
14 changes: 7 additions & 7 deletions test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,14 +86,14 @@ val v_C': u8
let v_C = v_C'
assume
val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
val impl_S1__ff_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)

let impl__S1__f_s1 = impl__S1__f_s1'
let impl_S1__ff_s1 = impl_S1__ff_s1'
assume
val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
val impl_S2__ff_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)

let impl__S2__f_s2 = impl__S2__f_s2'
let impl_S2__ff_s2 = impl_S2__ff_s2'
'''
"Attribute_opaque.fsti" = '''
module Attribute_opaque
Expand Down Expand Up @@ -124,7 +124,7 @@ class t_T (v_Self: Type0) = {
f_d_pre:Prims.unit -> Type0;
f_d_post:Prims.unit -> Prims.unit -> Type0;
f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result);
f_m_pre:self___: v_Self -> x: u8 -> pred: Type0{x =. mk_u8 0 ==> pred};
f_m_pre:self_: v_Self -> x: u8 -> pred: Type0{x =. mk_u8 0 ==> pred};
f_m_post:v_Self -> u8 -> bool -> Type0;
f_m:x0: v_Self -> x1: u8 -> Prims.Pure bool (f_m_pre x0 x1) (fun result -> f_m_post x0 x1 result)
}
Expand All @@ -146,9 +146,9 @@ val v_C:u8

type t_S1 = | S1 : t_S1

val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
val impl_S1__ff_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)

type t_S2 = | S2 : t_S2

val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
val impl_S2__ff_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
'''
70 changes: 35 additions & 35 deletions test-harness/src/snapshots/toolchain__attributes into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ let doing_nothing (_: Prims.unit)
: Prims.Pure Prims.unit
(requires true)
(ensures
fun v__x ->
let v__x:Prims.unit = v__x in
fun e_x ->
let e_x:Prims.unit = e_x in
true) = ()

let basically_a_constant (_: Prims.unit)
Expand Down Expand Up @@ -92,16 +92,6 @@ open FStar.Mul

unfold type t_Int = int

unfold let add x y = x + y

unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
{
f_Output = t_Int;
f_sub_pre = (fun (self: t_Int) (other: t_Int) -> true);
f_sub_post = (fun (self: t_Int) (other: t_Int) (out: t_Int) -> true);
f_sub = fun (self: t_Int) (other: t_Int) -> self + other
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_1': Core.Clone.t_Clone t_Int
Expand All @@ -113,6 +103,16 @@ assume
val impl': Core.Marker.t_Copy t_Int

let impl = impl'
unfold let add x y = x + y

unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
{
f_Output = t_Int;
f_sub_pre = (fun (self: t_Int) (other: t_Int) -> true);
f_sub_post = (fun (self: t_Int) (other: t_Int) (out: t_Int) -> true);
f_sub = fun (self: t_Int) (other: t_Int) -> self + other
}
'''
"Attributes.Issue_1266_.fst" = '''
module Attributes.Issue_1266_
Expand Down Expand Up @@ -146,12 +146,12 @@ let v_MAX: usize = mk_usize 10

type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} }

let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
let impl_SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
if i <. v_MAX
then Core.Option.Option_Some ({ f_i = i } <: t_SafeIndex) <: Core.Option.t_Option t_SafeIndex
else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex

let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
let impl_SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (mk_usize 10)) t_SafeIndex =
Expand Down Expand Up @@ -208,7 +208,7 @@ let impl: t_Operation t_ViaAdd =
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_1: t_Operation t_ViaMul =
let impl_Operation_for_ViaMul: t_Operation t_ViaMul =
{
f_double_pre
=
Expand All @@ -225,8 +225,8 @@ let impl_1: t_Operation t_ViaMul =
}

class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. mk_u8 100 ==> pred};
f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. mk_u8 88};
f_method_pre:self_: v_Self -> x: u8 -> pred: Type0{x <. mk_u8 100 ==> pred};
f_method_post:self_: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. mk_u8 88};
f_method:x0: v_Self -> x1: u8
-> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
}
Expand All @@ -249,7 +249,7 @@ type t_Foo = | Foo : u8 -> t_Foo
let impl: Core.Ops.Arith.t_Add t_Foo t_Foo =
{
f_Output = t_Foo;
f_add_pre = (fun (self___: t_Foo) (rhs: t_Foo) -> self___._0 <. (mk_u8 255 -! rhs._0 <: u8));
f_add_pre = (fun (self_: t_Foo) (rhs: t_Foo) -> self_._0 <. (mk_u8 255 -! rhs._0 <: u8));
f_add_post = (fun (self: t_Foo) (rhs: t_Foo) (out: t_Foo) -> true);
f_add = fun (self: t_Foo) (rhs: t_Foo) -> Foo (self._0 +! rhs._0) <: t_Foo
}
Expand All @@ -260,8 +260,8 @@ let impl_1: Core.Ops.Arith.t_Mul t_Foo t_Foo =
f_Output = t_Foo;
f_mul_pre
=
(fun (self___: t_Foo) (rhs: t_Foo) ->
rhs._0 =. mk_u8 0 || self___._0 <. (mk_u8 255 /! rhs._0 <: u8));
(fun (self_: t_Foo) (rhs: t_Foo) -> rhs._0 =. mk_u8 0 || self_._0 <. (mk_u8 255 /! rhs._0 <: u8)
);
f_mul_post = (fun (self: t_Foo) (rhs: t_Foo) (out: t_Foo) -> true);
f_mul = fun (self: t_Foo) (rhs: t_Foo) -> Foo (self._0 *! rhs._0) <: t_Foo
}
Expand All @@ -281,15 +281,15 @@ type t_MyArray = | MyArray : t_Array u8 (mk_usize 10) -> t_MyArray
Done vitae ullamcorper est.
Curabitur id dui eget sem viverra interdum. *)
let mutation_example
(use_generic_update_at: t_MyArray)
(use_specialized_update_at: t_Slice u8)
(uuse_generic_update_at: t_MyArray)
(uuse_specialized_update_at: t_Slice u8)
(specialized_as_well: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
: (t_MyArray & t_Slice u8 & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
let use_generic_update_at:t_MyArray =
Rust_primitives.Hax.update_at use_generic_update_at (mk_usize 2) (mk_u8 0)
let uuse_generic_update_at:t_MyArray =
Rust_primitives.Hax.update_at uuse_generic_update_at (mk_usize 2) (mk_u8 0)
in
let use_specialized_update_at:t_Slice u8 =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize use_specialized_update_at
let uuse_specialized_update_at:t_Slice u8 =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize uuse_specialized_update_at
(mk_usize 2)
(mk_u8 0)
in
Expand All @@ -298,15 +298,15 @@ let mutation_example
(mk_usize 2)
(mk_u8 0)
in
use_generic_update_at, use_specialized_update_at, specialized_as_well
uuse_generic_update_at, uuse_specialized_update_at, specialized_as_well
<:
(t_MyArray & t_Slice u8 & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl: Core.Ops.Index.t_Index t_MyArray usize =
{
f_Output = u8;
f_index_pre = (fun (self___: t_MyArray) (index: usize) -> index <. v_MAX);
f_index_pre = (fun (self_: t_MyArray) (index: usize) -> index <. v_MAX);
f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true);
f_index = fun (self: t_MyArray) (index: usize) -> self.[ index ]
}
Expand Down Expand Up @@ -339,7 +339,7 @@ let t_NoE =
{ let _, out:(Core.Str.Iter.t_Chars & bool) =
Core.Iter.Traits.Iterator.f_any #Core.Str.Iter.t_Chars
#FStar.Tactics.Typeclasses.solve
(Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String
(Core.Str.impl_str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String
#FStar.Tactics.Typeclasses.solve
x
<:
Expand Down Expand Up @@ -513,13 +513,13 @@ let swap_and_mut_req_ens (x y: u32)
let hax_temp_output:u32 = x +! y in
x, y, hax_temp_output <: (u32 & u32 & u32)

let issue_844_ (v__x: u8)
let issue_844_ (e_x: u8)
: Prims.Pure u8
Prims.l_True
(ensures
fun v__x_future ->
let v__x_future:u8 = v__x_future in
true) = v__x
fun e_x_future ->
let e_x_future:u8 = e_x_future in
true) = e_x

let add3_lemma (x: u32)
: Lemma Prims.l_True
Expand All @@ -533,7 +533,7 @@ type t_Foo = {
f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. mk_u32 3}
}

let inlined_code__V: u8 = mk_u8 12
let inlined_code__v_V: u8 = mk_u8 12

let before_inlined_code = "example before"

Expand All @@ -542,7 +542,7 @@ let inlined_code (foo: t_Foo) : Prims.unit =
let _:Prims.unit =
let x = foo.f_x in
let { f_y = y } = foo in
add3 ((fun _ -> 3ul) foo) vv_a inlined_code__V y
add3 ((fun _ -> 3ul) foo) vv_a inlined_code__v_V y
in
()

Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,13 +34,13 @@ open FStar.Mul

type t_Test = | Test : i32 -> t_Test

let impl__Test__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Test =
let impl_Test__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Test =
Core.Option.impl__map #i32 #t_Test x Test

type t_Context =
| Context_A : i32 -> t_Context
| Context_B : i32 -> t_Context

let impl__Context__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context =
let impl_Context__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context =
Core.Option.impl__map #i32 #t_Context x Context_B
'''
Loading

0 comments on commit 4e8dcb0

Please sign in to comment.