Skip to content

Commit

Permalink
Merge pull request #1140 from hacspec/fix-item-order-771
Browse files Browse the repository at this point in the history 
fix(engine): item ordering
  • Loading branch information
@maximebuyse
maximebuyse authored Nov 27, 2024
2 parents 01e7ecd + 40ba45e commit 7bb4c28
Show file tree
Hide file tree
Showing 30 changed files with 2,166 additions and 1,796 deletions.
953 changes: 514 additions & 439 deletions engine/lib/dependencies.ml
View file

Large diffs are not rendered by default.

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 @@ -35,7 +35,7 @@ module Attribute_opaque
open Core
open FStar.Mul

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_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
'''
140 changes: 70 additions & 70 deletions test-harness/src/snapshots/toolchain__attributes into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,15 +92,15 @@ 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
}

unfold let add x y = x + y
'''
"Attributes.Nested_refinement_elim.fst" = '''
module Attributes.Nested_refinement_elim
Expand All @@ -118,11 +118,16 @@ module Attributes.Newtype_pattern
open Core
open FStar.Mul

let v_MAX: usize = sz 10

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

let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
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 v_MAX: usize = sz 10
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 (sz 10)) t_SafeIndex =
Expand All @@ -132,11 +137,6 @@ let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIn
f_index_post = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) (out: v_T) -> true);
f_index = fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
}

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
'''
"Attributes.Pre_post_on_traits_and_impls.fst" = '''
module Attributes.Pre_post_on_traits_and_impls
Expand All @@ -162,13 +162,6 @@ class t_Operation (v_Self: Type0) = {
f_double:x0: u8 -> Prims.Pure u8 (f_double_pre x0) (fun result -> f_double_post x0 result)
}

class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
f_method:x0: v_Self -> x1: u8
-> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
}

type t_ViaAdd = | ViaAdd : t_ViaAdd

type t_ViaMul = | ViaMul : t_ViaMul
Expand Down Expand Up @@ -207,6 +200,13 @@ let impl_1: t_Operation t_ViaMul =
f_double = fun (x: u8) -> x *! 2uy
}

class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
f_method:x0: v_Self -> x1: u8
-> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
}

let test
(#v_T: Type0)
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
Expand Down Expand Up @@ -247,10 +247,10 @@ module Attributes.Refined_indexes
open Core
open FStar.Mul

type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray

let v_MAX: usize = sz 10

type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray

/// Triple dash comment
(** Multiline double star comment Maecenas blandit accumsan feugiat.
Done vitae ullamcorper est.
Expand Down Expand Up @@ -288,27 +288,20 @@ module Attributes.Refinement_types
open Core
open FStar.Mul

/// Example of a specific constraint on a value
let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}

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

/// A field element
let t_FieldElement = x: u16{x <=. 2347us}
let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
(x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy

/// Even `u8` numbers. Constructing pub Even values triggers static
/// proofs in the extraction.
let t_Even = x: u8{(x %! 2uy <: u8) =. 0uy}

/// A modular mutliplicative inverse
let t_ModInverse (v_MOD: u32) =
n:
u32
{ (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!
(cast (v_MOD <: u32) <: u128)
<:
u128) =.
pub_u128 1 }
let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
x +! x <: t_Even

let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
x +! x <: t_Even

/// A string that contains no space.
let t_NoE =
Expand All @@ -330,14 +323,21 @@ let t_NoE =
in
~.out }

let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
x +! x <: t_Even
/// A modular mutliplicative inverse
let t_ModInverse (v_MOD: u32) =
n:
u32
{ (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!
(cast (v_MOD <: u32) <: u128)
<:
u128) =.
pub_u128 1 }

let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
(x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy
/// A field element
let t_FieldElement = x: u16{x <=. 2347us}

let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
x +! x <: t_Even
/// Example of a specific constraint on a value
let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}
'''
"Attributes.Requires_mut.fst" = '''
module Attributes.Requires_mut
Expand Down Expand Up @@ -417,6 +417,12 @@ module Attributes.Verifcation_status
open Core
open FStar.Mul

#push-options "--admit_smt_queries true"

let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false

#pop-options

let a_panicfree_function (_: Prims.unit)
: Prims.Pure u8
Prims.l_True
Expand All @@ -441,36 +447,27 @@ let another_panicfree_function (_: Prims.unit)
let nothing:i32 = 0l in
let still_not_much:i32 = not_much +! nothing in
admit () (* Panic freedom *)

#push-options "--admit_smt_queries true"

let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false

#pop-options
'''
"Attributes.fst" = '''
module Attributes
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

type t_Foo = {
f_x:u32;
f_y:f_y: u32{f_y >. 3ul};
f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
}

let inlined_code__V: u8 = 12uy
let u32_max: u32 = 90000ul

let issue_844_ (v__x: u8)
: Prims.Pure u8
Prims.l_True
/// A doc comment on `add3`
///another doc comment on add3
let add3 (x y z: u32)
: Prims.Pure u32
(requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
(ensures
fun v__x_future ->
let v__x_future:u8 = v__x_future in
true) = v__x

let u32_max: u32 = 90000ul
fun result ->
let result:u32 = result in
Hax_lib.implies true
(fun temp_0_ ->
let _:Prims.unit = temp_0_ in
result >. 32ul <: bool)) = (x +! y <: u32) +! z

let swap_and_mut_req_ens (x y: u32)
: Prims.Pure (u32 & u32 & u32)
Expand All @@ -485,25 +482,28 @@ 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)

/// A doc comment on `add3`
///another doc comment on add3
let add3 (x y z: u32)
: Prims.Pure u32
(requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
let issue_844_ (v__x: u8)
: Prims.Pure u8
Prims.l_True
(ensures
fun result ->
let result:u32 = result in
Hax_lib.implies true
(fun temp_0_ ->
let _:Prims.unit = temp_0_ in
result >. 32ul <: bool)) = (x +! y <: u32) +! z
fun v__x_future ->
let v__x_future:u8 = v__x_future in
true) = v__x

let add3_lemma (x: u32)
: Lemma Prims.l_True
(ensures
x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
()

type t_Foo = {
f_x:u32;
f_y:f_y: u32{f_y >. 3ul};
f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
}

let inlined_code__V: u8 = 12uy

let before_inlined_code = "example before"

let inlined_code (foo: t_Foo) : Prims.unit =
Expand Down
8 changes: 4 additions & 4 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 @@ -32,15 +32,15 @@ module Constructor_as_closure
open Core
open FStar.Mul

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

type t_Test = | Test : i32 -> 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 =
Core.Option.impl__map #i32 #t_Context x Context_B
'''
Loading

0 comments on commit 7bb4c28

Please sign in to comment.