Skip to content

Commit

Permalink
fix(engine/fstar): add tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@W95Psp
Lucas Franceschino authored and W95Psp committed Jun 26, 2024
1 parent be55d48 commit 35145cc
Show file tree
Hide file tree
Showing 10 changed files with 331 additions and 124 deletions.
4 changes: 2 additions & 2 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 @@ -37,7 +37,7 @@ module Attribute_opaque
open Core
open FStar.Mul

val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
val t_OpaqueEnum (#v_X: usize) (#v_T #v_U: Type0) : Type0

val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
val t_OpaqueStruct (#v_X: usize) (#v_T #v_U: Type0) : Type0
'''
12 changes: 6 additions & 6 deletions test-harness/src/snapshots/toolchain__attributes into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index #(t_Array v_T (sz 10)) #t_SafeIndex =
let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
{
f_Output = v_T;
f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
Expand All @@ -79,7 +79,7 @@ open FStar.Mul
type t_Foo = | Foo : u8 -> t_Foo

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl: Core.Ops.Arith.t_Add #t_Foo #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 <. (255uy -! rhs._0 <: u8));
Expand All @@ -88,7 +88,7 @@ let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo =
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_1: Core.Ops.Arith.t_Mul #t_Foo #t_Foo =
let impl_1: Core.Ops.Arith.t_Mul t_Foo t_Foo =
{
f_Output = t_Foo;
f_mul_pre
Expand Down Expand Up @@ -131,7 +131,7 @@ let mutation_example
(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 =
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);
Expand All @@ -145,7 +145,7 @@ module Attributes.Refinement_types
open Core
open FStar.Mul

let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX}
let t_BoundedU8 (#v_MIN #v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX}

/// Example of a specific constraint on a value
let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}
Expand All @@ -158,7 +158,7 @@ let t_Even = x: u8{(x %! 2uy <: u8) =. 0uy}
let t_FieldElement = x: u16{x <=. 2347us}

/// A modular mutliplicative inverse
let t_ModInverse (v_MOD: u32) =
let t_ModInverse (#v_MOD: u32) =
n:
u32
{ (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!
Expand Down
38 changes: 19 additions & 19 deletions test-harness/src/snapshots/toolchain__generics into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,38 +45,38 @@ module Generics
open Core
open FStar.Mul

let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
let impl__Bar__inherent_impl_generics (#v_T: Type0) (#v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
()

class t_Foo (#v_Self: Type0) = {
f_const_add_pre:v_N: usize -> v_Self -> bool;
f_const_add_post:v_N: usize -> v_Self -> usize -> bool;
f_const_add:v_N: usize -> x0: v_Self
-> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
class t_Foo (v_Self: Type0) = {
f_const_add_pre:#v_N: usize -> v_Self -> bool;
f_const_add_post:#v_N: usize -> v_Self -> usize -> bool;
f_const_add:#v_N: usize -> x0: v_Self
-> Prims.Pure usize (f_const_add_pre #v_N x0) (fun result -> f_const_add_post #v_N x0 result)
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_Foo_for_usize: t_Foo #usize =
let impl_Foo_for_usize: t_Foo usize =
{
f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
f_const_add_pre = (fun (#v_N: usize) (self: usize) -> true);
f_const_add_post = (fun (#v_N: usize) (self: usize) (out: usize) -> true);
f_const_add = fun (#v_N: usize) (self: usize) -> self +! v_N
}

let dup
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone #v_T)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
(x: v_T)
: (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T)

let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
let f (#v_N x: usize) : usize = (v_N +! v_N <: usize) +! x

let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3
let call_f (_: Prims.unit) : usize = (f #(sz 10) (sz 3) <: usize) +! sz 3

let g
(v_N: usize)
(#v_N: usize)
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into #v_T #(t_Array usize v_N))
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N))
(arr: v_T)
: usize =
(Core.Option.impl__unwrap_or #usize
Expand All @@ -93,7 +93,7 @@ let g
v_N

let call_g (_: Prims.unit) : usize =
(g (sz 3)
(g #(sz 3)
#(t_Array usize (sz 3))
(let list = [sz 42; sz 3; sz 49] in
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
Expand All @@ -102,7 +102,7 @@ let call_g (_: Prims.unit) : usize =
usize) +!
sz 3

let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
let foo (#v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
let acc:usize = v_LEN +! sz 9 in
let acc:usize =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
Expand All @@ -121,9 +121,9 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
acc

let repeat
(v_LEN: usize)
(#v_LEN: usize)
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy #v_T)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
(x: v_T)
: t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN

Expand Down
6 changes: 3 additions & 3 deletions test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ module Include_flag
open Core
open FStar.Mul

class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }

/// Indirect dependencies
let main_a_a (_: Prims.unit) : Prims.unit = ()
Expand All @@ -42,7 +42,7 @@ let main_a_b (_: Prims.unit) : Prims.unit = ()
let main_a_c (_: Prims.unit) : Prims.unit = ()

/// Direct dependencies
let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait #v_T) (x: v_T)
let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
: Prims.unit =
let _:Prims.unit = main_a_a () in
let _:Prims.unit = main_a_b () in
Expand Down Expand Up @@ -76,7 +76,7 @@ let main_c (_: Prims.unit) : Prims.unit =
type t_Foo = | Foo : t_Foo

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_Trait_for_Foo: t_Trait #t_Foo = { __marker_trait = () }
let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }

/// Entrypoint
let main (_: Prims.unit) : Prims.unit =
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ type t_Bar = | Bar : t_Bar
/// dropped. This might be a bit surprising: see
/// https://github.com/hacspec/hax/issues/616.
[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl: Core.Convert.t_From #t_Bar #Prims.unit =
let impl: Core.Convert.t_From t_Bar Prims.unit =
{
f_from_pre = (fun ((): Prims.unit) -> true);
f_from_post = (fun ((): Prims.unit) (out: t_Bar) -> true);
Expand All @@ -65,7 +65,7 @@ val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)

/// If you need to drop the body of a method, please hoist it:
[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_1: Core.Convert.t_From #t_Bar #u8 =
let impl_1: Core.Convert.t_From t_Bar u8 =
{
f_from_pre = (fun (x: u8) -> true);
f_from_post = (fun (x: u8) (out: t_Bar) -> true);
Expand Down
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__loops into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ open FStar.Mul

let bool_returning (x: u8) : bool = x <. 10uy

let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let chunks (#v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
let acc:usize = sz 0 in
let chunks:Core.Slice.Iter.t_ChunksExact usize =
Core.Slice.impl__chunks_exact #usize
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ module Mut_ref_functionalization
open Core
open FStar.Mul

class t_FooTrait (#v_Self: Type0) = {
class t_FooTrait (v_Self: Type0) = {
f_z_pre:v_Self -> bool;
f_z_post:v_Self -> v_Self -> bool;
f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
Expand Down Expand Up @@ -173,7 +173,7 @@ type t_Bar = {
type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_FooTrait_for_Foo: t_FooTrait #t_Foo =
let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
{
f_z_pre = (fun (self: t_Foo) -> true);
f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);
Expand Down
18 changes: 9 additions & 9 deletions test-harness/src/snapshots/toolchain__naming into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,28 +108,28 @@ type t_Foo2 =
| Foo2_A : t_Foo2
| Foo2_B { f_x:usize }: t_Foo2

class t_FooTrait (#v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }

class t_T1 (#v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T1_for_Foo: t_T1 #t_Foo = { __marker_trait = () }
let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T1_for_tuple_Foo_u8: t_T1 #(t_Foo & u8) = { __marker_trait = () }
let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }

class t_T2_for_a (#v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }

class t_T3_e_for_a (#v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a #t_Foo = { __marker_trait = () }
let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }

let v_INHERENT_CONSTANT: usize = sz 3

let constants
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait #v_T)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
(_: Prims.unit)
: usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT

Expand All @@ -146,7 +146,7 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o
type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a #(t_Arity1 (t_Foo & u8)) =
let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
{ __marker_trait = () }

type t_B = | B : t_B
Expand Down
Loading

0 comments on commit 35145cc

Please sign in to comment.