diff --git a/kremlib/dist/generic/FStar_Pervasives.h b/kremlib/dist/generic/FStar_Pervasives.h index 6a248c2db..3d00db5d3 100644 --- a/kremlib/dist/generic/FStar_Pervasives.h +++ b/kremlib/dist/generic/FStar_Pervasives.h @@ -31,6 +31,7 @@ typedef void *FStar_Pervasives_pattern; #define FStar_Pervasives_UnfoldFully 11 #define FStar_Pervasives_UnfoldAttr 12 #define FStar_Pervasives_UnfoldQual 13 +#define FStar_Pervasives_Unmeta 14 typedef uint8_t FStar_Pervasives_norm_step_tags; @@ -87,6 +88,8 @@ extern bool FStar_Pervasives_uu___is_UnfoldQual(FStar_Pervasives_norm_step proje extern Prims_list__Prims_string *FStar_Pervasives___proj__UnfoldQual__item___0(FStar_Pervasives_norm_step projectee); +extern bool FStar_Pervasives_uu___is_Unmeta(FStar_Pervasives_norm_step projectee); + extern FStar_Pervasives_norm_step FStar_Pervasives_simplify; extern FStar_Pervasives_norm_step FStar_Pervasives_weak; @@ -116,6 +119,8 @@ extern FStar_Pervasives_norm_step FStar_Pervasives_delta_attr(Prims_list__Prims_ extern FStar_Pervasives_norm_step FStar_Pervasives_delta_qualifier(Prims_list__Prims_string *s); +extern FStar_Pervasives_norm_step FStar_Pervasives_unmeta; + typedef struct Prims_list__FStar_Pervasives_norm_step_s Prims_list__FStar_Pervasives_norm_step; typedef struct Prims_list__FStar_Pervasives_norm_step_s diff --git a/kremlib/dist/generic/FStar_UInt_8_16_32_64.h b/kremlib/dist/generic/FStar_UInt_8_16_32_64.h index ee3758454..f234776f4 100644 --- a/kremlib/dist/generic/FStar_UInt_8_16_32_64.h +++ b/kremlib/dist/generic/FStar_UInt_8_16_32_64.h @@ -14,6 +14,8 @@ +extern Prims_int FStar_UInt64_n; + extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee); extern Prims_int FStar_UInt64___proj__Mk__item__v(uint64_t projectee); @@ -22,6 +24,14 @@ extern Prims_int FStar_UInt64_v(uint64_t x); extern uint64_t FStar_UInt64_uint_to_t(Prims_int x); +extern uint64_t FStar_UInt64_zero; + +extern uint64_t FStar_UInt64_one; + +extern uint64_t FStar_UInt64_minus(uint64_t a); + +extern uint32_t FStar_UInt64_n_minus_one; + static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b) { uint64_t x = a ^ b; diff --git a/kremlib/dist/generic/Makefile.include b/kremlib/dist/generic/Makefile.include index 0cbe189b0..a8c67532d 100644 --- a/kremlib/dist/generic/Makefile.include +++ b/kremlib/dist/generic/Makefile.include @@ -1,5 +1,5 @@ USER_TARGET=libkremlib.a USER_CFLAGS= USER_C_FILES=testlib.c prims.c lowstar_printf.c fstar_uint8.c fstar_uint64.c fstar_uint32.c fstar_uint16.c fstar_string.c fstar_io.c fstar_int8.c fstar_int64.c fstar_int32.c fstar_int16.c fstar_hyperstack_io.c fstar_dyn.c fstar_date.c fstar_char.c fstar_bytes.c c_string.c c.c -ALL_C_FILES=WasmSupport.c FStar_ModifiesGen.c FStar_VConfig.c FStar_Order.c -ALL_H_FILES=Prims.h FStar_BitVector.h FStar_UInt.h FStar_UInt_8_16_32_64.h FStar_UInt128.h LowStar_Endianness.h C_Failure.h FStar_String.h LowStar_Printf.h FStar_HyperStack_IO.h TestLib.h C_String.h C.h FStar_Bytes.h FStar_Char.h FStar_IO.h FStar_Float.h FStar_Monotonic_HyperStack.h C_Loops.h WasmSupport.h FStar_Int_Cast.h FStar_Int.h FStar_Int8.h FStar_Int32.h FStar_Int64.h FStar_All.h FStar_Monotonic_Heap.h FStar_ST.h FStar_Kremlin_Endianness.h FStar_ModifiesGen.h FStar_VConfig.h FStar_Order.h FStar_Date.h FStar_HyperStack_All.h FStar_HyperStack_ST.h FStar_Monotonic_HyperHeap.h FStar_Int16.h FStar_Math_Lib.h FStar_Mul.h FStar_Pervasives.h +ALL_C_FILES=WasmSupport.c FStar_ModifiesGen.c FStar_Order.c FStar_VConfig.c +ALL_H_FILES=Prims.h FStar_BitVector.h FStar_UInt.h FStar_UInt_8_16_32_64.h FStar_UInt128.h LowStar_Endianness.h C_Failure.h FStar_String.h LowStar_Printf.h FStar_HyperStack_IO.h TestLib.h C_String.h C.h FStar_Bytes.h FStar_Char.h FStar_IO.h FStar_Float.h FStar_Monotonic_HyperStack.h C_Loops.h WasmSupport.h FStar_Int_Cast.h FStar_Int.h FStar_Int8.h FStar_Int32.h FStar_Int64.h FStar_All.h FStar_Monotonic_Heap.h FStar_ST.h FStar_Kremlin_Endianness.h FStar_ModifiesGen.h FStar_Order.h FStar_Date.h FStar_HyperStack_All.h FStar_HyperStack_ST.h FStar_Monotonic_HyperHeap.h FStar_VConfig.h FStar_Int16.h FStar_Math_Lib.h FStar_Mul.h FStar_Pervasives.h diff --git a/kremlib/dist/generic/libkremlib.def b/kremlib/dist/generic/libkremlib.def index 924b1a815..7202deec1 100644 --- a/kremlib/dist/generic/libkremlib.def +++ b/kremlib/dist/generic/libkremlib.def @@ -14,6 +14,19 @@ EXPORTS WasmSupport_betole32 WasmSupport_betole64 WasmSupport_memzero + FStar_Order_uu___is_Lt + FStar_Order_uu___is_Eq + FStar_Order_uu___is_Gt + FStar_Order_ge + FStar_Order_le + FStar_Order_ne + FStar_Order_gt + FStar_Order_lt + FStar_Order_eq + FStar_Order_lex + FStar_Order_order_from_int + FStar_Order_int_of_order + FStar_Order_compare_int FStar_VConfig___proj__Mkvconfig__item__initial_fuel FStar_VConfig___proj__Mkvconfig__item__max_fuel FStar_VConfig___proj__Mkvconfig__item__initial_ifuel @@ -41,16 +54,3 @@ EXPORTS FStar_VConfig___proj__Mkvconfig__item__z3seed FStar_VConfig___proj__Mkvconfig__item__trivial_pre_for_unannotated_effectful_fns FStar_VConfig___proj__Mkvconfig__item__reuse_hint_for - FStar_Order_uu___is_Lt - FStar_Order_uu___is_Eq - FStar_Order_uu___is_Gt - FStar_Order_ge - FStar_Order_le - FStar_Order_ne - FStar_Order_gt - FStar_Order_lt - FStar_Order_eq - FStar_Order_lex - FStar_Order_order_from_int - FStar_Order_int_of_order - FStar_Order_compare_int diff --git a/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h b/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h index 7f220ef41..2f016b540 100644 --- a/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h +++ b/kremlib/dist/minimal/FStar_UInt_8_16_32_64.h @@ -16,7 +16,7 @@ -extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee); +extern Prims_int FStar_UInt64_n; extern Prims_int FStar_UInt64___proj__Mk__item__v(uint64_t projectee); @@ -24,6 +24,14 @@ extern Prims_int FStar_UInt64_v(uint64_t x); extern uint64_t FStar_UInt64_uint_to_t(Prims_int x); +extern uint64_t FStar_UInt64_zero; + +extern uint64_t FStar_UInt64_one; + +extern uint64_t FStar_UInt64_minus(uint64_t a); + +extern uint32_t FStar_UInt64_n_minus_one; + static inline uint64_t FStar_UInt64_eq_mask(uint64_t a, uint64_t b) { uint64_t x = a ^ b; @@ -56,8 +64,6 @@ extern uint64_t FStar_UInt64_of_string(Prims_string uu___); extern Prims_int FStar_UInt32_n; -extern bool FStar_UInt32_uu___is_Mk(uint32_t projectee); - extern Prims_int FStar_UInt32___proj__Mk__item__v(uint32_t projectee); extern Prims_int FStar_UInt32_v(uint32_t x); @@ -104,8 +110,6 @@ extern uint32_t FStar_UInt32_of_string(Prims_string uu___); extern Prims_int FStar_UInt16_n; -extern bool FStar_UInt16_uu___is_Mk(uint16_t projectee); - extern Prims_int FStar_UInt16___proj__Mk__item__v(uint16_t projectee); extern Prims_int FStar_UInt16_v(uint16_t x); @@ -152,8 +156,6 @@ extern uint16_t FStar_UInt16_of_string(Prims_string uu___); extern Prims_int FStar_UInt8_n; -extern bool FStar_UInt8_uu___is_Mk(uint8_t projectee); - extern Prims_int FStar_UInt8___proj__Mk__item__v(uint8_t projectee); extern Prims_int FStar_UInt8_v(uint8_t x); diff --git a/src/DataTypes.ml b/src/DataTypes.ml index 85cebc804..caef57f28 100644 --- a/src/DataTypes.ml +++ b/src/DataTypes.ml @@ -35,10 +35,16 @@ let remove_unused_type_arguments files = let def_map = Helpers.build_map files (fun map d -> match d with - | DType (lid, _, n, d) -> Hashtbl.add map lid (n, d) + | DType (lid, _, n, d) -> + Hashtbl.add map lid (`Typ (n, d)) + | DFunction (_, _, n, t_ret, lid, bs, body) -> + let ts = List.map (fun b -> b.typ) bs in + Hashtbl.add map lid (`Fun (n, t_ret :: ts, body)) | _ -> () ) in + (* An ad-hoc reduce visitor over the bool monoid that simply returns true if + there is an occurrence of the i-th type parameter.*) let find_ith valuation = object(self) inherit [_] reduce method zero = false @@ -47,7 +53,8 @@ let remove_unused_type_arguments files = method! visit_TBound (j, n) i = j = n - i - 1 - method! visit_TApp env lid args = + + method private visit_app env lid args = let args = List.mapi (fun i arg -> if valuation (lid, i) then self#visit_typ env arg @@ -55,12 +62,26 @@ let remove_unused_type_arguments files = self#zero ) args in List.fold_left self#plus self#zero args + + method! visit_TApp env lid args = + self#visit_app env lid args + + method! visit_ETApp env e args = + let lid = assert_elid e.node in + self#visit_app (fst env) lid args end in let equations (lid, i) valuation = try - let n, def = Hashtbl.find def_map lid in - (find_ith valuation)#visit_type_def (i, n) def + match Hashtbl.find def_map lid with + | `Typ (n, def) -> + (find_ith valuation)#visit_type_def (i, n) def + | `Fun (n, ts, def) -> + (* This is an approximation because this LFP is not mutually + recursive with private-functions unused argument elimination. *) + List.fold_left (||) false + ((find_ith valuation)#visit_expr_w (i, n) def :: + List.map ((find_ith valuation)#visit_typ (i, n)) ts) with Not_found -> true in @@ -79,10 +100,10 @@ let remove_unused_type_arguments files = if i = n then kept, def else - if uses_nth lid (n - i - 1) then + if uses_nth lid i then chop (kept + 1) (i + 1) def else - let def = (new DeBruijn.subst_t TAny)#visit_type_def i def in + let def = (new DeBruijn.subst_t TAny)#visit_type_def (n - i - 1) def in chop kept (i + 1) def in let n, def = chop 0 0 def in @@ -101,6 +122,39 @@ let remove_unused_type_arguments files = TApp (lid, args) else TQualified lid + + method! visit_DFunction env cc flags n ret lid binders def = + let binders = self#visit_binders_w env binders in + let ret = self#visit_typ env ret in + let def = self#visit_expr_w env def in + let rec chop kept i (def, binders, ret) = + if i = n then + kept, (def, binders, ret) + else + if uses_nth lid i then + chop (kept + 1) (i + 1) (def, binders, ret) + else + let def = DeBruijn.subst_te TAny (n - i - 1) def in + let binders = List.map (fun { node; typ } -> { node; typ = DeBruijn.subst_t TAny (n - i - 1) typ }) binders in + let ret = DeBruijn.subst_t TAny (n - i - 1) ret in + chop kept (i + 1) (def, binders, ret) + in + let n, (def, binders, ret) = chop 0 0 (def, binders, ret) in + DFunction (cc, flags, n, ret, lid, binders, def) + + method! visit_ETApp env e args = + let lid = assert_elid e.node in + let args = List.map (self#visit_typ_wo env) args in + let args = KList.filter_mapi (fun i arg -> + if uses_nth lid i then + Some arg + else + None + ) args in + if List.length args > 0 then + ETApp (e, args) + else + e.node end in NamingHints.hints := List.map (fun ((head, args), hint) -> diff --git a/src/InputAst.ml b/src/InputAst.ml index f49b0ade3..3359ce532 100644 --- a/src/InputAst.ml +++ b/src/InputAst.ml @@ -40,6 +40,7 @@ and decl = * for it. *) | DExternal2 of (calling_convention option * flag list * lident * typ * string list) (** New variant that keeps names of arguments *) + | DUntaggedUnion of (lident * flag list * int * (ident * typ) list) and fields_t = (ident * (typ * bool)) list @@ -101,6 +102,7 @@ and expr = | EAbortT of (string * typ) | EComment of (string * expr * string) | EStandaloneComment of string + | EAddrOf of expr and branches = branch list @@ -145,6 +147,8 @@ and typ = | TApp of (lident * typ list) | TTuple of typ list | TConstBuf of typ + | TArray of (typ * K.t) + (** For flat arrays within structs. *) let flatten_arrow = let rec flatten_arrow acc = function diff --git a/src/InputAstToAst.ml b/src/InputAstToAst.ml index f2dde4ace..c3e241aee 100644 --- a/src/InputAstToAst.ml +++ b/src/InputAstToAst.ml @@ -56,6 +56,8 @@ let rec mk_decl = function Variant (List.map (fun (ident, fields) -> ident, mk_tfields fields) branches)) | I.DTypeAbstractStruct name -> DType (name, [], 0, Forward) + | I.DUntaggedUnion (name, flags, n, branches) -> + DType (name, flags, n, Union (List.map (fun (f, t) -> f, mk_typ t) branches)) and mk_binders bs = List.map mk_binder bs @@ -95,6 +97,8 @@ and mk_typ = function TApp (lid, List.map mk_typ ts) | I.TTuple ts -> TTuple (List.map mk_typ ts) + | I.TArray (t, c) -> + TArray (mk_typ t, c) and mk_expr = function | I.EBound i -> @@ -179,6 +183,8 @@ and mk_expr = function mk (EComment (before, mk_expr e, after)) | I.EStandaloneComment s -> mk (EStandaloneComment s) + | I.EAddrOf e -> + mk (EAddrOf (mk_expr e)) and mk_branches branches = List.map mk_branch branches diff --git a/test/.hints/Abbrev.fst.hints b/test/.hints/Abbrev.fst.hints index 762ee7318..a639b9b4e 100644 --- a/test/.hints/Abbrev.fst.hints +++ b/test/.hints/Abbrev.fst.hints @@ -34,7 +34,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "714ca644b1ebc41434a6a2cd1cb5b4d0" + "55c0d93592bff3bbfd2e2899dbe6721d" ] ] ] \ No newline at end of file diff --git a/test/.hints/AbstractStruct.fst.hints b/test/.hints/AbstractStruct.fst.hints index 94b54b2de..8cc7b72be 100755 --- a/test/.hints/AbstractStruct.fst.hints +++ b/test/.hints/AbstractStruct.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "1e94cffdb97e48cd1163f405409dd1b9" + "e21bd435bfbcd6964193419d39b1b912" ], [ "AbstractStruct.main", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "649fe6a316a206805f2b116ccb2d3867" + "c32feaedc13fb3d9607ae251f07c7eb9" ] ] ] \ No newline at end of file diff --git a/test/.hints/Attributes.fst.hints b/test/.hints/Attributes.fst.hints index a47213b1e..1e832977f 100644 --- a/test/.hints/Attributes.fst.hints +++ b/test/.hints/Attributes.fst.hints @@ -45,7 +45,7 @@ "typing_FStar.Set.union" ], 0, - "d4a840bd23c4314eac7d9cabc4453215" + "e999f3b0e67c862d6f625599b69e558b" ] ] ] \ No newline at end of file diff --git a/test/.hints/BadMatch.fst.hints b/test/.hints/BadMatch.fst.hints index 2d80f7eec..eba436b54 100644 --- a/test/.hints/BadMatch.fst.hints +++ b/test/.hints/BadMatch.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "438af333b717c6ad9185af04fe4a10a5" + "d5e8ea729deaa29e21ed7ac83bb16c13" ], [ "BadMatch.baz", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_BadMatch.bar__uu___haseq" ], 0, - "ae1240d1afce0445c9642b9ab4661e2d" + "bbeefe3fc7e472763dbb62f0f2bfdcbc" ] ] ] \ No newline at end of file diff --git a/test/.hints/BlitNull.fst.hints b/test/.hints/BlitNull.fst.hints index 2a4f9ae5d..c8f676692 100644 --- a/test/.hints/BlitNull.fst.hints +++ b/test/.hints/BlitNull.fst.hints @@ -58,7 +58,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "5efec399c193be821c9a94d2e791db41" + "7b709c1e508af81d6284c564b4a34ca6" ] ] ] \ No newline at end of file diff --git a/test/.hints/Buffer.Utils.fst.hints b/test/.hints/Buffer.Utils.fst.hints index f8552e9a0..632078076 100644 --- a/test/.hints/Buffer.Utils.fst.hints +++ b/test/.hints/Buffer.Utils.fst.hints @@ -22,7 +22,7 @@ "typing_FStar.UInt32.v" ], 0, - "70f92bcb43631495802cf032a959dde2" + "63c4d995032fc1ab4505dd29f4171385" ], [ "Buffer.Utils.uint32_of_bytes", @@ -34,7 +34,7 @@ "refinement_interpretation_Tm_refine_307c3f8471f15f30d8324ebc79cdcdfb" ], 0, - "c40440fe3fffab5e4ad6ede3082e66f4" + "a8049d63a1a938b623fbeba6170716a1" ], [ "Buffer.Utils.uint32_of_bytes", @@ -89,7 +89,7 @@ "typing_FStar.UInt8.v" ], 0, - "4a6b412ba39ebfe86833df603513b722" + "dd6f7a8dac7446f72caee30cafcc2ac6" ], [ "Buffer.Utils.bytes_of_uint32s", @@ -178,7 +178,7 @@ "unit_inversion", "unit_typing" ], 0, - "5a1c1d31bda6b673e06b73b6ca8afe26" + "dbf4198e18e45f5e7c84f51462abc302" ], [ "Buffer.Utils.bytes_of_uint32", @@ -199,7 +199,7 @@ "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, - "df4b38769110f5d73d7c62e994a5117e" + "b640e5ceb6f144e8903c5e459c805365" ], [ "Buffer.Utils.bytes_of_uint32", @@ -270,7 +270,7 @@ "typing_FStar.UInt32.v", "typing_FStar.UInt8.t" ], 0, - "0a30da6915c0f234647e996be9588ccc" + "a430404e142490a4db05dcd9dddcaae9" ], [ "Buffer.Utils.memset", @@ -285,7 +285,7 @@ "typing_FStar.UInt32.v" ], 0, - "37eb59280e2f56c53a2ef73b6dbb8697" + "8aba94cc5153db4b879dda8465394334" ], [ "Buffer.Utils.memset", @@ -369,7 +369,7 @@ "unit_typing" ], 0, - "d202180ac8f88f2f7580c9e5d81f6dc7" + "018653c8380c9139e80ae9784fb15da6" ] ] ] \ No newline at end of file diff --git a/test/.hints/C.Nullity.fsti.hints b/test/.hints/C.Nullity.fsti.hints index 55c7da31a..0bedef521 100644 --- a/test/.hints/C.Nullity.fsti.hints +++ b/test/.hints/C.Nullity.fsti.hints @@ -14,7 +14,7 @@ "refinement_interpretation_Tm_refine_0d4da60cb6187749d65a25df63d2ab15" ], 0, - "6c77e707671b95dddbb1bf251785c291" + "79a7e52395366241fbd92ee6c58cd6bb" ], [ "C.Nullity.pointer_distinct_sel_disjoint", @@ -80,7 +80,7 @@ "typing_FStar.UInt32.v" ], 0, - "8cb56d73b407fe94858d9624fdc75c35" + "e2d8c9049b299ab628629d5b9d0912aa" ] ] ] \ No newline at end of file diff --git a/test/.hints/C89.fst.hints b/test/.hints/C89.fst.hints index 425e48c13..526600de9 100644 --- a/test/.hints/C89.fst.hints +++ b/test/.hints/C89.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "835fdce63f833ddf0eb8b50b3e0447f3" + "7f10e21a2e846c9b5f0412c9e35ae4f2" ], [ "C89.g", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "1553cecd58214030db25121ce7f60f92" + "8d50a26d9c9882008597005668c4cbcc" ], [ "C89.h", @@ -62,7 +62,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "2b695a6589fae6c5e25b61daa56d2dc2" + "1b4e5e7347f3df04d0c21c59c707520a" ], [ "C89.i", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d19f833d3326633aabf9b60a1977b8db" + "68391752d39c14921c507b320b80e30f" ], [ "C89.touch", @@ -104,7 +104,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d8a5a4d9d4942f0f35b7c36be1d24186" + "be6bbd552238be33e7e8e8e2ddbf8493" ], [ "C89.t", @@ -117,7 +117,7 @@ "typing_FStar.Int32.t", "typing_FStar.Int64.t" ], 0, - "2856fd7584a31774e2a1de14722ca044" + "20fc82d22f1fb66b221eefe6797ac818" ], [ "C89.__proj__A__item___0", @@ -130,7 +130,7 @@ "refinement_interpretation_Tm_refine_dfc04c5c79d942a90086cac1eb7b1ae6" ], 0, - "997251b05e8081f1eec8eb1ce40cc626" + "2c66214aae206e82174294a90fe16621" ], [ "C89.__proj__B__item___0", @@ -143,7 +143,7 @@ "refinement_interpretation_Tm_refine_1a06de69b44dc8c0429a5d7e27c9f480" ], 0, - "b0552f83c87ce95d2f9acac6141119c6" + "3711fb7f1f3478d32f4287f19b1263dc" ], [ "C89.point", @@ -156,7 +156,7 @@ "typing_FStar.Int32.t" ], 0, - "a17e913a33f9a2940b572c2f30f1ce56" + "01549359b34b19ac4bca6ad8e5cf3395" ], [ "C89.__proj__Point2d__item___0", @@ -169,7 +169,7 @@ "refinement_interpretation_Tm_refine_17ea200a8473bdb82b8d303711705436" ], 0, - "5585ee70ed6dd212d024d80678a440f7" + "f3cfbfbd88f797f8517a38137e8d3d0d" ], [ "C89.__proj__Point2d__item___1", @@ -182,7 +182,7 @@ "refinement_interpretation_Tm_refine_17ea200a8473bdb82b8d303711705436" ], 0, - "aae8f5ba857887ff92d06b5e2f982cbe" + "220cd80ab9ace34c76c249fccdc12e99" ], [ "C89.__proj__Point3d__item___0", @@ -195,7 +195,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "676e7ff3d17344b029ba6159d84ac015" + "d02e2cd444c67651318dcbb4edf74b5a" ], [ "C89.__proj__Point3d__item___1", @@ -208,7 +208,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "9f072860f22f167d37dce0735d61f9c5" + "a7fe96e27caa660ab1abc448e52a8b17" ], [ "C89.__proj__Point3d__item___2", @@ -221,7 +221,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "603d564728677ac5187204bfeb51984c" + "1f576e00f95713b6d650395ab23adfc2" ], [ "C89.main", @@ -321,7 +321,7 @@ "typing_FStar.UInt32.t", "typing_Prims.pow2" ], 0, - "b779c9a55fabaf2ce1cfa8ef243cf306" + "cf28e9fbee8c25984bbf97706b8a6dff" ] ] ] \ No newline at end of file diff --git a/test/.hints/CheckedInt.fst.hints b/test/.hints/CheckedInt.fst.hints index fb907d9a5..aec053627 100644 --- a/test/.hints/CheckedInt.fst.hints +++ b/test/.hints/CheckedInt.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "f8f98bbacc380b7dfcd225ef44bbb649" + "b49c76e006f4181ec80db3af8f2c6d46" ], [ "CheckedInt.two", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "fcefcf514779cee7548667a76cfe560f" + "5614826e92937d05fe1d3e611f39627f" ], [ "CheckedInt.main", @@ -54,7 +54,7 @@ "primitive_Prims.op_Subtraction" ], 0, - "634f5b7098fa05fb39f1df457d2dd052" + "83b4b8301c5ff6b118f457a2f24103ac" ] ] ] \ No newline at end of file diff --git a/test/.hints/ColoredRegion.fst.hints b/test/.hints/ColoredRegion.fst.hints index 0c03e30fb..9dad507e2 100644 --- a/test/.hints/ColoredRegion.fst.hints +++ b/test/.hints/ColoredRegion.fst.hints @@ -44,7 +44,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "bedc004da61754473b5ef537e1171f55" + "fee93e82b4a0154d40bdfb1eb2743d55" ] ] ] \ No newline at end of file diff --git a/test/.hints/Comment.fst.hints b/test/.hints/Comment.fst.hints index b08cf82c7..54ee729ac 100644 --- a/test/.hints/Comment.fst.hints +++ b/test/.hints/Comment.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "443759de28495cc236a4036ca01225f5" + "a7d7ca27e5cacc03b9179250a6289894" ] ] ] \ No newline at end of file diff --git a/test/.hints/ConstBuffer.fst.hints b/test/.hints/ConstBuffer.fst.hints index d2dc573aa..ef0a797bc 100644 --- a/test/.hints/ConstBuffer.fst.hints +++ b/test/.hints/ConstBuffer.fst.hints @@ -31,7 +31,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "51348d559d06664fd419753626aa83d6" + "a0a232d8e79907b3c19e360021572a2b" ], [ "ConstBuffer.main", @@ -92,7 +92,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "666094c5e1bf0c661d46aa0ffa077fd2" + "e80cccbaa43084da0112fd172ff3b1aa" ] ] ] \ No newline at end of file diff --git a/test/.hints/Crypto.Symmetric.Chacha20.fst.hints b/test/.hints/Crypto.Symmetric.Chacha20.fst.hints index 2bd8f57e7..4bbdb42ee 100644 --- a/test/.hints/Crypto.Symmetric.Chacha20.fst.hints +++ b/test/.hints/Crypto.Symmetric.Chacha20.fst.hints @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, - "a98ef9c0861a7085b60eefb0e44e85af" + "f3548bc5e45e2004244a916eca4e69b9" ], [ "Crypto.Symmetric.Chacha20.counter_mode", @@ -128,7 +128,7 @@ "unit_typing" ], 0, - "c694a165954d2287107e1b2399ff31ad" + "0f3bba94f42e8a27c78e1e95b9214541" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes1.fst.hints b/test/.hints/Ctypes1.fst.hints index 589309f94..15f2eea2f 100644 --- a/test/.hints/Ctypes1.fst.hints +++ b/test/.hints/Ctypes1.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "22555ecfd7fd950693cb1c1e5747510d" + "73e3525b31a3c5058c1a78c401d536e4" ], [ "Ctypes1.point_no_bind", @@ -25,7 +25,7 @@ "typing_FStar.UInt32.t" ], 0, - "5acb5e0e77a6765017ad67b74732a777" + "344fa013fb8085b51deccaab62a31014" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes2.fst.hints b/test/.hints/Ctypes2.fst.hints index 0506a4b15..b8e13656a 100644 --- a/test/.hints/Ctypes2.fst.hints +++ b/test/.hints/Ctypes2.fst.hints @@ -24,7 +24,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "758656feb0078145ef9396738f019b3a" + "36e14ef7e964799a722203157182bd97" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes3.fst.hints b/test/.hints/Ctypes3.fst.hints index 5a789077f..a20884d20 100644 --- a/test/.hints/Ctypes3.fst.hints +++ b/test/.hints/Ctypes3.fst.hints @@ -13,7 +13,7 @@ "typing_FStar.UInt32.t" ], 0, - "c2cdb6155d0a117d3f8b36c950d3a3ed" + "d90f9d68854de8bee6b0f0cb247e065e" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes4.fst.hints b/test/.hints/Ctypes4.fst.hints index f682d1022..db53ab2e9 100644 --- a/test/.hints/Ctypes4.fst.hints +++ b/test/.hints/Ctypes4.fst.hints @@ -24,7 +24,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "35a9786486ba9c137465fea5c8076976" + "736562d71f5a40fd98640d4f800ae5b1" ], [ "Ctypes4.move_circle", @@ -37,7 +37,7 @@ "typing_Ctypes3.__proj__Mkcircle__item__r" ], 0, - "bdf84c681252cc2143130eba6dfc3c38" + "728a273a2854fe6171c27d29d1d3f4f1" ], [ "Ctypes4.my_not", @@ -62,7 +62,7 @@ "true_interp" ], 0, - "3f7a4860cb584fd3ce7fec2813c6c73b" + "44f0f29dde096698f30584ea44ecbf15" ], [ "Ctypes4.tr", @@ -77,7 +77,7 @@ "typing_FStar.UInt32.t" ], 0, - "746f1cffd116284fd8f8bb1cbdd027d5" + "63652ebc20c0488ed20f6577406c6f3f" ], [ "Ctypes4.replicate", @@ -90,7 +90,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "ab8bf0dbaba4f3d99e4297ac1166b6b6" + "16346d53e119d253a9b6cc7efad26199" ], [ "Ctypes4.int_opt", @@ -103,7 +103,7 @@ "typing_FStar.UInt32.t" ], 0, - "cb721f852bf9787f2ee3e8c79cd29feb" + "9bc809e0ef5dea968fb7218b02f44cb3" ], [ "Ctypes4.__proj__IntSome__item___0", @@ -116,7 +116,7 @@ "refinement_interpretation_Tm_refine_747e8dbcdadc1011beb312d289ca27b1" ], 0, - "abf540eb561fd35f58135a6fc6d6e08c" + "0f545ba1f7d898364e6ffb34b41ec236" ], [ "Ctypes4.maybe_double", @@ -138,7 +138,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "4ca41f00e2dc662c11400ff13cab8b7b" + "d6b870b880e8dcc5bf49664921056822" ], [ "Ctypes4.maybe_double", @@ -174,7 +174,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "cc1102b999a45d95b63934a486bc5935" + "3ee01b78d42d35709bdcde22725578d0" ], [ "Ctypes4.__proj__L__item___0", @@ -187,7 +187,7 @@ "refinement_interpretation_Tm_refine_369514edfb0ad292ed962e8252b9565a" ], 0, - "d82845a34499ba41e58abfd0752bfa3b" + "2d4779a250599e41b5a35154d1207c59" ], [ "Ctypes4.__proj__R__item___0", @@ -200,7 +200,7 @@ "refinement_interpretation_Tm_refine_692b693643b05e0d1ba47aa0fabd554b" ], 0, - "9232d8ee3b6debc8fe83953a0486b777" + "600d68b47745d6b9d59d87dfd4aa5f41" ], [ "Ctypes4.make_L", @@ -213,7 +213,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "f29aea27b48fb0a0d072073bd55296dc" + "8454c86c1baa05507a0bfe5ba2681b37" ], [ "Ctypes4.make_R", @@ -226,7 +226,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "0f8af29dca6f1f9ec4b5aed24de32d22" + "d338e82e48cf41e2efe4e4b875b83687" ], [ "Ctypes4.flip_t", @@ -249,7 +249,7 @@ "true_interp" ], 0, - "928545d4670071eb17143a4dc8bd926b" + "a2e556da9cd79549f6b5fb1d1d90cd62" ], [ "Ctypes4.unsupported_t", @@ -262,7 +262,7 @@ "typing_FStar.UInt128.t", "typing_FStar.UInt32.t" ], 0, - "99be59f3dfc35eccdd56b90d3153e38f" + "671cc96087f8a4f2fac9dc3828919f52" ], [ "Ctypes4.unsupported_abstract_t", @@ -275,7 +275,7 @@ "typing_FStar.UInt128.t", "typing_FStar.UInt32.t" ], 0, - "394a4780d293ba9a6e64cbf8ae349192" + "63e7793d0035d45865b6fe10da43a1b6" ], [ "Ctypes4.create_u", @@ -308,7 +308,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "87834c186ead56945863eb3f3a1819e5" + "3871c02a3140ed001ee185b05a5748f2" ], [ "Ctypes4.read_u_a2", @@ -324,7 +324,7 @@ "typing_Ctypes4.__proj__Mkunsupported_abstract_t__item__a2" ], 0, - "820b1d6b69dab7ad948e7c004e63eed9" + "316105857c085156119b0f6348c3085c" ] ] ] \ No newline at end of file diff --git a/test/.hints/CustomEq.fst.hints b/test/.hints/CustomEq.fst.hints index 6c52c7d29..73c50675c 100644 --- a/test/.hints/CustomEq.fst.hints +++ b/test/.hints/CustomEq.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "4a68cad8e11539d676f44e9e55d73a7a" + "531395bf5c4396dd6d337a6b02a9016a" ], [ "CustomEq.t", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_CustomEq.point__uu___haseq" ], 0, - "9f1e7985abd926e10b34e978fc73d892" + "bbb8e99ce8fe137f8605944c4599140a" ], [ "CustomEq.__proj__A__item__p1", @@ -34,7 +34,7 @@ "refinement_interpretation_Tm_refine_b42bbc5acfd996b49e25c6ab17e83c41" ], 0, - "b61cf479ca08572a9027f05b490d8dd2" + "9af109c265d9b103467cef4f167be6d3" ], [ "CustomEq.__proj__A__item__p2", @@ -47,7 +47,7 @@ "refinement_interpretation_Tm_refine_b42bbc5acfd996b49e25c6ab17e83c41" ], 0, - "be6b729e18f0f7f715bf953972c166fa" + "02f281d82110fb777162f51408bfb632" ], [ "CustomEq.__proj__B__item___0", @@ -60,7 +60,7 @@ "refinement_interpretation_Tm_refine_499f060f30a6559751f4282e23af22de" ], 0, - "a58e292ade266db88aa4e9193f119602" + "63d7d430418702e1777cf92acc922ab2" ], [ "CustomEq.p1", @@ -81,7 +81,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "04d5d0ffe503916e996fc6f45a130146" + "32ce0a4f3db9a4c0a63a33bfa1c8da57" ], [ "CustomEq.f", @@ -102,7 +102,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "f5fbbfbc4ee44f02a0f3f8f341bfa5a8" + "ea5acc002e608abe4cbae601ddf5c122" ], [ "CustomEq.p2", @@ -128,7 +128,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "89eaa51f83f426772d5bcc28e094318c" + "705c290c17dda04850815d39f4269d65" ], [ "CustomEq.t1", @@ -143,7 +143,7 @@ "typing_FStar.Int64.t" ], 0, - "ff0fc83c4cb5f41bf48de833f4566aa3" + "f42986b95afa2f3dc88d5246ef53f1cd" ], [ "CustomEq.t2", @@ -164,7 +164,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "2d01dd3bc9f93018a3046824303b3010" + "7627711aad925d91f116430dfc23ca2f" ], [ "CustomEq.id", @@ -185,7 +185,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "a67eae000a24be1400fe6dc2351c273b" + "8846e262fb969e49e3db11b2b790b9e3" ], [ "CustomEq.main", @@ -205,7 +205,7 @@ "typing_FStar.Int64.t" ], 0, - "9fe5da177c4881567663a646f3b3186b" + "8a843372b741206e9285f5cb38e76fc0" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypes.fst.hints b/test/.hints/DataTypes.fst.hints index d581708ed..243b53c2e 100644 --- a/test/.hints/DataTypes.fst.hints +++ b/test/.hints/DataTypes.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_599cdc3d9160d7b695e8959f132bb409" ], 0, - "9a73c83ab8b9d680198497bb4de6ca16" + "7d4be40e76824ef69c0935dae9c1c630" ], [ "DataTypes.__proj__A__item__b", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_599cdc3d9160d7b695e8959f132bb409" ], 0, - "c26d3a69707d3709da7400e4d12436aa" + "a24ff2547a984fa16af22fc4da64b824" ], [ "DataTypes.__proj__B__item__c", @@ -38,7 +38,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "f84f54438af5b82eaab10cb1bb2070b3" + "7159a1fceba9a47f3adcc67c63a2b441" ], [ "DataTypes.__proj__B__item__d", @@ -51,7 +51,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "804bae06287d734286bb49da2eeba07a" + "036a139edcb4ec43a6f69234352a76fe" ], [ "DataTypes.__proj__B__item__e", @@ -64,7 +64,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "350e3d3f1463b60c8f629f43ff6a63b1" + "32f3a99f244da3ab9fc0a902cf3de56d" ], [ "DataTypes.__proj__C__item__f", @@ -77,7 +77,7 @@ "refinement_interpretation_Tm_refine_b63a9a8aecee956770bb1476545b326e" ], 0, - "f71b8d2f9bda64f6f46711780a7aa822" + "a78c88b99a4f68c0366c5ffacfbe6cd4" ], [ "DataTypes.__proj__C__item__g", @@ -90,7 +90,7 @@ "refinement_interpretation_Tm_refine_b63a9a8aecee956770bb1476545b326e" ], 0, - "e5c0a4b481be48487f73c080ca0da9fe" + "a925bb68289817ada0716d70f88dd07d" ], [ "DataTypes.__proj__D__item__h", @@ -103,7 +103,7 @@ "refinement_interpretation_Tm_refine_4c835444c923ef29c3c5e4f8248f0c1c" ], 0, - "0918db07c12289a796c20827c0a66014" + "43c8bb5fc6927f1a4ffc5967885baa84" ], [ "DataTypes.__proj__D__item__i", @@ -116,7 +116,7 @@ "refinement_interpretation_Tm_refine_4c835444c923ef29c3c5e4f8248f0c1c" ], 0, - "b8e9d499233aa324b4774b471750dfa4" + "3f4b79c5a3dd39394a64ca01fd01f67c" ], [ "DataTypes.test", @@ -138,7 +138,7 @@ "typing_tok_DataTypes.E@tok" ], 0, - "b4593ddb5c6188fb4951b0abb9276933" + "29e0180ca8fe853277192e9381c6abe0" ], [ "DataTypes.something", @@ -159,7 +159,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "9e42fb4469955b61cbf982195c974ce1" + "bd79fc67ab3246befdde4c21c9824cf8" ], [ "DataTypes.whatever", @@ -180,7 +180,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "ae51771954a3fd88b71865f5e8d66156" + "e1938884e61516d027e58cd77772f7db" ], [ "DataTypes.point", @@ -193,7 +193,7 @@ "typing_FStar.UInt32.t" ], 0, - "2e572c5beef4d38ab1cff28cae9f70e0" + "19be71aa6eda1aceb5fccf7101386384" ], [ "DataTypes.f", @@ -212,7 +212,7 @@ "true_interp" ], 0, - "11ab33d36415a78f9a42714d55261228" + "259456eb3a8096d005f5ad47005faf07" ], [ "DataTypes.f'", @@ -231,7 +231,7 @@ "true_interp" ], 0, - "60c819ba08e7332a8222d7d3a51df76d" + "e26d6a5b43a276f8cf4bd8f1e3a41115" ], [ "DataTypes.main", @@ -272,7 +272,7 @@ "typing_tok_C.EXIT_FAILURE@tok", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "29f5e57e2b8f126b6779cad2de9c4b9a" + "9af50130932e2800a49e46dc3628c547" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypesEq.fst.hints b/test/.hints/DataTypesEq.fst.hints index 517192a10..dd404c59c 100644 --- a/test/.hints/DataTypesEq.fst.hints +++ b/test/.hints/DataTypesEq.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "c0c7fbb7f4e402b0d66d19588a91562b" + "5fe2aef07e20e1170499d6404eae9c51" ], [ "DataTypesEq.__proj__A__item___0", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_7fe4ec39530be71d09622e6ea631b362" ], 0, - "99f3bbbc03d6f972c3326cc294a3c511" + "8ae76786d86b56945bddc45b35b312ec" ], [ "DataTypesEq.__proj__B__item___0", @@ -38,7 +38,7 @@ "refinement_interpretation_Tm_refine_4d5e6c06bbfb6471b81e2745aebd0ea5" ], 0, - "72e3baa4ee3284d6c83a37d24df1090a" + "83ce948d9b8dc36742fe4e40ff21e063" ], [ "DataTypesEq.f", @@ -59,7 +59,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "324115b504e0e3c15d3745c938a87b87" + "3f7917dde9345e82e2b1afb9cc8827ce" ], [ "DataTypesEq.main", @@ -68,7 +68,7 @@ 1, [ "@query", "assumption_DataTypesEq.t__uu___haseq" ], 0, - "8c5a311055433be42cae7665087f132f" + "343f469dc18b33099a4f2c9f2235730f" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypesSimple.fst.hints b/test/.hints/DataTypesSimple.fst.hints index b3d009e1e..9827abadf 100644 --- a/test/.hints/DataTypesSimple.fst.hints +++ b/test/.hints/DataTypesSimple.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "ed3c1f18f8f9c4b87e53eb44d296e4cb" + "86e253473b894755a57f97ff9cd7d79b" ], [ "DataTypesSimple.f", @@ -35,7 +35,7 @@ "typing_tok_DataTypesSimple.Cons1@tok" ], 0, - "cda8fb46bd361896b1b4e3943748b11a" + "6289530666b0f9378a06fc2a616631cc" ], [ "DataTypesSimple.main", @@ -56,7 +56,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "802d099e093331cae00c32ade1c9873a" + "df35c2f2ffcdc86294964868dd9a7284" ] ] ] \ No newline at end of file diff --git a/test/.hints/Endianness.fst.hints b/test/.hints/Endianness.fst.hints index 9ffa2a5c3..ccc173d32 100644 --- a/test/.hints/Endianness.fst.hints +++ b/test/.hints/Endianness.fst.hints @@ -63,7 +63,7 @@ "typing_FStar.Set.complement", "typing_FStar.Set.singleton" ], 0, - "4a1cf09385fe5a2261a127299aa3469e" + "d9ebfd5b7c557b7ec690248d4624d42c" ] ] ] \ No newline at end of file diff --git a/test/.hints/EqB.fst.hints b/test/.hints/EqB.fst.hints index b67e1d1ff..fa50147fb 100644 --- a/test/.hints/EqB.fst.hints +++ b/test/.hints/EqB.fst.hints @@ -74,7 +74,7 @@ "typing_FStar.UInt32.t" ], 0, - "755812571586e97d20fb705075f08cbb" + "f496dc60046ac4061b81dc94c91be852" ] ] ] \ No newline at end of file diff --git a/test/.hints/EtaStruct.fst.hints b/test/.hints/EtaStruct.fst.hints index 7d44df036..c2feea427 100644 --- a/test/.hints/EtaStruct.fst.hints +++ b/test/.hints/EtaStruct.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "0b1d4e80f8bf8c22bfb6a1c1bb38f4d3" + "00dcb56b778051819ffa5793a36d377f" ], [ "EtaStruct.f", @@ -27,7 +27,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "e8e7690070492d8553eef6303ca4b0f0" + "858e2c678c0c445e2d9e52534eb97935" ], [ "EtaStruct.main", @@ -36,7 +36,7 @@ 1, [ "@query" ], 0, - "1a1da915e6d5dc06eeee7b87796bce7b" + "4794ed5a335a942765da2cb0359d79b2" ] ] ] \ No newline at end of file diff --git a/test/.hints/ExitCode.fst.hints b/test/.hints/ExitCode.fst.hints index 625ec377c..24f1fdc60 100644 --- a/test/.hints/ExitCode.fst.hints +++ b/test/.hints/ExitCode.fst.hints @@ -21,7 +21,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "66c840400e1e51c386dd54e1a55d5422" + "d7247f2a8844e42ccb5c55cd27ac3a22" ] ] ] \ No newline at end of file diff --git a/test/.hints/Failwith.fst.hints b/test/.hints/Failwith.fst.hints index 7b2810415..77fe12fac 100644 --- a/test/.hints/Failwith.fst.hints +++ b/test/.hints/Failwith.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "ab22847cdff2548d55eb757ce08ae374" + "747768eccab23e9468ab06c4f2943231" ], [ "Failwith.main", @@ -33,7 +33,7 @@ "function_token_typing_C.exit_success" ], 0, - "eba298e25e660503bd4b718a478fd69e" + "fee9a65b74849546a772d9e81561fe13" ] ] ] \ No newline at end of file diff --git a/test/.hints/Fill.fst.hints b/test/.hints/Fill.fst.hints index d2af34d40..8df45deb3 100644 --- a/test/.hints/Fill.fst.hints +++ b/test/.hints/Fill.fst.hints @@ -17,7 +17,7 @@ "true_interp" ], 0, - "617ca062dc995b39f30225a96a2b1a34" + "eb8a9df95ce578bbe6c3933900051906" ], [ "Fill.fill_out_uint8", @@ -34,7 +34,7 @@ "true_interp" ], 0, - "6c6cc42a96442f7fe1252d1f9a96cfc6" + "2a423f49ad80f0f9e4d53df97b7be795" ], [ "Fill.test", @@ -106,7 +106,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "a3d2de8d4c6839be15abfd7886235844" + "2d6ec37ffba75ac8b8398e2bbacd3508" ], [ "Fill.main", @@ -155,7 +155,7 @@ "typing_FStar.Set.singleton", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "6f365c9ae2777942820e461f9b8af9f8" + "4dc01e46f13e6b746b04056eba1b4176" ] ] ] \ No newline at end of file diff --git a/test/.hints/Flat.fst.hints b/test/.hints/Flat.fst.hints index aaf5fd89e..36f2232d1 100644 --- a/test/.hints/Flat.fst.hints +++ b/test/.hints/Flat.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "754585aa843a177663bf811664651550" + "b80d1b565e322cbfb4e33cc0a4c5acc3" ], [ "Flat.main", @@ -91,7 +91,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "6d0e80090d8c2c09ab68c7165fa3acca" + "c29548b4707dd17d599cf26096ff95dd" ] ] ] \ No newline at end of file diff --git a/test/.hints/FunPtr.fst.hints b/test/.hints/FunPtr.fst.hints index 73327b112..e520462f1 100644 --- a/test/.hints/FunPtr.fst.hints +++ b/test/.hints/FunPtr.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "fe955c4a903862a3464b6a4ba9bb44a3" + "463115b426ed10b609f1551b389c47e3" ], [ "FunPtr.main", @@ -30,7 +30,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "049733aaffed245d1de6b4d88aee6588" + "78bf6d6c27c80999e92fde41bb041ba5" ] ] ] \ No newline at end of file diff --git a/test/.hints/FunctionalEncoding.fst.hints b/test/.hints/FunctionalEncoding.fst.hints index 82cc7aaec..9e2dacfbe 100644 --- a/test/.hints/FunctionalEncoding.fst.hints +++ b/test/.hints/FunctionalEncoding.fst.hints @@ -15,7 +15,7 @@ "typing_FunctionalEncoding.__proj__Mkanimal__item__species" ], 0, - "c58357fe7a757d94662be0bacd41e888" + "42e990117298bd997cfa5c36b77af09f" ] ] ] \ No newline at end of file diff --git a/test/.hints/GcTypes.fst.hints b/test/.hints/GcTypes.fst.hints index 1f94e45f3..fa5fa987a 100644 --- a/test/.hints/GcTypes.fst.hints +++ b/test/.hints/GcTypes.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "6bfaed2ed4f8ad55c43c4e70b8aac85b" + "c0df1fb40d9750c6f2018b9a255d0642" ], [ "GcTypes.main", @@ -33,7 +33,7 @@ "refinement_interpretation_Tm_refine_abf749ae3c800f91a6f1dcf2ecb5621e" ], 0, - "c08802c21c060ba1b991631a50f4e84e" + "ec7e9ca31ec1f65ed02937207332fda4" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ghost1.fst.hints b/test/.hints/Ghost1.fst.hints index 444ee36e7..268d682f2 100644 --- a/test/.hints/Ghost1.fst.hints +++ b/test/.hints/Ghost1.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "a4dc5dc7ad4ea1b6f0efe54fe870606f" + "e8dc27ef83dbab1372407f8a139ec076" ], [ "Ghost1.test", @@ -29,7 +29,7 @@ 1, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "66c07aed4ecd54ed6125993cb269c7ac" + "452732117d4c62fbb5efed58f50f5cf6" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder.fst.hints b/test/.hints/HigherOrder.fst.hints index 0b0774afb..1dab07efa 100644 --- a/test/.hints/HigherOrder.fst.hints +++ b/test/.hints/HigherOrder.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "f92a8a3c20cb25650880b744a4598410" + "e10b6b0887995724bb36ff3e19685bfe" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder2.fst.hints b/test/.hints/HigherOrder2.fst.hints index 3aa8725df..6fe3189f8 100644 --- a/test/.hints/HigherOrder2.fst.hints +++ b/test/.hints/HigherOrder2.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "0d9487d66c8c31713b06346be22deb0e" + "a7b0575d105eb6fe4d945d9cde240dd1" ], [ "HigherOrder2.exampleFunc", @@ -31,7 +31,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "5db302fa81794f7cc04f890ac6c21559" + "06c480d2143bcfa6395c26a644eee9bb" ], [ "HigherOrder2.main", @@ -60,7 +60,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "f2c18ec91d40511e8091ae2b023ac19f" + "29be37c8231c8c8692ccb513c64e0e2f" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder3.fst.hints b/test/.hints/HigherOrder3.fst.hints index 9584f14ec..db57207c4 100644 --- a/test/.hints/HigherOrder3.fst.hints +++ b/test/.hints/HigherOrder3.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "c4a2583820b1239d0e812626aa052d0d" + "73513e9b40d42b7e6cdb84902cda83f8" ], [ "HigherOrder3.exampleFunc", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "8b2dfbc5df869c1d4f9d84b460999cde" + "5ee7a9e62af5403bd9e8f1cbdfc2bed2" ], [ "HigherOrder3.main", @@ -50,7 +50,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "c3b100f874ca65d56ae2761f8293b887" + "40567965fbc37d6df9aa2b439c196678" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder4.fst.hints b/test/.hints/HigherOrder4.fst.hints index 3eefb2f29..c5b5f1d3d 100644 --- a/test/.hints/HigherOrder4.fst.hints +++ b/test/.hints/HigherOrder4.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "4a83e6df4c4ba9cfb3be677d6c2f8d83" + "499240ea5f0c586f3f2f666481378bd1" ], [ "HigherOrder4.createContainer", @@ -66,7 +66,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "189c423bd89a819eddd0993bb87164e7" + "ca261f71342dee1027134f98a4d5336b" ], [ "HigherOrder4.main", @@ -118,7 +118,7 @@ "typing_Prims.pow2" ], 0, - "c38b878d37b7f814f986a582ff6058d5" + "e5f2ea629e7ee925dd6f021bc15c8da4" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder5.fst.hints b/test/.hints/HigherOrder5.fst.hints index 3b27cc83c..2beb97d8c 100644 --- a/test/.hints/HigherOrder5.fst.hints +++ b/test/.hints/HigherOrder5.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "9e320e866ea0016bdb306cb794d0f49f" + "2e5f641faf8ffe076990f59adfa88c21" ], [ "HigherOrder5.t_D", @@ -25,7 +25,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperHeap.rid" ], 0, - "e87ba8b7ede3605ca93aab03c2c9d6ce" + "287da05019dbf3210998642cb77f23d0" ], [ "HigherOrder5.foo", @@ -38,7 +38,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "94ffcce4a5a13d2caeed46601fb1897b" + "b74c4a6d4e86044039b51b31cc86442e" ], [ "HigherOrder5.main", @@ -87,7 +87,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "a2f1ed58e28f436b5a68e96843e18449" + "68eba598ff132974774b1d41015f640e" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder6.fst.hints b/test/.hints/HigherOrder6.fst.hints index 6347e0289..cd82bb9c3 100644 --- a/test/.hints/HigherOrder6.fst.hints +++ b/test/.hints/HigherOrder6.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "80c061adb1043a7f1a1b78f4d8415bac" + "b8e6f23decb47c9801e1707171f579ea" ], [ "HigherOrder6.t_D", @@ -25,7 +25,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperHeap.rid" ], 0, - "c6ad7ee067290e76c7a0cfdb29693098" + "a3c3535f8f2de2417364f5bacf1616a8" ], [ "HigherOrder6.foo", @@ -38,7 +38,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "64c84813c1e723b9af53d21a3c841a99" + "14c1a970cc47237efa2a0172a985c0d4" ], [ "HigherOrder6.main", @@ -87,7 +87,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "f93f22ae8c7f9fd324200caf8e7dba75" + "732c47404136c79b1ed0f12c74a3c714" ] ] ] \ No newline at end of file diff --git a/test/.hints/Hoisting.fst.hints b/test/.hints/Hoisting.fst.hints index 3f4c99b22..3d1c8389b 100644 --- a/test/.hints/Hoisting.fst.hints +++ b/test/.hints/Hoisting.fst.hints @@ -42,7 +42,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "e2373cde4a4940135a07b1c8247298ce" + "111bcb81dd7c5a3da35d0c52fd10716e" ], [ "Hoisting.main", @@ -127,7 +127,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "da393b0adf4a6d55175927af27226fb0" + "aa2d8ae56cbc28acd137ad507046df13" ] ] ] \ No newline at end of file diff --git a/test/.hints/IfDef.fst.hints b/test/.hints/IfDef.fst.hints index 1bc7e99ae..3ce033cad 100644 --- a/test/.hints/IfDef.fst.hints +++ b/test/.hints/IfDef.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "8994378441296f4922a1935e1a0cc8bd" + "2743f2a41c9b83b47993cd114d60802c" ], [ "IfDef.foo'", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "bfcfe61158c7eeed195e6ee5a5318fe2" + "78e4c216e882d2ec803916dd96b33d7a" ], [ "IfDef.test", @@ -63,7 +63,7 @@ "unit_typing" ], 0, - "4a23b565e90198070810b8280e7cfbea" + "29f3fb79d5f62f470dc4012aef540b20" ], [ "IfDef.bar", @@ -84,7 +84,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "a293fd2bea3b8cc66ca086a805eacdb6" + "42dfca5454b39da730b479926e37f6e2" ], [ "IfDef.test3", @@ -93,7 +93,7 @@ 1, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "9eecb320b90155165d930fa1f3e1173d" + "ecc4b05f79991399ee204a8878c79b9d" ] ] ] \ No newline at end of file diff --git a/test/.hints/IfThenElse.fst.hints b/test/.hints/IfThenElse.fst.hints index 01df4b99d..30df54b9e 100644 --- a/test/.hints/IfThenElse.fst.hints +++ b/test/.hints/IfThenElse.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "193e2c66f6617072f7fb77dabc2e0ea7" + "24ae9f4722376906aedf4cca38e21486" ], [ "IfThenElse.main", @@ -34,7 +34,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "9c9b4fc9933de1998d9647c9dc9a063a" + "1cbefa503c40f9007d360051b291dd82" ] ] ] \ No newline at end of file diff --git a/test/.hints/InitializerLists.fst.hints b/test/.hints/InitializerLists.fst.hints index a2c3b4c41..1fd3ac487 100644 --- a/test/.hints/InitializerLists.fst.hints +++ b/test/.hints/InitializerLists.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "d29c8504131f758ce57b9839a97fb08c" + "778d61efe152c3bed60c22449c1de8b3" ], [ "InitializerLists.x2", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "b9218e672ece8481cbc8d12e0da67c3c" + "5599a9b848e63582afbe2e0a3c3da658" ], [ "InitializerLists.x3", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "37fef042b0ab29e26add19d54e698ae5" + "418133b48089d5a61836a88458760497" ], [ "InitializerLists.f", @@ -96,7 +96,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "85ec1842d404fca1926f29c0d74d99d9" + "6672c7caeb144829c728a8ab0b4a89ff" ], [ "InitializerLists.main", @@ -147,7 +147,7 @@ "typing_InitializerLists.x" ], 0, - "22b515e29411538c0981a97130671aa0" + "64cd57fd60bfa0a7a839700ed9550693" ] ] ] \ No newline at end of file diff --git a/test/.hints/Inline.fst.hints b/test/.hints/Inline.fst.hints index d5207f2eb..a3d96bb93 100644 --- a/test/.hints/Inline.fst.hints +++ b/test/.hints/Inline.fst.hints @@ -37,7 +37,7 @@ "typing_FStar.Int32.t", "typing_FStar.Int32.v" ], 0, - "c1748fa88816f1f833d38ae7b38c06ad" + "48f81cf1be650af083c782581953efb1" ], [ "Inline.main", @@ -118,7 +118,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "6c353c551c62c5841f9e4a1161759030" + "84e44e50b5a384ec3af49ed92f955570" ] ] ] \ No newline at end of file diff --git a/test/.hints/InlineNoExtract.fst.hints b/test/.hints/InlineNoExtract.fst.hints index f04ac8d10..baf800cc5 100644 --- a/test/.hints/InlineNoExtract.fst.hints +++ b/test/.hints/InlineNoExtract.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "55aa6c74a4232b842c26749be194d47d" + "ceced0abc7aa05c44b0a4a14056e91d7" ], [ "InlineNoExtract.b", @@ -29,7 +29,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "f203ce8c809f4d66b810ed77a777a013" + "69e5d0520d66ebed2c6d03e4c6c5740f" ] ] ] \ No newline at end of file diff --git a/test/.hints/InlineTest.fst.hints b/test/.hints/InlineTest.fst.hints index 7559aa3a5..4fafe2817 100644 --- a/test/.hints/InlineTest.fst.hints +++ b/test/.hints/InlineTest.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "e4595facad533206a33ce4df31bf0bee" + "9e36a5702afd6a53feeba2e6512d3443" ], [ "InlineTest.__proj__Error__item___0", @@ -21,7 +21,7 @@ "refinement_interpretation_Tm_refine_dc1c4313057dcc858ffa9fd88c3f020d" ], 0, - "335efa3dd61fc364f065ef828155d617" + "e46f139e8f94eacf0744b5870812aa0c" ], [ "InlineTest.__proj__Correct__item___0", @@ -34,7 +34,7 @@ "refinement_interpretation_Tm_refine_dc046c5c58c78691ac946f81662277ac" ], 0, - "d04f3a28441d7200f924b4e3849a3714" + "7ca4cbf29eb486db93d6473b64f3f123" ], [ "InlineTest.main", @@ -52,7 +52,7 @@ "projection_inverse_InlineTest.Correct__b" ], 0, - "2f09bbe5b32e11e6617cfa9c512cffde" + "fce5db17d161986b8123ce99c1a59aa3" ] ] ] \ No newline at end of file diff --git a/test/.hints/Intro.fst.hints b/test/.hints/Intro.fst.hints index 88d8af4a3..90bbfce2c 100644 --- a/test/.hints/Intro.fst.hints +++ b/test/.hints/Intro.fst.hints @@ -82,7 +82,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "0beec881787b4f9c90e6b8cf3314a21e" + "5530273dcb88222738b36203ef459fd2" ] ] ] \ No newline at end of file diff --git a/test/.hints/Layered.fst.hints b/test/.hints/Layered.fst.hints index 668383e4c..c9156f470 100644 --- a/test/.hints/Layered.fst.hints +++ b/test/.hints/Layered.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "86da433ee1b06a2f6ad60a75a9caea1f" + "68982dfc821d8f2275530b547ee8d14b" ], [ "Layered.return", @@ -29,7 +29,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "5b8e4c7d9bb3c7dcf6c1b55b040417ca" + "6f57f82690b672556550c138ccd5497b" ], [ "Layered.bind_wp", @@ -53,7 +53,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "d0b1b1377d7a2a975134b051ecbcf7f6" + "e9f68101aec566eeed3bc142c2153536" ], [ "Layered.bind", @@ -89,7 +89,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "f48b950ae858b6a6340fb016087b932a" + "756e48795cb9830fa4dd261ce4b86a60" ], [ "Layered.subcomp", @@ -110,7 +110,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "23d7637391aae209fa92c082bd10f6ad" + "c13b4b3d88f485e3f79ef9c72afcb994" ], [ "Layered.if_then_else_wp", @@ -125,7 +125,7 @@ "refinement_interpretation_Tm_refine_b5b7150a72165c5a72019df5afbe737b" ], 0, - "2b0fa9be85bb6bfdbe141740715be333" + "fd1f5a64bee24cb578e8f1e1d7dd8207" ], [ "Layered.BUG", @@ -137,7 +137,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "0b4bf2ccd0a5bcdf00278d3fe4625e7f" + "564d09cf3bd8db6ddc6e1829c78640c4" ], [ "Layered.BUG", @@ -149,7 +149,7 @@ "refinement_interpretation_Tm_refine_de09779676242898794a0b057d5f5bb4" ], 0, - "0b2057ed6b60fba6c7a5d5696e49ec7b" + "a03828b58e55e61382cbf0607f959ac6" ], [ "Layered.get_ctx", @@ -175,7 +175,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "ab430ca34d92d62401c16c3d4d096a4b" + "af628e0d3effdc3b5c226cfbccc05cfa" ], [ "Layered.lift_pure_wp", @@ -196,7 +196,7 @@ "typing_Tm_abs_d0f415a5361a9d7988d8e425dc193472" ], 0, - "2222a2c38aa2b32ea887d5ca11657a02" + "035aa2b3f45fcba0bc2204c643f28b8c" ], [ "Layered.lift_pure", @@ -227,7 +227,7 @@ "typing_Tm_abs_efa2eac81cd2c08d7047b2fc27fb6578" ], 0, - "b4efb0ac7b417f61aa27bf532378aece" + "1f6c96c2df44e4c55cbf87b6d373caa4" ], [ "Layered.test", @@ -254,7 +254,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "a5f070c02ea95d67ad7ded5f27558f0b" + "e97db8f9651fcbad3c0a814aa7fd5178" ], [ "Layered.main", @@ -283,7 +283,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "d91c88d7211ef3d0e2375d94ba8b59cd" + "6b976501824538b4a31b5e3c916ef766" ] ] ] \ No newline at end of file diff --git a/test/.hints/Library.fst.hints b/test/.hints/Library.fst.hints index 8030a5392..c13ec55a8 100644 --- a/test/.hints/Library.fst.hints +++ b/test/.hints/Library.fst.hints @@ -82,7 +82,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "1b66bc96d6fe1dc45692df8b3eba621e" + "1d0e76890011a3051bb47873b68cdb52" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList1.fst.hints b/test/.hints/LinkedList1.fst.hints index 5f1eccdff..16b5e1929 100644 --- a/test/.hints/LinkedList1.fst.hints +++ b/test/.hints/LinkedList1.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_a3ca1ff7326b0e9a8828d37afc6032a0" ], 0, - "47c52578abf5556c4e94fda0db62cbe2" + "2e640a45ad8eb3e4e3f739a7d7c2f0ea" ], [ "LinkedList1.__proj__Cons__item__data", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_a3ca1ff7326b0e9a8828d37afc6032a0" ], 0, - "d751b2ff4899e575ca6bf00ec554829e" + "443ea7682b0b33a932da7212822bc38a" ], [ "LinkedList1.well_formed", @@ -46,7 +46,7 @@ "well-founded-ordering-on-nat" ], 0, - "3658a833816cdd19512968234a90e088" + "82eb7fc5bc04fb88fe1a897bd3c00dfe" ], [ "LinkedList1.cons_nonzero_length", @@ -66,7 +66,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "4f7c2179e9442ff437f0537b037ca748" + "e78a9726e34b23c91339764c6ed13afa" ], [ "LinkedList1.length_functional", @@ -80,7 +80,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "8c0448260103dd468059b8938e868e67" + "e2cabb485ad63aece27fd40776d88e3e" ], [ "LinkedList1.length_functional", @@ -130,7 +130,7 @@ "well-founded-ordering-on-nat" ], 0, - "1e83d64c84ebbb6faf7e2d387fbde1f6" + "8fe90657575d4fd68090c9e9808c1d2c" ], [ "LinkedList1.live_nil", @@ -163,7 +163,7 @@ "typing_FStar.Monotonic.HyperStack.sel" ], 0, - "4aa1a863c497a277d52f9be9cc968933" + "fe357115063438fb675bb2585bdb2a62" ], [ "LinkedList1.live_cons", @@ -207,7 +207,7 @@ "typing_LinkedList1.__proj__Cons__item__next" ], 0, - "a82e48d1209ecb747fca060422ad0697" + "1ea3205ad79241241d9fead0ba7ef89d" ], [ "LinkedList1.disjoint", @@ -221,7 +221,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "0b05f5a20487469fa4c8ccac179fb1ca" + "a1cb802b1ef52f74b1fad6ca448bcf27" ], [ "LinkedList1.disjoint_from_list", @@ -236,7 +236,7 @@ "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons" ], 0, - "657799ee5eeeefa4c3d87b84bf62eec1" + "ebeb9f47861d65d097bc2b18c57d2010" ], [ "LinkedList1.footprint", @@ -250,7 +250,7 @@ "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d" ], 0, - "797ebfd6cad25fccb1ec6cde62a868d5" + "d1f052bc9b610c582f0510b25a1c3557" ], [ "LinkedList1.footprint", @@ -313,7 +313,7 @@ "typing_FStar.Heap.trivial_preorder", "well-founded-ordering-on-nat" ], 0, - "47edbe5280e7e4b13952d685218fd88b" + "035b7cf2fc4a0a07f7413bb9a0f665c9" ], [ "LinkedList1.footprint", @@ -381,7 +381,7 @@ "well-founded-ordering-on-nat" ], 0, - "ba72d51e4dc24643bb04baf7a8067e7d" + "51a45c8d89d1edc814c08cdf953d7df4" ], [ "LinkedList1.modifies_disjoint_footprint", @@ -410,7 +410,7 @@ "typing_FStar.Monotonic.HyperStack.as_addr" ], 0, - "5d646b126b144286a8364131593e0ee9" + "ef7613b33f4a844c3569b99154044bb1" ], [ "LinkedList1.modifies_disjoint_footprint", @@ -533,7 +533,7 @@ "well-founded-ordering-on-nat" ], 0, - "54ae8052571b66549898e3210c4aac79" + "35076ae57c54cfec05f83778e94824bf" ], [ "LinkedList1.well_formed_distinct_lengths_disjoint", @@ -547,7 +547,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "4dc66ccbf1521d1a66571a88b14d101e" + "eecdee61c894ff5278d7998d1129d4a5" ], [ "LinkedList1.well_formed_distinct_lengths_disjoint", @@ -621,7 +621,7 @@ "typing_LinkedList1.disjoint", "well-founded-ordering-on-nat" ], 0, - "cd854b2fd1778d6e5b38ec9a450b08ad" + "935f79b5a7472d215834482650daa8e6" ], [ "LinkedList1.well_formed_gt_lengths_disjoint_from_list", @@ -634,7 +634,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "245250f39621e187be5786bbef64385f" + "6a6563e759a6f6638afbded8659279b3" ], [ "LinkedList1.well_formed_gt_lengths_disjoint_from_list", @@ -721,7 +721,7 @@ "well-founded-ordering-on-nat" ], 0, - "0f4af885e7a7fd92fc23d1700a2d8cca" + "343eb3d0ef08b512ab19ed457abd1854" ], [ "LinkedList1.well_formed_head_tail_disjoint", @@ -787,7 +787,7 @@ "typing_LinkedList1.footprint", "unit_typing" ], 0, - "d6677b7098b41ebd175a2cdc7af8c054" + "210345c7521830b07defc7159f18677a" ], [ "LinkedList1.unused_in_well_formed_disjoint_from_list", @@ -800,7 +800,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "26be27fbc7b690b035d1c39f715ba096" + "0f77a5a34b7d37230f9b2f657e903eb3" ], [ "LinkedList1.unused_in_well_formed_disjoint_from_list", @@ -887,7 +887,7 @@ "typing_LinkedList1.footprint", "well-founded-ordering-on-nat" ], 0, - "ac750ff1c89b3501b1f3d8f3034b0987" + "59737c16d19c980d7a66753f848294e6" ], [ "LinkedList1.pop", @@ -905,7 +905,7 @@ "typing_FStar.Pervasives.Native.uu___is_Some" ], 0, - "bb2c41f16d781381d9ea98ddd27dc9bf" + "1c7eded9941ba95684b2b0fe4251efcd" ], [ "LinkedList1.pop", @@ -1045,7 +1045,7 @@ "typing_LowStar.Monotonic.Buffer.loc_addresses" ], 0, - "f1fcd1d2eddd5aa8da9459063c99224c" + "016c1d7e20227e7c9387d1407ae13213" ], [ "LinkedList1.push", @@ -1060,7 +1060,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "0b153b661e45b0eaae4532a091c93df7" + "91ca93b26c8331c2b0491fcb7397f1fa" ], [ "LinkedList1.push", @@ -1219,7 +1219,7 @@ "typing_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs" ], 0, - "6be6fe56237daceb3387e74c5e8b5c77" + "b3a959642a81d0941f89056c83a136c6" ], [ "LinkedList1.length", @@ -1231,7 +1231,7 @@ "haseqFStar.Kremlin.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "bab0c11ec6f4a82ac7ea3abf201a86fc" + "6669cf5b116bca9f0c476fce30e92a8b" ], [ "LinkedList1.length", @@ -1301,7 +1301,7 @@ "typing_FStar.UInt32.v" ], 0, - "ca1ae1a17bba0cc5cac6bc3f48098792" + "0178d0f58493cbc3c9916f6131d28893" ], [ "LinkedList1.main", @@ -1386,7 +1386,7 @@ "typing_FStar.StrongExcludedMiddle.strong_excluded_middle" ], 0, - "2479e8a81cace533cc8708a3d0d6b844" + "a10801fc7ba8f505fb6b7f2f3bdaff49" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList2.fst.hints b/test/.hints/LinkedList2.fst.hints index 88c51b5d6..b56ed574d 100644 --- a/test/.hints/LinkedList2.fst.hints +++ b/test/.hints/LinkedList2.fst.hints @@ -18,7 +18,7 @@ "well-founded-ordering-on-nat" ], 0, - "2d10299d6129d069141d3a06b4c98ee0" + "cfdc55877f80d828d0722efbb58066ca" ], [ "LinkedList2.cons_nonzero_length", @@ -44,7 +44,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "22a9ec3ee72bdaadaa3626ac20ba8c2d" + "c53643654c3c08f9c029875d8f5d033e" ], [ "LinkedList2.length_functional", @@ -58,7 +58,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "be9b9541fa487029a72bda0177dd0322" + "40b1de7f1f9a761d9e3be561fc7fc3be" ], [ "LinkedList2.length_functional", @@ -93,7 +93,7 @@ "well-founded-ordering-on-nat" ], 0, - "794e019136f1bd2222c4026aac239401" + "18b7a8e318801f2fa34c6e832360aa85" ], [ "LinkedList2.live_nil", @@ -119,7 +119,7 @@ "typing_C.Nullity.is_null", "typing_FStar.Buffer.length" ], 0, - "4b505c2c47d87e3ca3b7a19f0f746efb" + "0b89d00e69cc60a5099fad9cd4aa4848" ], [ "LinkedList2.live_cons", @@ -163,7 +163,7 @@ "typing_LinkedList2.__proj__Mkcell__item__next" ], 0, - "1bfa6e0b041fa77ccf373e93049af7e2" + "debc4baec17a900b452fda706dc953e0" ], [ "LinkedList2.footprint", @@ -194,7 +194,7 @@ "well-founded-ordering-on-nat" ], 0, - "a1f32e4892cfca8bb55342bad2f2e191" + "d1c7803e47bb41ec2e47b37c654987a4" ], [ "LinkedList2.modifies_disjoint_footprint", @@ -207,7 +207,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "889aec77305ed4a964deddd0705f6fe6" + "16b9c1ed3a7780da655941486526c8f5" ], [ "LinkedList2.modifies_disjoint_footprint", @@ -282,7 +282,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "64ef56f9df2eb14dc11a13e8f7b4c6f0" + "7213fbc0c299e1d0451e9f55ceba6f47" ], [ "LinkedList2.well_formed_distinct_lengths_disjoint", @@ -296,7 +296,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "5719413e3fc78088a3457d4c8e3e3a91" + "0d84d2654c4dcf18b9d2fff29ca8fb3c" ], [ "LinkedList2.well_formed_distinct_lengths_disjoint", @@ -348,7 +348,7 @@ "well-founded-ordering-on-nat" ], 0, - "ba74141f932fe2ce0ac6179557afb9a8" + "0d6cd434bbf060ba9dd537c6d9e7b2dd" ], [ "LinkedList2.well_formed_gt_lengths_disjoint_from_list", @@ -361,7 +361,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "8625d733be2b07179c824ce8659c08bc" + "7c65391ea7466739daba6a5a4e20042d" ], [ "LinkedList2.well_formed_gt_lengths_disjoint_from_list", @@ -418,7 +418,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "c8d8f2edb3bfffeb3f64489776243534" + "56b2b3e15025999cfdc6b6e32dd175d0" ], [ "LinkedList2.well_formed_head_tail_disjoint", @@ -461,7 +461,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "9f58991a7bdff88b75391360488474c6" + "f181f489945a7508055c6e475016c20b" ], [ "LinkedList2.unused_in_well_formed_disjoint_from_list", @@ -474,7 +474,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "6f675f585c64289069cbd521b4d6a776" + "9157dfea297d199ceef19dafc0719f8c" ], [ "LinkedList2.unused_in_well_formed_disjoint_from_list", @@ -533,7 +533,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "e54c4c5fc56199a913a19ef8b0b9ab7c" + "13d49a95379d65611798815ca26801b8" ], [ "LinkedList2.pop", @@ -549,7 +549,7 @@ "refinement_interpretation_Tm_refine_610746826f8faaaa969bcb2a27509311" ], 0, - "c62398853ae09e14062321a09f988e73" + "94e06525b01888fba7b5f65918a13a2c" ], [ "LinkedList2.pop", @@ -603,7 +603,7 @@ "typing_LinkedList2.footprint", "typing_LinkedList2.t" ], 0, - "b180293c0f476f4a5c7324d59cb18225" + "1da9388c5cd387b31c4d6841fa608e88" ], [ "LinkedList2.push", @@ -620,7 +620,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "4f2c343752051f6818f285e0fe643347" + "dbb37c6102ce3a4d60b1b16c96b05751" ], [ "LinkedList2.push", @@ -732,7 +732,7 @@ "typing_LinkedList2.t" ], 0, - "751b6076f844df11ee368a3c99045321" + "b4e3bd58e9240761f5672be5ddc2a3d4" ], [ "LinkedList2.length", @@ -744,7 +744,7 @@ "haseqFStar.Kremlin.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "0ca425c12e8cc521b1c4384655a4332a" + "6960c56d0a86fa88ef5d5cec11dc6b63" ], [ "LinkedList2.length", @@ -808,7 +808,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "7a003c1eae21830629efef9232568f78" + "05789548327db8a554811feac2b071c4" ], [ "LinkedList2.main", @@ -892,7 +892,7 @@ "typing_FStar.UInt32.v", "typing_LinkedList2.t" ], 0, - "6b73979b2878cdf4a003afb57dbe0689" + "92a2148194448b00aa7b5873bded7315" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList3.fst.hints b/test/.hints/LinkedList3.fst.hints index 8af22e6c5..eed9e0fb7 100644 --- a/test/.hints/LinkedList3.fst.hints +++ b/test/.hints/LinkedList3.fst.hints @@ -18,7 +18,7 @@ "well-founded-ordering-on-nat" ], 0, - "03fc6fb4782dbf751b1abc30913161c5" + "90048659b20d5a622d394bb63f851a03" ], [ "LinkedList3.cons_nonzero_length", @@ -50,7 +50,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null" ], 0, - "59c691c3a8739eff75b4eebb66fb6761" + "81ee97a79906ebc4e59e8dfd8c7ca507" ], [ "LinkedList3.length_functional", @@ -64,7 +64,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "7ebaafac3ecfae7b39241bfffaac37dd" + "f8a1094bfb6ed3f33fbd6bcfdd89849e" ], [ "LinkedList3.length_functional", @@ -100,7 +100,7 @@ "well-founded-ordering-on-nat" ], 0, - "b1c6cbe7c49437890707186b70700af6" + "5a27b842251f21bd32ffd089b3f8b596" ], [ "LinkedList3.live_nil", @@ -132,7 +132,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "3abde827c121da600cdeb8687bb1d209" + "5d2db4f1160ebbc008728be7c58d394e" ], [ "LinkedList3.live_cons", @@ -177,7 +177,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "63f8778b3bc4a6f769373172597aef18" + "2fc213b5dc256d77c336d0068b579676" ], [ "LinkedList3.footprint", @@ -207,7 +207,7 @@ "well-founded-ordering-on-nat" ], 0, - "6d54a60ae0cf6cacdb386fe81ed43cc5" + "17a1feb92a8b2570d301869a59bb12ed" ], [ "LinkedList3.modifies_disjoint_footprint", @@ -220,7 +220,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "8012d4bd30ee2e3b24fa68017140d3c3" + "c7cd316184050322005469da8f100714" ], [ "LinkedList3.modifies_disjoint_footprint", @@ -271,7 +271,7 @@ "well-founded-ordering-on-nat" ], 0, - "e1a1a1b4d09eb223c441e46a70b3d5c8" + "a6422da3dbbf67bf819a14a17755c0ef" ], [ "LinkedList3.well_formed_distinct_lengths_disjoint", @@ -285,7 +285,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "8efee2c31cbe744a543693db53366c8d" + "b2be11b7592f9c13e224d00b2efd2e8c" ], [ "LinkedList3.well_formed_distinct_lengths_disjoint", @@ -341,7 +341,7 @@ "well-founded-ordering-on-nat" ], 0, - "e3a19d7a4ab939652e3c5cca8f03fb28" + "8dba3c4b6e0ecffa5ca0b8f353182ce2" ], [ "LinkedList3.well_formed_gt_lengths_disjoint_from_list", @@ -354,7 +354,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "121c75fc1ea3743281962732cac6db89" + "67205417c4db90550a7899098fa4b1d9" ], [ "LinkedList3.well_formed_gt_lengths_disjoint_from_list", @@ -406,7 +406,7 @@ "well-founded-ordering-on-nat" ], 0, - "677f04f03dbc64edc651d6dd316e45f9" + "2f7ca235630e5a511e820e9f08275416" ], [ "LinkedList3.well_formed_head_tail_disjoint", @@ -441,7 +441,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "bc3cc2f851cfdcdfc17b64d341890515" + "3f908a2c90594222501746de901612db" ], [ "LinkedList3.unused_in_well_formed_disjoint_from_list", @@ -454,7 +454,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "ccdc9a08451e7e65ed711312a4c14817" + "1efdc062986402122e1ec4263c509b0c" ], [ "LinkedList3.unused_in_well_formed_disjoint_from_list", @@ -527,7 +527,7 @@ "well-founded-ordering-on-nat" ], 0, - "9a9f5b01e631cd28589956ef7330e152" + "07549cfda2ec894f294dd33ad291da17" ], [ "LinkedList3.pop", @@ -542,7 +542,7 @@ "refinement_interpretation_Tm_refine_849dd87a0704847cf995021569fd0af6" ], 0, - "ef04f6ef174cdf4920c6a7decc63ae08" + "541affbbd175eeaee60198d4c7e3b86e" ], [ "LinkedList3.pop", @@ -597,7 +597,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "fe550885d9d7ad4228abca48912c2af9" + "6b726ae00f6bbcd1c0704fabdcfe9b99" ], [ "LinkedList3.push", @@ -614,7 +614,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "926a6660dc5d9876164109b7d86b2f55" + "43a5ea23ace648720f36569914d39703" ], [ "LinkedList3.push", @@ -715,7 +715,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "05339e59690105c1040c63f580f04ef3" + "8c296a230fa6db3972f7780aeb218fe5" ], [ "LinkedList3.length", @@ -727,7 +727,7 @@ "haseqFStar.Kremlin.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "e9f26621718c45b2604fe0af5720099e" + "38d30bebe23a558a28840f6cd90f4aca" ], [ "LinkedList3.length", @@ -784,7 +784,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "b0d0788164525658eed8f94e7e8173b8" + "dc6c9127b4179e5ff9b9accd94e3f8d6" ], [ "LinkedList3.main", @@ -860,7 +860,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "516e925585f93f6c61e3d68f7267d1e1" + "d0dcc76d6a3ca212a1cf002407d8e901" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList4.fst.hints b/test/.hints/LinkedList4.fst.hints index 91f251038..3eafbb8ce 100644 --- a/test/.hints/LinkedList4.fst.hints +++ b/test/.hints/LinkedList4.fst.hints @@ -15,7 +15,7 @@ "projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "069597af55afe5a039d5b8a2c866080c" + "882a451a3d3cbbe9fde1e6090ade0432" ], [ "LinkedList4.length_functional", @@ -55,7 +55,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "03b734e03194d579e664a519b5e1178e" + "0062e4ade5b28528e22b711a73bd0764" ], [ "LinkedList4.footprint", @@ -84,7 +84,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "3475bc78c4f9298f5d64bea842745baa" + "a5eb698445bdec54230765fc7cd06847" ], [ "LinkedList4.modifies_disjoint_footprint", @@ -97,7 +97,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "9c81760e8181bbe93db477baac54ac03" + "b96969730b01a4178e31083465475aee" ], [ "LinkedList4.modifies_disjoint_footprint", @@ -155,7 +155,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "54041fa7e04db9b6be4a964136fb95b4" + "fd5ea764d1f2dbd62ad6f6a384611867" ], [ "LinkedList4.well_formed_distinct_lengths_disjoint", @@ -169,7 +169,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "f20fd389f488ae8055aef588a352dc12" + "3a65f111fbd13e6a578bcdb65c1dfa72" ], [ "LinkedList4.well_formed_distinct_lengths_disjoint", @@ -223,7 +223,7 @@ "well-founded-ordering-on-nat" ], 0, - "450810f45390ab9ddadb28ea0d5f0788" + "ea550e81a55e186170eac7d0e3ae19d5" ], [ "LinkedList4.well_formed_gt_lengths_disjoint_from_list", @@ -236,7 +236,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "0568e218230cb047f331708e5d4dadaf" + "c293f9147dbe290cb887975975042fcb" ], [ "LinkedList4.well_formed_gt_lengths_disjoint_from_list", @@ -305,7 +305,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "de52d7eb0e8e6c8660d7d0fd09cbdfb1" + "9edd450f6b4ef92c6010a48ee02765c0" ], [ "LinkedList4.well_formed_head_tail_disjoint", @@ -339,7 +339,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "4d74535667fb1b97856b3f58f360d249" + "e7c37a08315c591626c103550698eb27" ], [ "LinkedList4.unused_in_well_formed_disjoint_from_list", @@ -352,7 +352,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "c30620996162734a9b6582d7d00a8ab4" + "fbb6653c602b171f307af51e7dceed22" ], [ "LinkedList4.unused_in_well_formed_disjoint_from_list", @@ -427,7 +427,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "848e3d9190d8d856d4f02fb85a2b6bf1" + "e4b85da6a11c8d793388b9863e801d44" ], [ "LinkedList4.pop", @@ -442,7 +442,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "e30e2a8ee0eb31624f8dfb46793abd86" + "3a8676accd8a4a8ef7babfacc155baf5" ], [ "LinkedList4.pop", @@ -497,7 +497,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "0549e30341f0489ded7dd8b1260d8a08" + "2bb9d5e9750cda7aa5b5b5597ec9b1ac" ], [ "LinkedList4.push", @@ -511,7 +511,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "63bb9360d468741946c631715cc4fe47" + "89bbdef7c4f5760305e889798e86a945" ], [ "LinkedList4.push", @@ -621,7 +621,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "305087dc459f16197618ee4177b9bf0e" + "ab3e3dbe5c4ec8c5934ead0588fd71db" ], [ "LinkedList4.length", @@ -633,7 +633,7 @@ "haseqFStar.Kremlin.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "d023dc0ea8f01b9417117d6830d57ad0" + "e8ec31262074c34075a18e78e15c397a" ], [ "LinkedList4.length", @@ -697,7 +697,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "4daf7e0e508a0da7351fdd6e2957aed0" + "d84c29fa1263f9769dc9dcef41b51cba" ], [ "LinkedList4.main", @@ -791,7 +791,7 @@ "typing_LowStar.Monotonic.Buffer.mnull", "typing_Prims.pow2" ], 0, - "3fa9e37f83ecf4579cba7cbb3c5eb1d6" + "c52da194dd2e5bff94fc0f8608867b6b" ] ] ] \ No newline at end of file diff --git a/test/.hints/Loops.fst.hints b/test/.hints/Loops.fst.hints index 0c4ee0614..e914b9455 100644 --- a/test/.hints/Loops.fst.hints +++ b/test/.hints/Loops.fst.hints @@ -86,7 +86,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "b570daa65e514b290ff2b31a64181ec0" + "1dd3c2202da3e91deed9f2fbc4f176f0" ], [ "Loops.sum_to_n_buf", @@ -190,7 +190,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "977f43f369db10a20492e168b0db8900" + "e12f8bdf6c696cffe8c955ecb1a4f86b" ], [ "Loops.count_to_n", @@ -276,7 +276,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "b8cdb2defa93f8930853457b332636cd" + "cb63f1e66ff9924e4972701830852770" ], [ "Loops.wait_for_false", @@ -306,7 +306,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "c90f04a719071bdd7fab69d709cb2ab8" + "a54d61a2259ea002afe6e9cf1f51329e" ], [ "Loops.test_pre", @@ -318,7 +318,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "4256a7be9171d9dacf6e37fde66559d5" + "f4387d0b344b374d085bd9cf5889a44c" ], [ "Loops.test_post", @@ -330,7 +330,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "d6e18b251c9a676d48b540f3b52a14fe" + "e3c7c0a0e43ec71bfe30eb4b93d501d7" ], [ "Loops.square_while", @@ -460,7 +460,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "6c02d3a35322f3e934906fce801dc073" + "ba37e92140254ced87c82b8c38834f30" ], [ "Loops.test_map", @@ -562,7 +562,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "3f24b7bfbad3293774227eaf3ad85f4f" + "9c29745217e5ae168f42ebded3a3a8f0" ], [ "Loops.main", @@ -661,7 +661,7 @@ "typing_LowStar.Monotonic.Buffer.len", "typing_Prims.pow2" ], 0, - "077efb4c8a6e6f8074b1ec75ecfb2521" + "73dbb6ae398a7f3f5583ac7860b0b166" ] ] ] \ No newline at end of file diff --git a/test/.hints/ML16.fst.hints b/test/.hints/ML16.fst.hints index 74e297845..18b39c87a 100644 --- a/test/.hints/ML16.fst.hints +++ b/test/.hints/ML16.fst.hints @@ -88,7 +88,7 @@ "typing_FStar.UInt.fits", "typing_FStar.UInt32.v" ], 0, - "bd4c2e5a4b54999f5d0cf8045a26c623" + "43f315351e33232cc8eaa817861beafc" ], [ "ML16.test2", @@ -152,7 +152,7 @@ "typing_FStar.UInt32.v" ], 0, - "048cfc5cbc298891a1f4d26779c1bc6a" + "2d202ab6e3fafab05785fb74d52123bd" ], [ "ML16.main", @@ -229,7 +229,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "2eef6dddfea30075afc2a864596e29a8" + "a2cc765f740f7ad3941cdcbdc53de166" ] ] ] \ No newline at end of file diff --git a/test/.hints/Macro.fst.hints b/test/.hints/Macro.fst.hints index d564de7fc..ff737fa58 100644 --- a/test/.hints/Macro.fst.hints +++ b/test/.hints/Macro.fst.hints @@ -24,7 +24,7 @@ "typing_Prims.pow2" ], 0, - "7282f32d4be8c7e40bc97e506c9afe47" + "9c5953de900efeb18fd43091e18977ec" ] ] ] \ No newline at end of file diff --git a/test/.hints/MallocFree.fst.hints b/test/.hints/MallocFree.fst.hints index b12e88880..32c99def0 100644 --- a/test/.hints/MallocFree.fst.hints +++ b/test/.hints/MallocFree.fst.hints @@ -82,7 +82,7 @@ "typing_FStar.UInt32.t", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "dec2f7fcba1ceba7475322ecbd066ff0" + "37822ce3abe9c848b64d3dbcf8039839" ] ] ] \ No newline at end of file diff --git a/test/.hints/MemCpy.fst.hints b/test/.hints/MemCpy.fst.hints index c9bf55550..e9e798392 100644 --- a/test/.hints/MemCpy.fst.hints +++ b/test/.hints/MemCpy.fst.hints @@ -38,7 +38,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.cons" ], 0, - "cd6110072ba0e9e976959f0fa51a113a" + "dad8facbffe1cb3266a1e9cea06eafae" ], [ "MemCpy.memcpy", @@ -47,7 +47,7 @@ 0, [ "@query" ], 0, - "51c84c6fbff5bee2d25cd3a27e351178" + "1383cabca908987262d883ed6af926a2" ], [ "MemCpy.memcpy", @@ -98,7 +98,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "ec95a38e2900b4c50c462fd96d3693ad" + "7641f21b9603c5959cb95ef05c69ea6b" ], [ "MemCpy.main", @@ -195,7 +195,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "b62fd0066acbfb068343af7f138f2568" + "e640f40e6c5fbd27e86840573a3465b8" ] ] ] \ No newline at end of file diff --git a/test/.hints/MemCpyModel.fst.hints b/test/.hints/MemCpyModel.fst.hints index 146029009..b4d8f83d4 100644 --- a/test/.hints/MemCpyModel.fst.hints +++ b/test/.hints/MemCpyModel.fst.hints @@ -39,7 +39,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice" ], 0, - "ae094bdbcf2afc4e1889398f89081937" + "d6b4e02d5ae744161f2e43ee3480bbc1" ], [ "MemCpyModel.memcpy", @@ -125,7 +125,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "fb1ab1524d1e53efc7c921d6373bec84" + "7f9e0bd6ceec28bdd7d085a364ae04e0" ] ] ] \ No newline at end of file diff --git a/test/.hints/Mini.fst.hints b/test/.hints/Mini.fst.hints index 317c739d0..0ea617341 100644 --- a/test/.hints/Mini.fst.hints +++ b/test/.hints/Mini.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_8fd6f269a3ccd743e70c909024d76576" ], 0, - "3c28c79a1942c6535adb4783da82daea" + "db0592906dd907ffa3328f5486089305" ], [ "Mini.g", @@ -39,7 +39,7 @@ "typing_FStar.UInt32.v" ], 0, - "ab9caae286bf0aa682183a7e6f441e88" + "9c04aa61935a02be3dbf3cb9a5a9c86b" ] ] ] \ No newline at end of file diff --git a/test/.hints/MutRec.fst.hints b/test/.hints/MutRec.fst.hints index 8ad7449e1..1ae92af70 100644 --- a/test/.hints/MutRec.fst.hints +++ b/test/.hints/MutRec.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051" ], 0, - "0027e4554eedd6ff37129d0c388ba546" + "33fd00f345c0904bde4ffd44f0797f80" ], [ "MutRec.f", @@ -67,7 +67,7 @@ "typing_FStar.Set.singleton" ], 0, - "e3c268928086131d7041579c73515d80" + "867aff7ef05eccda963973b02ac05832" ] ] ] \ No newline at end of file diff --git a/test/.hints/NameCollisionHelper.fst.hints b/test/.hints/NameCollisionHelper.fst.hints index a70f516f1..005a9de57 100644 --- a/test/.hints/NameCollisionHelper.fst.hints +++ b/test/.hints/NameCollisionHelper.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "87a59d5ce9b2eb4d4f367d11c912abf2" + "2b182c6c596c01b55b21c5421c6268a6" ] ] ] \ No newline at end of file diff --git a/test/.hints/NoExtract.fst.hints b/test/.hints/NoExtract.fst.hints index a09697f11..5315094b2 100644 --- a/test/.hints/NoExtract.fst.hints +++ b/test/.hints/NoExtract.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "3603572ebc224e3b6ddb0d1d56e023e0" + "9a3243cbb81eb3278d9432bc5dbca014" ], [ "NoExtract.b", @@ -29,7 +29,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "ecdd43359e253993af4a2cb944e24899" + "a3bc4ff71e25d8eb093f7f52e4b41600" ] ] ] \ No newline at end of file diff --git a/test/.hints/NoShadow.fst.hints b/test/.hints/NoShadow.fst.hints index bd047070b..b98babe89 100644 --- a/test/.hints/NoShadow.fst.hints +++ b/test/.hints/NoShadow.fst.hints @@ -22,7 +22,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "f39e9e5f87955396ee86eb4857327126" + "63fe7d0186901fdbac8d787ca5107eb4" ], [ "NoShadow.g", @@ -45,7 +45,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "c6e3ea44147b009857f701710a55c4f8" + "5a68a14bbe5a4d709c6426ed2de06110" ], [ "NoShadow.b", @@ -66,7 +66,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "692b4920d93658f42bd771cc08a23618" + "aa90602cc9dd3d12cadae3d38dad1ed6" ], [ "NoShadow.h", @@ -121,7 +121,7 @@ "typing_FStar.Set.singleton" ], 0, - "b80c74526c45b1a6a3ad4713701699ef" + "87d3b77b7b16960bc0ab1fc6a78c5e54" ], [ "NoShadow.main", @@ -146,7 +146,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "69186977767e7dd5fd486de277ae426b" + "356e4525ca35b90d6ebd83d8f27b604b" ] ] ] \ No newline at end of file diff --git a/test/.hints/Null.fst.hints b/test/.hints/Null.fst.hints index 192f6601b..f3e1b1101 100644 --- a/test/.hints/Null.fst.hints +++ b/test/.hints/Null.fst.hints @@ -26,7 +26,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "bea45944f79ad7cdbfc60a50f80784a8" + "4f7684e94427641de5a06647fe776154" ], [ "Null.main", @@ -45,7 +45,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "1630e8e50fe1b9c725f32bf252e46e48" + "02b190a665d2bdce90e34ed9ea08e86a" ] ] ] \ No newline at end of file diff --git a/test/.hints/OptimizedOption.fst.hints b/test/.hints/OptimizedOption.fst.hints index fcdf5691d..efb9a85d2 100644 --- a/test/.hints/OptimizedOption.fst.hints +++ b/test/.hints/OptimizedOption.fst.hints @@ -15,7 +15,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "4159551f014b3207778fc715028edb50" + "087fd2c7054488dfb01f76894f86b7a1" ] ] ] \ No newline at end of file diff --git a/test/.hints/ParamAbbrev.fst.hints b/test/.hints/ParamAbbrev.fst.hints index db3b171b4..12483c623 100644 --- a/test/.hints/ParamAbbrev.fst.hints +++ b/test/.hints/ParamAbbrev.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "0943af3248f0a50e01416b72d30eaa1e" + "7582f697b7f23a757fa30937d8453752" ], [ "ParamAbbrev.g", @@ -42,7 +42,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "da71d5f95aaa0e2fd05334f82c9ab97a" + "290628a9c0fd2d6d61a0ad39dc540e30" ], [ "ParamAbbrev.touch", @@ -63,7 +63,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "03552297a3909c52d6df11fee64c0615" + "688fe2c7e40b3d34aa96538e69f174d2" ], [ "ParamAbbrev.main", @@ -89,7 +89,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "9059b9e9c222a2c5c4be1726779b2ddd" + "38d1d1eb6677e565c0b2bcc05b0bd181" ] ] ] \ No newline at end of file diff --git a/test/.hints/Parameterized.fst.hints b/test/.hints/Parameterized.fst.hints index eeb9b30e2..17b8a1fba 100644 --- a/test/.hints/Parameterized.fst.hints +++ b/test/.hints/Parameterized.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "63b956d41b2e4a45338e68bb4e58de75" + "a9f99a1c4bfd29fece94b35f7fe2a25e" ], [ "Parameterized.get", @@ -27,7 +27,7 @@ "refinement_interpretation_Tm_refine_7661503e258cd8eb6e95252fc3102979" ], 0, - "f73a687179d0356948c3ec16e88c1945" + "c0ce9761c9c33ead266af4cc38c49dd9" ], [ "Parameterized.main", @@ -75,7 +75,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "ec5aa8e7bc33389e5a939a41f7f16dad" + "d02edaeb03b399c97fb6e619c467807b" ] ] ] \ No newline at end of file diff --git a/test/.hints/PatternAny.fst.hints b/test/.hints/PatternAny.fst.hints index 830e36dc7..5c8512705 100644 --- a/test/.hints/PatternAny.fst.hints +++ b/test/.hints/PatternAny.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query", "assumption_PatternAny.role__uu___haseq" ], 0, - "2cf984147c83f3857a38eae3784c4efe" + "90c77dbdf1352bc0300fae71a13d3cff" ] ] ] \ No newline at end of file diff --git a/test/.hints/PolyComp.fst.hints b/test/.hints/PolyComp.fst.hints index 970cd2a0c..0a7da1058 100644 --- a/test/.hints/PolyComp.fst.hints +++ b/test/.hints/PolyComp.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "edc054a6481aa4497786681985a57d8b" + "d5a73e84522990b355cb0461e1d244ca" ], [ "PolyComp.__proj__B__item___0", @@ -20,7 +20,7 @@ "refinement_interpretation_Tm_refine_ace5180d8b9c0680cccc5c56d8744ca7" ], 0, - "4539925f2b8e88d65b2a991a76b061b9" + "df0718b9b2e8b5042a2edf4ae81ebf97" ], [ "PolyComp.one_t", @@ -33,7 +33,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "065754709e459b7d1e698046422f6c90" + "ffd3e63c5b7ce6d4b2e5a99610623c1a" ], [ "PolyComp.another_t", @@ -46,7 +46,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "66f94f23391850ec045204656423da8f" + "0989d9e329f57f4d15ac4a761c652005" ], [ "PolyComp.yet_another_t", @@ -59,7 +59,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "9a7e11ce06167b8745a8ee352b7c56bc" + "66e74d9daa71264f9486b6e73692f35a" ], [ "PolyComp.main", @@ -86,7 +86,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "174324349ec53fc7cbc0abcb115ab297" + "aeb45285bd3f3fd681c504114a436255" ] ] ] \ No newline at end of file diff --git a/test/.hints/Polymorphic.fst.hints b/test/.hints/Polymorphic.fst.hints index e675ec3bd..aa4855268 100644 --- a/test/.hints/Polymorphic.fst.hints +++ b/test/.hints/Polymorphic.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "4680ba6dc0977443d2673037f89c5754" + "a27e4d81c516ef76256b4a086c58f57c" ], [ "Polymorphic.main", @@ -46,7 +46,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "2cc1b7ebc8987b1f76bc9d05b288d52c" + "ca98aae3af6de8f72ed59fee331decc9" ] ] ] \ No newline at end of file diff --git a/test/.hints/Printf.fst.hints b/test/.hints/Printf.fst.hints index ca52da2a0..638fb0f31 100644 --- a/test/.hints/Printf.fst.hints +++ b/test/.hints/Printf.fst.hints @@ -85,7 +85,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "550854ecd53d7b8eef6e54d57c669d61" + "109d4fce0dcf1c303307bcc10c5a198f" ] ] ] \ No newline at end of file diff --git a/test/.hints/Private.fst.hints b/test/.hints/Private.fst.hints index 26752ae78..55b1321d6 100644 --- a/test/.hints/Private.fst.hints +++ b/test/.hints/Private.fst.hints @@ -47,7 +47,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "3aeb6adb0465a2cdeb9e5353aff5f30d" + "96a21ce7779d0d4d9b8aea620bf317e2" ] ] ] \ No newline at end of file diff --git a/test/.hints/PushPop.fst.hints b/test/.hints/PushPop.fst.hints index f6c0f8b55..b1ffd8faa 100644 --- a/test/.hints/PushPop.fst.hints +++ b/test/.hints/PushPop.fst.hints @@ -44,7 +44,7 @@ "typing_FStar.Set.union" ], 0, - "e4a003bac80e6d2a2bf73e1f4cfd0576" + "f0e9f0d6bd6c2a07d310aab854390dbe" ], [ "PushPop.main", @@ -76,7 +76,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "73c91a26fb60752a24bb90d59657a2e6" + "9e8fa60ab4af81c9fb9a3924e5b34d1b" ] ] ] \ No newline at end of file diff --git a/test/.hints/RecordTypingLimitation.fst.hints b/test/.hints/RecordTypingLimitation.fst.hints index d373fd718..b4937134a 100644 --- a/test/.hints/RecordTypingLimitation.fst.hints +++ b/test/.hints/RecordTypingLimitation.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "32a35ef8ba2f5fdee36918020036db08" + "bbd2f61e6ea212235d802605d8da9b20" ] ] ] \ No newline at end of file diff --git a/test/.hints/Recursive.fst.hints b/test/.hints/Recursive.fst.hints index edb277b9c..ffe191c33 100644 --- a/test/.hints/Recursive.fst.hints +++ b/test/.hints/Recursive.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_fe78738bbffac158d58c53f89b03a1b7" ], 0, - "f18f76c306d06af1d6236e12361ef33f" + "54969e55f28f01ff92ccd0c8a002e2a7" ], [ "Recursive.__proj__Cons__item__next", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_fe78738bbffac158d58c53f89b03a1b7" ], 0, - "a6d5a33710837c72dd4db9654875d72e" + "0f37dab0787e71c32af4eb5b1d3fda44" ] ] ] \ No newline at end of file diff --git a/test/.hints/RecursivePoly.fst.hints b/test/.hints/RecursivePoly.fst.hints index bc6f0fcbf..eb448410a 100644 --- a/test/.hints/RecursivePoly.fst.hints +++ b/test/.hints/RecursivePoly.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_ec0be7ef8d42c8c1f9f883ea579d9abf" ], 0, - "b0c3d2ef55bd8dbf2afff3a5975b7fdb" + "f769aa122da4645296f48599d840eaf5" ], [ "RecursivePoly.__proj__Cons__item__next", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_ec0be7ef8d42c8c1f9f883ea579d9abf" ], 0, - "2ec7f9d69f211acb0873bea6fdc4a75a" + "6ff70788e43cd921081f2b836d1ffa82" ], [ "RecursivePoly.f", @@ -46,7 +46,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "3428bb34174d3b8e9b78a2f096cc217b" + "d96a5a68d236f1a0b801cb44a0fa743a" ], [ "RecursivePoly.g", @@ -67,7 +67,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "dec978d66a08c456be8187fcc86329ff" + "cd42335673874e7fbbda97e591aa5cba" ] ] ] \ No newline at end of file diff --git a/test/.hints/Renaming.fst.hints b/test/.hints/Renaming.fst.hints index af0778477..0232e99f1 100644 --- a/test/.hints/Renaming.fst.hints +++ b/test/.hints/Renaming.fst.hints @@ -15,7 +15,7 @@ "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2" ], 0, - "d10c54b6c39d1e72ae9c3c983b516edf" + "3b3af15acef6eec74f20de1a0e455df6" ], [ "Renaming.main", @@ -32,7 +32,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "e6058bb80ebbca0e4997554560cfeac6" + "f7e32c7ff7dc77688f3e1c49ddca8f69" ] ] ] \ No newline at end of file diff --git a/test/.hints/RingBuffer.fst.hints b/test/.hints/RingBuffer.fst.hints index b3a859a1e..17bc659f3 100644 --- a/test/.hints/RingBuffer.fst.hints +++ b/test/.hints/RingBuffer.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "6b1f08d5261eabefb4bbb7a19d51c102" + "51fbf4a6f664e206ae807c7d448326b4" ], [ "RingBuffer.well_formed_f", @@ -24,7 +24,7 @@ "haseqRingBuffer_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "e1be8056c1d0784fd5cc9d07fb208c35" + "b64f6686142f5822b55a314758af1980" ], [ "RingBuffer.next", @@ -51,7 +51,7 @@ "typing_FStar.UInt32.v" ], 0, - "49aab99cc1c075df1cd13143411f1a6b" + "dadb81523ab8c9289c699320bb3a9c66" ], [ "RingBuffer.prev", @@ -77,7 +77,7 @@ "typing_FStar.UInt32.v" ], 0, - "76e4d60daad7215e0e83402f953e18db" + "61671f26ff1a324869e80f9dbbd50b7f" ], [ "RingBuffer.remaining_space", @@ -113,7 +113,7 @@ "typing_RingBuffer.__proj__Mkt__item__total_length" ], 0, - "b7fd92e76afc4c932208bf56aca8c2a2" + "59fcb32cce6f08d4107983cfc3c06f0e" ], [ "RingBuffer.as_list_f", @@ -161,7 +161,7 @@ "well-founded-ordering-on-nat" ], 0, - "a29ada4a423b3938a8be9713844f328f" + "e6882d80bd0bd0d55ea80a1054cdde8e" ], [ "RingBuffer.as_list_f", @@ -203,7 +203,7 @@ "well-founded-ordering-on-nat" ], 0, - "a356f5eab87dd734bb36bdf2cb76d8b8" + "4ae6665c0a1dd588953c5ba3e6327820" ], [ "RingBuffer.seq_update_unused_preserves_list", @@ -229,7 +229,7 @@ "typing_FStar.UInt32.v" ], 0, - "030c63b9d1323192265812b9cf361ee2" + "8200172098ba182ef6b7f31cab7d5059" ], [ "RingBuffer.seq_update_unused_preserves_list", @@ -286,7 +286,7 @@ "well-founded-ordering-on-nat" ], 0, - "7ddfb17fe9f42cc904c8eeea04bd249d" + "5ac07f01804226ac43e17ab514142cfa" ], [ "RingBuffer.as_list", @@ -303,7 +303,7 @@ "haseqRingBuffer_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d" ], 0, - "02af39efbd31aa82ad3d3206e9a7f5d5" + "334168c85912c96a0c74f725189581de" ], [ "RingBuffer.pop", @@ -398,7 +398,7 @@ "typing_RingBuffer.as_list", "typing_RingBuffer.remaining_space" ], 0, - "bac30280c8923865d056fcadde00ece2" + "45674194a4fbcd4fd4d178b527608fc6" ], [ "RingBuffer.push", @@ -504,7 +504,7 @@ "typing_RingBuffer.prev", "typing_RingBuffer.remaining_space" ], 0, - "84f9a4dbf648a3d21e030e340eea4090" + "cd7f10826137a5049da24396a3ae5c3a" ], [ "RingBuffer.one_past_last", @@ -534,7 +534,7 @@ "typing_FStar.UInt32.v" ], 0, - "b07fa54c9e8614673e21a20035ea85a3" + "037b1e96c8f5250d064cda3c344d0dcb" ], [ "RingBuffer.as_list_append_one", @@ -564,7 +564,7 @@ "typing_RingBuffer.one_past_last" ], 0, - "a72ca82207330718898638c626eafab0" + "30c6e423fb9ff2217d534e4c5990a0cb" ], [ "RingBuffer.as_list_append_one", @@ -632,7 +632,7 @@ "typing_RingBuffer.one_past_last", "well-founded-ordering-on-nat" ], 0, - "578e1ae07e73ca0d665f19f7c11aec0b" + "460e661e96c9075e958cdf32c9b122a5" ], [ "RingBuffer.push_back", @@ -721,7 +721,7 @@ "typing_RingBuffer.as_list_f", "typing_RingBuffer.remaining_space" ], 0, - "6afa5514dcda72dad57fe533bc8fc49b" + "fa6894ef4bc2d7e5d64e236b0b267f7d" ], [ "RingBuffer.as_list_minus_one", @@ -757,7 +757,7 @@ "typing_RingBuffer.prev" ], 0, - "821d0ca45f2770b1025bec1294284d67" + "aa4e8df9d67a57ac3339fdb25fced367" ], [ "RingBuffer.as_list_minus_one", @@ -828,7 +828,7 @@ "typing_RingBuffer.prev", "well-founded-ordering-on-nat" ], 0, - "c399023165c1d39d099be6e9fc7043fd" + "ee18316371340eaddf371dd268d92eaa" ], [ "RingBuffer.pop_back", @@ -916,7 +916,7 @@ "typing_RingBuffer.as_list_f", "typing_RingBuffer.remaining_space" ], 0, - "2fac89524702f3596308f4ebca309158" + "2761b20fdf9470f6eef23210de3324fa" ], [ "RingBuffer.create", @@ -1013,7 +1013,7 @@ "typing_RingBuffer.remaining_space" ], 0, - "70c450289348e88a64e4b78d11359458" + "15d9043e20c46cbe0179acaaf5cbe142" ], [ "RingBuffer.main", @@ -1127,7 +1127,7 @@ "typing_RingBuffer.space_left" ], 0, - "dd27638fb96756971964ebdddaf7731a" + "7e158c78cdd25345e0f6c9aef3a185b1" ] ] ] \ No newline at end of file diff --git a/test/.hints/Scope.fst.hints b/test/.hints/Scope.fst.hints index ca039099a..bc3731be7 100644 --- a/test/.hints/Scope.fst.hints +++ b/test/.hints/Scope.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "c27438caf92a8f70ab25e03b642c56e1" + "5a431bf905418c44800b0754d423c1b7" ], [ "Scope.main", @@ -117,7 +117,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "f546087830aa669900b485c4365e1a0e" + "7aea2be1acfb78b4eb6a3650d17a0ae2" ] ] ] \ No newline at end of file diff --git a/test/.hints/Server.fst.hints b/test/.hints/Server.fst.hints index ba8013efe..6037f730b 100644 --- a/test/.hints/Server.fst.hints +++ b/test/.hints/Server.fst.hints @@ -16,7 +16,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "4b15bf2820c9c6ebf74e4d683cbe70a6" + "e72e3544b29e8c45686142a828b4a713" ], [ "Server.bufstrcmp", @@ -37,7 +37,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "2db251fd8c4a278d624d2a270ffb78c0" + "f274ded93f8a48c40d907f03313a50ba" ], [ "Server.bufstrcmp", @@ -193,7 +193,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "5bca9b9497b71f6c52de56b4a3299d2d" + "6d41f18f87554441175d5226ba58e39c" ], [ "Server.bufstrcpy", @@ -219,7 +219,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "a8569486c2f028a350d0edf187b5f1bb" + "6fc6032c2864918c81b20da01caafae7" ], [ "Server.bufcpy", @@ -243,7 +243,7 @@ "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder" ], 0, - "75e1e4bb9bddef31ba3ca6212b47d3b4" + "ace5e8b804df205d55f65b50d8368527" ], [ "Server.respond", @@ -297,7 +297,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "f7f2785b2aeb84e04b441f016f44a3c0" + "a10fcc025abbffbce5cabe62893c1b1c" ], [ "Server.respond_index", @@ -409,7 +409,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "263e4f8a875555f66edc014a0bd299c2" + "28d6802e9eda2a30ae7cecc59ed9bbee" ], [ "Server.respond_stats", @@ -540,7 +540,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "eee5fec21b6ad8c1c1d92c9cb9359130" + "9fbd9db6af457e56a945b956a1f411ca" ], [ "Server.respond_404", @@ -673,7 +673,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "cf167c21b2cd0726887258f1ccde6028" + "334a9469e3c49c743d1ed9ef0d295cd5" ], [ "Server.server", @@ -812,7 +812,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_Prims.pow2" ], 0, - "86984eb1c3102b8fa071cda2a833b2a9" + "592aae95aa72d21a7d1829932d255d0f" ] ] ] \ No newline at end of file diff --git a/test/.hints/SimpleWasm.fst.hints b/test/.hints/SimpleWasm.fst.hints index 069134ab6..e1db02533 100644 --- a/test/.hints/SimpleWasm.fst.hints +++ b/test/.hints/SimpleWasm.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "519b2b6a37c091a117d64885ea735cfe" + "aafbac017ff53aa7ef45f13e21ac1f5c" ], [ "SimpleWasm.main", @@ -37,7 +37,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "c380ae9ea8b147c6dc51283cfb2393fb" + "70ec8c3ad67ad670c8d9309aa59b5731" ] ] ] \ No newline at end of file diff --git a/test/.hints/StaticHeaderLib.fst.hints b/test/.hints/StaticHeaderLib.fst.hints index 1d1292002..0afb295ed 100644 --- a/test/.hints/StaticHeaderLib.fst.hints +++ b/test/.hints/StaticHeaderLib.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "2bb9ec4e614a5e8012bd8a1ad7c66632" + "f64087a263cea80b81e6caf1016c5c24" ], [ "StaticHeaderLib.private_helper", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "65b3e0a5246f0f4bba4d4ca4bb663c2c" + "ced45005ccf988ab0dad758236bfd113" ], [ "StaticHeaderLib.helper", @@ -42,7 +42,7 @@ 1, [ "@query", "typing_StaticHeaderLib.__proj__Mkt__item__x" ], 0, - "3d4ddd36b123842ffd457916df25793c" + "333f0346d7de65064e1fd0e10ddcb2b0" ] ] ] \ No newline at end of file diff --git a/test/.hints/StaticHeaderLib.fsti.hints b/test/.hints/StaticHeaderLib.fsti.hints index 9a17bdc4a..c6e72e534 100644 --- a/test/.hints/StaticHeaderLib.fsti.hints +++ b/test/.hints/StaticHeaderLib.fsti.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "2bb9ec4e614a5e8012bd8a1ad7c66632" + "f64087a263cea80b81e6caf1016c5c24" ], [ "StaticHeaderLib.private_helper", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "65b3e0a5246f0f4bba4d4ca4bb663c2c" + "ced45005ccf988ab0dad758236bfd113" ] ] ] \ No newline at end of file diff --git a/test/.hints/StringLit.fst.hints b/test/.hints/StringLit.fst.hints index 013fa92e5..c9253c3cb 100644 --- a/test/.hints/StringLit.fst.hints +++ b/test/.hints/StringLit.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "9c2128b2980896db9ea93ebd745cea25" + "9ed07c6e0e36ee66dcd4c557025fb285" ], [ "StringLit.cat", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "a308bd6549ffd83802d2673e0a85a83e" + "90bd7ad5afd53b37ac45928dbb88be9f" ], [ "StringLit.test_c_string", @@ -50,7 +50,7 @@ 1, [ "@query" ], 0, - "e8f7d8c4f2f7a0d4f3566fcad9acb243" + "e5eaf9a9e3facd3596e7e57b15475633" ], [ "StringLit.main", @@ -69,7 +69,7 @@ "typing_FStar.Int.Cast.uint8_to_int32" ], 0, - "4c036efa3a2e716b994c7fd6b9795572" + "0a6871177bcfb9822ac4d9fb5ca0bebf" ] ] ] \ No newline at end of file diff --git a/test/.hints/Strlen.fst.hints b/test/.hints/Strlen.fst.hints index 70affd245..685a89ed9 100644 --- a/test/.hints/Strlen.fst.hints +++ b/test/.hints/Strlen.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "ba9c970164f4fd8bafb52bad0bb88c14" + "596933d836dd9e5106262d4e591d0d11" ], [ "Strlen.main", @@ -24,7 +24,7 @@ "typing_tok_C.EXIT_FAILURE@tok", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "d1b58d804e1bc9d324a6a6d86a5be6ee" + "9e08861bcb668d6894598dae0a6a3015" ] ] ] \ No newline at end of file diff --git a/test/.hints/Structs.fst.hints b/test/.hints/Structs.fst.hints index 5679015c5..e8e6a52bd 100644 --- a/test/.hints/Structs.fst.hints +++ b/test/.hints/Structs.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "d9683ba87bc99c26f56387a56a80ad64" + "ac1a409b71bab45158f73a19f5f2dfa7" ], [ "Structs.f", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "f76b775e556f2bfe638d91404b92a81e" + "d9b01976ed80ffaf445e2d4cba5c603b" ], [ "Structs.main", @@ -45,7 +45,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "f16eddfe649c8a5bb0ee57903a0295cd" + "98f926475a6b273d17bb2cb63617a487" ] ] ] \ No newline at end of file diff --git a/test/.hints/Structs2.fst.hints b/test/.hints/Structs2.fst.hints index 8b974c944..648f54320 100644 --- a/test/.hints/Structs2.fst.hints +++ b/test/.hints/Structs2.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt8.t" ], 0, - "92644551df0ae59cab84ffc893b08cad" + "68b7ba00469a10a56e96fc889c2e780e" ], [ "Structs2.point", @@ -25,7 +25,7 @@ "typing_FStar.UInt32.t" ], 0, - "a64b77bc4106211e1a4c82b1a634fbac" + "b7665cfa47ff73f8c90dd3f6dbc08600" ], [ "Structs2.t", @@ -37,7 +37,7 @@ "assumption_Structs2.point__uu___haseq" ], 0, - "ed68ee7330f0b467c4bc7bb4cc5065b7" + "4919faa5c2c6b868e61c7597b9e01757" ], [ "Structs2.test1", @@ -58,7 +58,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "3bc864528a64a2680d2f881c271d6ed0" + "50060193daccd019eff90d3be7b9e2ab" ], [ "Structs2.main", @@ -84,7 +84,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "c65571d14c52ade5965fd25fb6b7b989" + "f85feceff78dd663da8b264f09b0b423" ] ] ] \ No newline at end of file diff --git a/test/.hints/Substitute.fst.hints b/test/.hints/Substitute.fst.hints index cd7a4a3cb..954bf7ced 100644 --- a/test/.hints/Substitute.fst.hints +++ b/test/.hints/Substitute.fst.hints @@ -21,7 +21,7 @@ "typing_FStar.Int32.t" ], 0, - "d69d7c27c03ced2b9eb02a695fb6c775" + "ca01aefbc42fb2b7116a46aaf00a2754" ], [ "Substitute.main", @@ -50,7 +50,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "938b862dd7cafc6f71287cd84a80204f" + "093f11b71ab9df42bb1cf2f5adab0461" ] ] ] \ No newline at end of file diff --git a/test/.hints/TailCalls.fst.hints b/test/.hints/TailCalls.fst.hints index edec9de65..654a21375 100644 --- a/test/.hints/TailCalls.fst.hints +++ b/test/.hints/TailCalls.fst.hints @@ -43,7 +43,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "a68f897610f18148c9f9574284fccb2f" + "3e6d8aa47ea1795fb9ba128a183f098c" ] ] ] \ No newline at end of file diff --git a/test/.hints/TestAlloca.fst.hints b/test/.hints/TestAlloca.fst.hints index 843ad359a..4e694668c 100644 --- a/test/.hints/TestAlloca.fst.hints +++ b/test/.hints/TestAlloca.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "316017f1b7a232e917a9434275287a72" + "827e3966849a37d5ced090563729ce22" ], [ "TestAlloca.main", @@ -79,7 +79,7 @@ "typing_FStar.Set.singleton", "typing_FStar.UInt32.v" ], 0, - "fc08e0a6a044210499c15adc9cc6c0df" + "cd0113cb01c1654ac6c90dbc551a5532" ] ] ] \ No newline at end of file diff --git a/test/.hints/TopLevelArray.fst.hints b/test/.hints/TopLevelArray.fst.hints index 68798fe4d..ec43e4251 100644 --- a/test/.hints/TopLevelArray.fst.hints +++ b/test/.hints/TopLevelArray.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "96c984030ed0577498364327862b7b60" + "0f002327c74578d36292b7c2728e97bd" ], [ "TopLevelArray.y", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "c508cb57c430d65d0266b4e7510426f8" + "607b0ecb49d6301cbad6af4ee2eeccf1" ], [ "TopLevelArray.x", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "a5cd874c6b7e274815678bf28eecf687" + "a00dd2b54a23981a58266d8168477a46" ], [ "TopLevelArray.g", @@ -97,7 +97,7 @@ "refinement_interpretation_TopLevelArray_Tm_refine_cb33895ece621ae8bc092dc7297a0116" ], 0, - "4ba7b1521e785e564636f9b8c6742b73" + "fdd101c4cca6a1fb06b66e2887af2147" ], [ "TopLevelArray.main", @@ -119,7 +119,7 @@ "typing_TopLevelArray.__proj__Mkt__item__y", "typing_TopLevelArray.x" ], 0, - "219542d22be66d38d5300fe518f007cb" + "4383adb8093ccbfd1ca3116876543d80" ] ] ] \ No newline at end of file diff --git a/test/.hints/TotalLoops.fst.hints b/test/.hints/TotalLoops.fst.hints index 09e1ba046..cf9aa0dbd 100644 --- a/test/.hints/TotalLoops.fst.hints +++ b/test/.hints/TotalLoops.fst.hints @@ -16,7 +16,7 @@ "well-founded-ordering-on-nat" ], 0, - "a0fe86791487eecfebdac6a47403db00" + "83d57af69892a743d807fffab8495389" ], [ "TotalLoops.t", @@ -30,7 +30,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "805288f5ad2360321badf2c9aec0b52a" + "187da72459d1caf7aa92a2a5c2a2613a" ], [ "TotalLoops.tfib", @@ -70,7 +70,7 @@ "typing_TotalLoops.__proj__Mkt__item__i", "typing_TotalLoops.fib" ], 0, - "9a3ed0b1d22e63f2e67235596543809c" + "715a08d4f9ede38977b910d7d269325e" ] ] ] \ No newline at end of file diff --git a/test/.hints/Tuples.fst.hints b/test/.hints/Tuples.fst.hints index cb2afa856..60d788ce7 100644 --- a/test/.hints/Tuples.fst.hints +++ b/test/.hints/Tuples.fst.hints @@ -47,7 +47,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "e24a85bc4376408414c8630bcc7ce488" + "3e69dcf67ccf1d21a443a5bcedb4356f" ] ] ] \ No newline at end of file diff --git a/test/.hints/UBuffer.fst.hints b/test/.hints/UBuffer.fst.hints index 3ad447ab1..7b3fc94a1 100644 --- a/test/.hints/UBuffer.fst.hints +++ b/test/.hints/UBuffer.fst.hints @@ -98,7 +98,7 @@ "typing_LowStar.UninitializedBuffer.initialization_preorder" ], 0, - "17956544a1c591b54ecf6f030cae1e25" + "fffe6e102c5aedf658af5fa2e08eac25" ], [ "UBuffer.test_ub_stack", @@ -188,7 +188,7 @@ "typing_LowStar.UninitializedBuffer.initialization_preorder" ], 0, - "6eaf457cd3b85832e6aa468937a261a4" + "d6eda2f6b346a0eb9a0f6e9e5f1ba613" ], [ "UBuffer.main", @@ -213,7 +213,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "a270fd5711768a586be4240185ee20f0" + "4a31d761f31caf1bfebad3fab384b72d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unsound.fst.hints b/test/.hints/Unsound.fst.hints index 6f81a22c6..0332e050c 100644 --- a/test/.hints/Unsound.fst.hints +++ b/test/.hints/Unsound.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_652f0f3ffdde8cb9fe553db21d874aee" ], 0, - "74f34f3b4e62b1bf970208f89dfd46e1" + "2545bcf53a8eded8c8cb0202ff7239b1" ], [ "Unsound.g", @@ -26,7 +26,7 @@ "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051" ], 0, - "9475c4c75efbb649b91019bc3e13d81a" + "d3a565aaa4a42759b7ac9acdc9a31ad9" ], [ "Unsound.main", @@ -98,7 +98,7 @@ "typing_FStar.UInt32.t", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "ac27a8a666463138c9c7fa3ce90af39a" + "b0916b12d9fab22445b25591cf3544c2" ] ] ] \ No newline at end of file diff --git a/test/.hints/UnusedParameter.fst.hints b/test/.hints/UnusedParameter.fst.hints index 337773ac1..a6292675d 100644 --- a/test/.hints/UnusedParameter.fst.hints +++ b/test/.hints/UnusedParameter.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int64.t" ], 0, - "2ffbd903a5fbf554addad053279b9693" + "332912aa9f1fb388338c23d2d1064a80" ], [ "UnusedParameter.touch", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "5c69d043dee26d72448ce3179b83e3b7" + "9efa192e76b2a46cc6477384e4d6dc37" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unused_A.fst.hints b/test/.hints/Unused_A.fst.hints index 08b840771..0051fd85b 100644 --- a/test/.hints/Unused_A.fst.hints +++ b/test/.hints/Unused_A.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "bf17ac43ac3ef01b832e995ba40de336" + "744aadb43d0ab8da1f430c28aa05bf7e" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unused_B.fst.hints b/test/.hints/Unused_B.fst.hints index 4bcb10570..69d1db171 100644 --- a/test/.hints/Unused_B.fst.hints +++ b/test/.hints/Unused_B.fst.hints @@ -34,7 +34,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "cf60680db732b163a108264af6e3dd5b" + "a4772d664028f643a95f09ebbd07e38b" ] ] ] \ No newline at end of file diff --git a/test/.hints/Uu.fst.hints b/test/.hints/Uu.fst.hints index 8177d10a8..76b575f23 100644 --- a/test/.hints/Uu.fst.hints +++ b/test/.hints/Uu.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "1a4fce693d26b9cf1cc0e023e65fd1f6" + "814d4a41bf401211ef52b6516449da18" ] ] ] \ No newline at end of file diff --git a/test/.hints/VariableMerge.fst.hints b/test/.hints/VariableMerge.fst.hints index be7cb2e9b..3a440422e 100644 --- a/test/.hints/VariableMerge.fst.hints +++ b/test/.hints/VariableMerge.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "25712309705ef1efd385edb9483424eb" + "9f74b7c47ba302c33917c45c3d8cb051" ], [ "VariableMerge.test", @@ -34,7 +34,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "5d1347dcc59b07b0847afbf2590a4924" + "71d20b3076327786baaafe4e7dd7b6d0" ], [ "VariableMerge.test1", @@ -56,7 +56,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "8efc1fadabe71c647bae8aefe55c8e48" + "ff756c1c9a007caba5e64a3112d98e8c" ], [ "VariableMerge.test2", @@ -78,7 +78,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "0aedb0fe706dd8ab4ee5f6448ad6e2e9" + "a5c8cf0495425d7935a28fda7ce75d67" ], [ "VariableMerge.main", @@ -101,7 +101,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "59c3d64d7221e98fc00549ad2ff77709" + "fed21cc311e0ba045298438a3490de81" ] ] ] \ No newline at end of file diff --git a/test/.hints/Verbatim.fst.hints b/test/.hints/Verbatim.fst.hints index bd3144577..9fa718372 100644 --- a/test/.hints/Verbatim.fst.hints +++ b/test/.hints/Verbatim.fst.hints @@ -15,7 +15,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "ef8b9618ce4c3ffcf44430b0509bd9ad" + "bb41c9486af4503ad5df73837be5030c" ] ] ] \ No newline at end of file diff --git a/test/.hints/Vla.fst.hints b/test/.hints/Vla.fst.hints index cb2e75388..a1b8cb7f0 100644 --- a/test/.hints/Vla.fst.hints +++ b/test/.hints/Vla.fst.hints @@ -48,7 +48,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt32.v" ], 0, - "d5b1f937f342b1f2d38a03a899cc6725" + "bd843aabd7b153141d755de6702708b8" ], [ "Vla.main", @@ -65,7 +65,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "76cd64af9232d03cf4ea18e88ec92ee2" + "c1a529c8370f3426df39c8bfcf4053c0" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm1.fst.hints b/test/.hints/Wasm1.fst.hints index ec58c870b..68f242793 100644 --- a/test/.hints/Wasm1.fst.hints +++ b/test/.hints/Wasm1.fst.hints @@ -38,7 +38,7 @@ "typing_FStar.UInt.fits", "typing_FStar.UInt32.v" ], 0, - "9db6d2f982030b2d36d5f8bee6d1db16" + "b0ec12f934d790d0a7352facdcb64f0b" ], [ "Wasm1.maybe_true", @@ -59,7 +59,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "3cc80b7b79fcb8037d38cf508ae3b844" + "60a52dd24b1c3f98785853c3109a1604" ], [ "Wasm1.fact'", @@ -72,7 +72,7 @@ "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "8d0cadfffc80a507752ba2f2750a0363" + "1c22313ae408f78ccbc6fc009fda1e52" ], [ "Wasm1.minus", @@ -95,7 +95,7 @@ "typing_FStar.UInt32.v" ], 0, - "e5b967e753d6179253c6aad0ef70b65d" + "d6b4348c169b25ef66891813bbd24acc" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm10.fst.hints b/test/.hints/Wasm10.fst.hints index 440181c83..8c252eb89 100644 --- a/test/.hints/Wasm10.fst.hints +++ b/test/.hints/Wasm10.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "8fffcfbab1bafe3bd356ac72e9ee942d" + "f97fdda0f0fb9fb58acc627ae023b701" ], [ "Wasm10.b", @@ -40,7 +40,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "f3e96492389e717871deeeb278d65578" + "4ea5fd5747bb5fa025379789bd845a9d" ], [ "Wasm10.main", @@ -58,7 +58,7 @@ "typing_Wasm10.b" ], 0, - "f2fa9082b1c89c814a812b9765911c65" + "f6c0d0a06e8534ad4ecd28165a9705d7" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm2.fst.hints b/test/.hints/Wasm2.fst.hints index a6946f67e..cf6ae62cf 100644 --- a/test/.hints/Wasm2.fst.hints +++ b/test/.hints/Wasm2.fst.hints @@ -79,7 +79,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_Prims.pow2" ], 0, - "bd7b41c8d4770fc064e4f659708ad0d7" + "c6847f71b6567a422b3c59b7828f96d4" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm3.fst.hints b/test/.hints/Wasm3.fst.hints index 3099a9d9d..b7f752d69 100644 --- a/test/.hints/Wasm3.fst.hints +++ b/test/.hints/Wasm3.fst.hints @@ -64,7 +64,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "e4ca6552e4584a39ab26610246ca57cc" + "849a5c6421fce7105f8f29236ccb2b3e" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm4.fst.hints b/test/.hints/Wasm4.fst.hints index 07f0744a4..9f2287089 100644 --- a/test/.hints/Wasm4.fst.hints +++ b/test/.hints/Wasm4.fst.hints @@ -14,7 +14,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "c40583d1ecf0c93f3df8adfaa0770175" + "da3f451cb71253eb761b2dd3a90c263d" ], [ "Wasm4.test", @@ -27,7 +27,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "d0bddc262b6f00ef1df95faaa3705b0d" + "06c05209f5406a0e55933276c2c7ac2e" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm5.fst.hints b/test/.hints/Wasm5.fst.hints index 46e4a95e0..e110d4ad1 100644 --- a/test/.hints/Wasm5.fst.hints +++ b/test/.hints/Wasm5.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "01e6db7410c8779311c1f9a1eaf6d7bb" + "fda54fd361e36dfce43b3ca96afeb4d0" ], [ "Wasm5.y", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "633479db8d86e7f597bc9a5493616a44" + "66da4d54f606cf43552749c103fb70a9" ], [ "Wasm5.main", @@ -72,7 +72,7 @@ "typing_Wasm5.x" ], 0, - "56bad771ec8e3d9e6081bc9b477a5b8f" + "6078e604b4728f4f239f93454eb632b8" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm6.fst.hints b/test/.hints/Wasm6.fst.hints index a0699cbfa..981fbf7e1 100644 --- a/test/.hints/Wasm6.fst.hints +++ b/test/.hints/Wasm6.fst.hints @@ -14,7 +14,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "08b4e7b6ca23212a49a73b0766c1f9ea" + "3daf013f83519c7dd01cb1ffe0a3bf81" ], [ "Wasm6.snd", @@ -29,7 +29,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "69a32423b9cd495900171be544ddd6a9" + "9e8b33f0b960f623def3d38526ee7279" ], [ "Wasm6.main", @@ -97,7 +97,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null" ], 0, - "5d883385410f1d4edfe1d7ada10336c2" + "d1009c210b1f3c6f2bf29c0728517acc" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm7.fst.hints b/test/.hints/Wasm7.fst.hints index e637f7f18..1ebb7b4d7 100644 --- a/test/.hints/Wasm7.fst.hints +++ b/test/.hints/Wasm7.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "a56c2cd33707c415bcbffd50f966e27f" + "49b5d8a422a84f1a6f9a47be35efa9f0" ], [ "Wasm7.__proj__A__item___0", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_ec10ccf333cf39e2d779a27ff25f9f69" ], 0, - "1d758b35ca94b775e8d81bd8211cb3e8" + "c8227439c155b48bc3459717db62dec1" ], [ "Wasm7.__proj__A__item___1", @@ -38,7 +38,7 @@ "refinement_interpretation_Tm_refine_ec10ccf333cf39e2d779a27ff25f9f69" ], 0, - "3425d0d27823f134971cef6bd9871c1b" + "f98fcf94a9399f464202f6ba7e0f8838" ], [ "Wasm7.__proj__B__item___0", @@ -51,7 +51,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "574b8a85d47a10f58549f7a303fd6ad4" + "0556ec6fbc8dfaf2ffc3c742c92633b1" ], [ "Wasm7.__proj__B__item___1", @@ -64,7 +64,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "979ecd38b01e9c8b8538717aa4f87418" + "ddaef9df671157cbdeeabe2a4a2ef3bc" ], [ "Wasm7.__proj__B__item___2", @@ -77,7 +77,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "1ec2eb8f8fe952791a54d56299c47381" + "80a71b8753f9fdfbb75e43a0d7b47391" ], [ "Wasm7.v2", @@ -90,7 +90,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "9daa915f16288994f50b032494bd4d19" + "19545024bca1e1dae81e0a3f3aecaa62" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm8.fst.hints b/test/.hints/Wasm8.fst.hints index 744bbb2a2..6ef43b7b7 100644 --- a/test/.hints/Wasm8.fst.hints +++ b/test/.hints/Wasm8.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "1b295e6e2ad492cb6fbe206545270c8a" + "4669c6f552e66357caaf7fe4e9d1334e" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm9.fst.hints b/test/.hints/Wasm9.fst.hints index d3672e5e9..2ef1a0a84 100644 --- a/test/.hints/Wasm9.fst.hints +++ b/test/.hints/Wasm9.fst.hints @@ -81,7 +81,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "75bc15a3d65ef8952219c54489f5e1e9" + "218db1013d0ab075a2f56bc92e46df1f" ] ] ] \ No newline at end of file diff --git a/test/.hints/WasmTrap.fst.hints b/test/.hints/WasmTrap.fst.hints index f27d6bc8a..34ff34022 100644 --- a/test/.hints/WasmTrap.fst.hints +++ b/test/.hints/WasmTrap.fst.hints @@ -55,7 +55,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt32.v" ], 0, - "9c1d78235d4ec4be88b18d72d2afa6af" + "cb256565222ae770131f7d1b074add5e" ] ] ] \ No newline at end of file diff --git a/test/.hints/WildCard.fst.hints b/test/.hints/WildCard.fst.hints index 86c29f895..1f4d6910b 100644 --- a/test/.hints/WildCard.fst.hints +++ b/test/.hints/WildCard.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "2b92513c2cea353635c1f63c5e1c42d0" + "c5a4362eb99f4ef09bebb931a5561548" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wireguard.fst.hints b/test/.hints/Wireguard.fst.hints index 5af93248b..7779322f9 100644 --- a/test/.hints/Wireguard.fst.hints +++ b/test/.hints/Wireguard.fst.hints @@ -15,7 +15,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "48c9956f14b128e4c9a7784784214398" + "0c39d2a5beb25a7825df665896b41bb8" ], [ "Wireguard.peers_footprint", @@ -31,7 +31,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "6eb29b7a3a09d36d4165a1905de8f114" + "c94555fab81ef9d1264d3c18bd85da61" ], [ "Wireguard.peers_disjoint", @@ -47,7 +47,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "819bce70c674bb2bd0b3d7e71830b790" + "7c3efd5510d2949dd62c16c0a8ab9fa2" ], [ "Wireguard.peers_invariants", @@ -64,7 +64,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "2119b2b4369e7c8030dd847606a2ea79" + "266dfbcdb63d4d3f557c39521d34c1df" ], [ "Wireguard.peer_by_id", @@ -82,7 +82,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "36ec9346b0d5ceccbcb6c7e3996954c5" + "302776c3a2377e18a8ae347eb3a206f9" ], [ "Wireguard.peer_of_id_in_peers", @@ -102,7 +102,7 @@ "typing_LowStar.Lib.LinkedList.t" ], 0, - "113b9fc680590a982e995200a0531145" + "37e6c06ec40c455f44ae54393de2bc72" ], [ "Wireguard.peers_back", @@ -122,7 +122,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "ca57b02008bdec6e88ec6298de250f92" + "02e4e0dcd9c070887fa6633ba2bb5e0b" ], [ "Wireguard.invariant", @@ -140,7 +140,7 @@ "typing_Wireguard.__proj__Mkdevice__item__r" ], 0, - "6a549bb62f88b12d437fde38447615ea" + "5274f56996c863af7e1f4d440ea3ac7f" ], [ "Wireguard.peer_footprint_in", @@ -206,7 +206,7 @@ "typing_Wireguard.peer_footprint", "typing_Wireguard.peers_footprint" ], 0, - "4c8710232ad5685b8dba5a5b89536c5e" + "16f5043b76fe45abb2e4c0d3cf674e2a" ], [ "Wireguard.device_peers_footprint_in", @@ -215,7 +215,7 @@ 0, [ "@query", "equation_Wireguard.invariant" ], 0, - "e3deca51d9d64dd77b169ba777bb5204" + "bd3ee4a93064b7fa9d9b180c84eeb575" ], [ "Wireguard.frame_peers_back", @@ -291,7 +291,7 @@ "typing_Wireguard.__proj__Mkpeer__item__hs" ], 0, - "9765705be20b7b4b7325a65e233eef71" + "21bc821a9ad6e7af1072c65c800e0ef0" ], [ "Wireguard.frame_peers_invariants", @@ -377,7 +377,7 @@ "typing_Wireguard.peer_footprint" ], 0, - "5dfb7b9c4aa5d952ccec8de9cfa1d1af" + "b29eb33aac27f246cc0499a71969016b" ], [ "Wireguard.cell_by_id_is_peer_by_id", @@ -392,7 +392,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "67c9e60575b6b3e4459dfb7589dcbfa1" + "ab7d8ed70008e31269ba70fb16c98b3a" ], [ "Wireguard.cell_by_id_is_peer_by_id", @@ -501,7 +501,7 @@ "typing_Wireguard.cell_by_id", "typing_Wireguard.peer_by_id" ], 0, - "b3a40fa6f7ccb929143bf12d59cb2016" + "cc620457f6a982fce3744fb60ccf8366" ], [ "Wireguard.peer_by_id_invariant", @@ -536,7 +536,7 @@ "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons" ], 0, - "6b9d17f53b08aa2b331e03bf09c2a936" + "b75c46a039ca5ae31f95f9fd39e43cd3" ], [ "Wireguard.frame_invariant", @@ -637,7 +637,7 @@ "typing_Wireguard.peers_footprint" ], 0, - "f9225e7a42b95e25dcd893cb2fd57e97" + "a56ff32199c7360ce6a67e4067051141" ], [ "Wireguard.create_in", @@ -774,7 +774,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions" ], 0, - "feaa43693d69ba625fd92dbccff8e3b2" + "4833041df023b53fbd7f32f9f18a4299" ], [ "Wireguard.free_peer_list", @@ -884,7 +884,7 @@ "typing_Wireguard.peer_footprint" ], 0, - "d78706c3c84e485696d1c1c594d205a3" + "4f5f73d72683f26aea68686c14cb0013" ], [ "Wireguard.free_", @@ -950,7 +950,7 @@ "typing_Wireguard.__proj__Mkdevice__item__r_peers_payload" ], 0, - "f1b35e80cd1532f2ea061b93022f14eb" + "c163d10deff1c20694d3ffe98f81cbcf" ], [ "Wireguard.insert_peer", @@ -959,7 +959,7 @@ 0, [ "@query" ], 0, - "5715cdd9c3335729b7f2dd4dc2cec2d0" + "ed6433f5d9b9cf666bda9d2ec31450f0" ], [ "Wireguard.insert_peer", @@ -1155,7 +1155,7 @@ "typing_Wireguard.peers_footprint" ], 0, - "1b242cc0a64de62890462d8af87558a4" + "947a15de653ab68f670132718003a76d" ], [ "Wireguard.find_peer_by_id_", @@ -1254,7 +1254,7 @@ "typing_Wireguard.cell_by_id" ], 0, - "acd3cf27cfb48e877080f5c165cbfd4a" + "8df1e67673462ed2e14ef6d82061ae36" ], [ "Wireguard.find_peer_by_id", @@ -1280,7 +1280,7 @@ "typing_Wireguard.__proj__Mkdevice__item__peers" ], 0, - "a667aa4349d43e2817515e8271d8b637" + "b1a6d9d5d722b85a4c0b4339d531ecd3" ], [ "Wireguard.link_peer_by_id", @@ -1390,7 +1390,7 @@ "typing_Wireguard.peer_by_id", "typing_Wireguard.peers_footprint" ], 0, - "ce26e41c076ab2cc49e981e139222177" + "17dde4ae0047e15833c7f21d4d690b8e" ], [ "Wireguard.main", @@ -1595,7 +1595,7 @@ "typing_Wireguard.peer_by_id", "typing_Wireguard.peers_footprint" ], 0, - "dd1b2362262b03d731d378bb08145db5" + "f59a1a4d0f2f11747c7d603ccfa5a11e" ] ] ] \ No newline at end of file diff --git a/test/Makefile b/test/Makefile index b36e0b32d..5919439fd 100644 --- a/test/Makefile +++ b/test/Makefile @@ -110,7 +110,7 @@ $(OUTPUT_DIR)/Structs2.exe: EXTRA = -wasm -d force-c wasm-stubs.c $(OUTPUT_DIR)/ML16.exe: EXTRA = ml16-native.c $(OUTPUT_DIR)/Scope.exe: EXTRA = -ccopt -O3 $(OUTPUT_DIR)/HigherOrder.exe: EXTRA = -warn-error +9 -$(OUTPUT_DIR)/C89.exe: EXTRA = -ccopts -Wno-long-long,-Wno-format,-pedantic -fc89 +$(OUTPUT_DIR)/C89.exe: EXTRA = -ccopts -Wno-long-long,-Wno-format,-pedantic,-Wno-c99-extensions -fc89 $(OUTPUT_DIR)/Debug.exe: EXTRA = -d c-calls $(OUTPUT_DIR)/Server.exe: EXTRA = main-Server.c helpers-Server.c $(OUTPUT_DIR)/StringLit.exe: EXTRA = -add-include '"kremlin/internal/compat.h"' diff --git a/test/UnusedPoly.fst b/test/UnusedPoly.fst new file mode 100644 index 000000000..405345ae4 --- /dev/null +++ b/test/UnusedPoly.fst @@ -0,0 +1,3 @@ +module UnusedPoly + +let main (a: Type) () = 0l