From bdf06956e6ee025d4819bf2f8cc92651e572ad85 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Tue, 13 Aug 2024 08:30:59 -0700 Subject: [PATCH] hints, minor pretty-printing fix --- krmllib/dist/generic/FStar_Issue.h | 4 +- krmllib/dist/generic/FStar_Monotonic_Heap.h | 12 +- krmllib/hints/C.Endianness.fst.hints | 44 +++--- krmllib/hints/C.Failure.fst.hints | 4 +- krmllib/hints/C.Loops.fst.hints | 78 +++++------ krmllib/hints/C.String.fst.hints | 18 +-- krmllib/hints/C.String.fsti.hints | 10 +- krmllib/hints/C.fst.hints | 2 +- krmllib/hints/FStar.Krml.Endianness.fst.hints | 130 +++++++++--------- krmllib/hints/LowStar.Lib.AssocList.fst.hints | 26 ++-- .../hints/LowStar.Lib.LinkedList.fst.hints | 58 ++++---- .../hints/LowStar.Lib.LinkedList2.fst.hints | 42 +++--- krmllib/hints/TestLib.fsti.hints | 4 +- krmllib/hints/WasmSupport.fst.hints | 6 +- lib/PrintC.ml | 7 +- lib/Simplify.ml | 1 + test/.hints/Abbrev.fst.hints | 2 +- test/.hints/AbstractStruct.fst.hints | 4 +- test/.hints/AbstractStruct2.fst.hints | 4 +- test/.hints/Attributes.fst.hints | 2 +- test/.hints/BadMatch.fst.hints | 4 +- test/.hints/BlitNull.fst.hints | 2 +- test/.hints/C.Nullity.fsti.hints | 4 +- test/.hints/C89.fst.hints | 30 ++-- test/.hints/CheckedInt.fst.hints | 6 +- test/.hints/ColoredRegion.fst.hints | 2 +- test/.hints/Comment.fst.hints | 2 +- test/.hints/ConstBuffer.fst.hints | 4 +- test/.hints/Ctypes1.fst.hints | 4 +- test/.hints/Ctypes2.fst.hints | 2 +- test/.hints/Ctypes3.fst.hints | 2 +- test/.hints/Ctypes4.fst.hints | 36 ++--- test/.hints/CustomEq.fst.hints | 24 ++-- test/.hints/DataTypes.fst.hints | 32 ++--- test/.hints/DataTypesEq.fst.hints | 10 +- test/.hints/DataTypesSimple.fst.hints | 6 +- test/.hints/DepPair.fst.hints | 2 +- test/.hints/Deref.fst.hints | 8 +- test/.hints/Endianness.fst.hints | 2 +- test/.hints/EqB.fst.hints | 2 +- test/.hints/EtaStruct.fst.hints | 6 +- test/.hints/ExitCode.fst.hints | 2 +- test/.hints/Failwith.fst.hints | 4 +- test/.hints/Fill.fst.hints | 8 +- test/.hints/Flat.fst.hints | 4 +- test/.hints/FunPtr.fst.hints | 4 +- test/.hints/FunctionalEncoding.fst.hints | 2 +- test/.hints/GcTypes.fst.hints | 4 +- test/.hints/Ghost1.fst.hints | 4 +- test/.hints/HigherOrder.fst.hints | 2 +- test/.hints/HigherOrder2.fst.hints | 6 +- test/.hints/HigherOrder3.fst.hints | 6 +- test/.hints/HigherOrder4.fst.hints | 6 +- test/.hints/HigherOrder5.fst.hints | 8 +- test/.hints/HigherOrder6.fst.hints | 8 +- test/.hints/Hoisting.fst.hints | 4 +- test/.hints/IfDef.fst.hints | 10 +- test/.hints/IfDefKrml.fst.hints | 2 +- test/.hints/IfThenElse.fst.hints | 4 +- test/.hints/InitializerLists.fst.hints | 10 +- test/.hints/Inline.fst.hints | 4 +- test/.hints/InlineNoExtract.fst.hints | 4 +- test/.hints/InlineTest.fst.hints | 8 +- test/.hints/Intro.fst.hints | 2 +- test/.hints/Layered.fst.hints | 28 ++-- test/.hints/Library.fst.hints | 2 +- test/.hints/LinkedList1.fst.hints | 58 ++++---- test/.hints/LinkedList2.fst.hints | 46 +++---- test/.hints/LinkedList3.fst.hints | 46 +++---- test/.hints/LinkedList4.fst.hints | 38 ++--- test/.hints/Literal.fst.hints | 2 +- test/.hints/Loops.fst.hints | 18 +-- test/.hints/ML16.fst.hints | 6 +- test/.hints/Macro.fst.hints | 2 +- test/.hints/MallocFree.fst.hints | 2 +- test/.hints/MemCpy.fst.hints | 8 +- test/.hints/MemCpyModel.fst.hints | 4 +- test/.hints/Mini.fst.hints | 4 +- test/.hints/MonomorphizationCrash.fst.hints | 4 +- test/.hints/MutRec.fst.hints | 10 +- test/.hints/NameCollisionHelper.fst.hints | 2 +- test/.hints/NoExtract.fst.hints | 4 +- test/.hints/NoShadow.fst.hints | 10 +- test/.hints/Null.fst.hints | 4 +- test/.hints/OptimizedOption.fst.hints | 2 +- test/.hints/ParamAbbrev.fst.hints | 8 +- test/.hints/Parameterized.fst.hints | 6 +- test/.hints/PatternAny.fst.hints | 2 +- test/.hints/PolyComp.fst.hints | 12 +- test/.hints/Polymorphic.fst.hints | 4 +- test/.hints/Printf.fst.hints | 2 +- test/.hints/Private.fst.hints | 2 +- test/.hints/PrivateInclude1.fst.hints | 2 +- test/.hints/PrivateInclude2.fst.hints | 2 +- test/.hints/PushPop.fst.hints | 4 +- test/.hints/RecordTypingLimitation.fst.hints | 2 +- test/.hints/Recursive.fst.hints | 4 +- test/.hints/RecursivePoly.fst.hints | 8 +- test/.hints/Renaming.fst.hints | 4 +- test/.hints/RingBuffer.fst.hints | 44 +++--- test/.hints/Rust1.fst.hints | 14 +- test/.hints/Scope.fst.hints | 4 +- test/.hints/Server.fst.hints | 20 +-- test/.hints/Shift.fst.hints | 4 +- test/.hints/SimpleWasm.fst.hints | 4 +- test/.hints/StaticHeaderLib.fst.hints | 6 +- test/.hints/StaticHeaderLib.fsti.hints | 4 +- test/.hints/StringLit.fst.hints | 8 +- test/.hints/Strlen.fst.hints | 2 +- test/.hints/Structs.fst.hints | 6 +- test/.hints/Structs2.fst.hints | 10 +- test/.hints/Substitute.fst.hints | 4 +- test/.hints/TailCalls.fst.hints | 2 +- test/.hints/TailCalls2.fst.hints | 2 +- test/.hints/TestAlloca.fst.hints | 4 +- test/.hints/TopLevelArray.fst.hints | 10 +- test/.hints/TotalLoops.fst.hints | 6 +- test/.hints/Tuples.fst.hints | 2 +- test/.hints/UBuffer.fst.hints | 6 +- test/.hints/Underspec.fst.hints | 4 +- test/.hints/Unsound.fst.hints | 6 +- test/.hints/UnusedParameter.fst.hints | 4 +- test/.hints/Unused_A.fst.hints | 2 +- test/.hints/Unused_B.fst.hints | 2 +- test/.hints/Uu.fst.hints | 2 +- test/.hints/VariableMerge.fst.hints | 10 +- test/.hints/Verbatim.fst.hints | 2 +- test/.hints/Vla.fst.hints | 4 +- test/.hints/Wasm1.fst.hints | 8 +- test/.hints/Wasm10.fst.hints | 6 +- test/.hints/Wasm2.fst.hints | 2 +- test/.hints/Wasm3.fst.hints | 2 +- test/.hints/Wasm4.fst.hints | 4 +- test/.hints/Wasm5.fst.hints | 6 +- test/.hints/Wasm6.fst.hints | 6 +- test/.hints/Wasm7.fst.hints | 14 +- test/.hints/Wasm8.fst.hints | 2 +- test/.hints/Wasm9.fst.hints | 2 +- test/.hints/WasmTrap.fst.hints | 2 +- test/.hints/WildCard.fst.hints | 2 +- test/.hints/Wireguard.fst.hints | 50 +++---- 141 files changed, 717 insertions(+), 713 deletions(-) diff --git a/krmllib/dist/generic/FStar_Issue.h b/krmllib/dist/generic/FStar_Issue.h index dd34a65c..ed9e61b9 100644 --- a/krmllib/dist/generic/FStar_Issue.h +++ b/krmllib/dist/generic/FStar_Issue.h @@ -41,7 +41,7 @@ FStar_Pervasives_Native_option__krml_checked_int_t; extern FStar_Pervasives_Native_option__krml_checked_int_t FStar_Issue_number_of_issue(FStar_Issue_issue i); -extern FStar_Pervasives_Native_option__FStar_Range_range +extern FStar_Pervasives_Native_option__FStar_Sealed_sealed_FStar_Range___range FStar_Issue_range_of_issue(FStar_Issue_issue i); extern Prims_list__Prims_string *FStar_Issue_context_of_issue(FStar_Issue_issue i); @@ -52,7 +52,7 @@ extern FStar_Issue_issue FStar_Issue_mk_issue_doc( Prims_string i, Prims_list__FStar_Pprint_document *msg, - FStar_Pervasives_Native_option__FStar_Range_range range, + FStar_Pervasives_Native_option__FStar_Sealed_sealed_FStar_Range___range range, FStar_Pervasives_Native_option__krml_checked_int_t number, Prims_list__Prims_string *ctx ); diff --git a/krmllib/dist/generic/FStar_Monotonic_Heap.h b/krmllib/dist/generic/FStar_Monotonic_Heap.h index 3e239c28..5a117951 100644 --- a/krmllib/dist/generic/FStar_Monotonic_Heap.h +++ b/krmllib/dist/generic/FStar_Monotonic_Heap.h @@ -15,26 +15,26 @@ typedef void *FStar_Monotonic_Heap_tset; -typedef struct FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any_s +typedef struct FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any_s { FStar_Pervasives_Native_option__Prims_string_tags _2; bool _3; void *_4; } -FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any; +FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any; typedef struct -FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option_____bool_any_s +FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any_s { FStar_Pervasives_Native_option__Prims_string_tags tag; - FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option_____bool_any v; + FStar_Pervasives_dtuple4_____FStar_Pervasives_Native_option____bool_any v; } -FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option_____bool_any; +FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any; typedef struct FStar_Monotonic_Heap_heap_rec_s { krml_checked_int_t next_addr; - FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option_____bool_any + FStar_Pervasives_Native_option__FStar_Pervasives_dtuple4____FStar_Pervasives_Native_option____bool_any (*memory)(krml_checked_int_t x0); } FStar_Monotonic_Heap_heap_rec; diff --git a/krmllib/hints/C.Endianness.fst.hints b/krmllib/hints/C.Endianness.fst.hints index a178a7b2..f75a01f7 100644 --- a/krmllib/hints/C.Endianness.fst.hints +++ b/krmllib/hints/C.Endianness.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "cfdaef4aad628928249995f7219f9963" + "8dc510924f8b7fd225c293fc781b2eee" ], [ "C.Endianness.load16_le", @@ -17,7 +17,7 @@ 1, [ "@query" ], 0, - "cb3bf014be54d76e289015af59f74f2e" + "af39f10aa1af6da243f3d4c346c94645" ], [ "C.Endianness.store16_be", @@ -26,7 +26,7 @@ 1, [ "@query" ], 0, - "1be674a60367bde13a05c22221903d8c" + "784f577a3d2cd52b449fcc3f2d1427aa" ], [ "C.Endianness.load16_be", @@ -35,7 +35,7 @@ 1, [ "@query" ], 0, - "09f2b613fc2d5f8c38e83958544efd6e" + "ef780de93d526866b76fe9d1d83ba17d" ], [ "C.Endianness.store32_le", @@ -44,7 +44,7 @@ 1, [ "@query" ], 0, - "30267a364b1fcc2f6d543f977525b9af" + "04caeb03b1b5d06a134a2c5a821cccb2" ], [ "C.Endianness.load32_le", @@ -53,7 +53,7 @@ 1, [ "@query" ], 0, - "9fda6c88065a6ce618658370dad31fbe" + "9e851a45ad5a7970502f001441333713" ], [ "C.Endianness.store32_be", @@ -62,7 +62,7 @@ 1, [ "@query" ], 0, - "25f7a1c7c57249a07a8c5ebb17a43b69" + "2678b758b13755f6283fd5b75f0c3d81" ], [ "C.Endianness.load32_be", @@ -71,7 +71,7 @@ 1, [ "@query" ], 0, - "0056aa616ef324f6d521e2a6808ca94c" + "85dd5031c0d5a5aad56cda647d643030" ], [ "C.Endianness.store64_le", @@ -80,7 +80,7 @@ 1, [ "@query" ], 0, - "ae1c75f1b5fd78b96449584801583c85" + "a77453adea1912293bd578063141aa0a" ], [ "C.Endianness.load64_le", @@ -89,7 +89,7 @@ 1, [ "@query" ], 0, - "36c9f8068c1966b0c2b150b3b7614e44" + "756bd5b952aa7ae2b5237520a328b857" ], [ "C.Endianness.load64_be", @@ -98,7 +98,7 @@ 1, [ "@query" ], 0, - "7b0bef3247da2aa554312d69998f22cb" + "ba24c98a32b7c358e7603be5e1301423" ], [ "C.Endianness.store64_be", @@ -107,7 +107,7 @@ 1, [ "@query" ], 0, - "a5e63f72df21f65e578b13d5b489bd2e" + "43185c40a2da7391cc99fbe0a38b32f1" ], [ "C.Endianness.load128_le", @@ -119,7 +119,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "ad28d00b986612134ca86871e61ea920" + "c8a29b96abf4c1eec62ce3b1196df4c1" ], [ "C.Endianness.store128_le", @@ -131,7 +131,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "fc46e88fb657187ca8e859c0d7084838" + "e351ce82ea2ef30e3cea5ad2bb73271a" ], [ "C.Endianness.load128_be", @@ -143,7 +143,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "9059caacd412964a44e045795e6cc317" + "cafc5490d5ff1a7c92619986448dd9b7" ], [ "C.Endianness.store128_be", @@ -155,7 +155,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "78e72aeabaa692af633abd6996fa2d23" + "d7ad47f16604a0b02a8c739442b9f5b8" ], [ "C.Endianness.index_32_be", @@ -217,7 +217,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "3b2d465a6b8c84a1fca2792929938f29" + "4b6539306b3e8f230ac874d9ba0f1672" ], [ "C.Endianness.index_32_le", @@ -274,7 +274,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "02a35c3d33a3ec7eeab0c153f01de0d8" + "e9d8da99ba7c0569816f5b1107631b9e" ], [ "C.Endianness.index_64_be", @@ -330,7 +330,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "0d5d02e8dd2e7da7ce01147e8a2d6588" + "becc67d1ca963120edeb9ef0d9590183" ], [ "C.Endianness.index_64_le", @@ -390,7 +390,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "304c21a3ced4fa125993d8c42013bc0a" + "23fb97ef5f1342a308ad91ca4444efb5" ], [ "C.Endianness.interval_4_disjoint", @@ -407,7 +407,7 @@ "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "4cf0cfee91cd3d51a66d2f32deca8b29" + "156eda0d0957c0c424aca75efad85725" ], [ "C.Endianness.upd_32_be", @@ -502,7 +502,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "f206be4f567e7a2adacc5b679a156083" + "18e9f0061e85eb2d74d647b66d58690e" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.Failure.fst.hints b/krmllib/hints/C.Failure.fst.hints index bf27c974..e3045dc9 100644 --- a/krmllib/hints/C.Failure.fst.hints +++ b/krmllib/hints/C.Failure.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "75256bd25d1d91db5a2588b3b1d44492" + "b390c0f39d04be1c03c24b79ca2a080e" ], [ "C.Failure.failwith", @@ -29,7 +29,7 @@ 1, [ "@query" ], 0, - "378d9a902e6d36111b3bf99aed5a01f8" + "64217e022e6791b98590da1d9987ddb9" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.Loops.fst.hints b/krmllib/hints/C.Loops.fst.hints index 2c85dd9a..5cbfe9a4 100644 --- a/krmllib/hints/C.Loops.fst.hints +++ b/krmllib/hints/C.Loops.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.UInt32.v" ], 0, - "9586864fd99336d29746e5444041df0e" + "35ff02a9fa781447cb9fd119eff6ed5d" ], [ "C.Loops.for", @@ -60,7 +60,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "e57baf14df3e814111f243b768e897d5" + "515834d02c6144689006e980d2cb8143" ], [ "C.Loops.for", @@ -80,7 +80,7 @@ "typing_FStar.UInt32.v" ], 0, - "f482909c9d4ff4206324e4a02e4ee0c0" + "abd5979b46cf61c370855e257907a21e" ], [ "C.Loops.for64", @@ -101,7 +101,7 @@ "typing_FStar.UInt64.v" ], 0, - "c6ad65c80ef16033011f5e1cf8603d3d" + "40dea0818ed51752e3f14504b7c95935" ], [ "C.Loops.for64", @@ -141,7 +141,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt64.v" ], 0, - "f688d5cbb2e48b8fab14e58b6599c0cc" + "ff57bc5c3d54a944ba67bb99b72b6421" ], [ "C.Loops.for64", @@ -161,7 +161,7 @@ "typing_FStar.UInt64.v" ], 0, - "4ecab2ba184cd31e9dc273f81b64bdea" + "5d5d4e6cdffaa9d8c97edcdbc6644f0a" ], [ "C.Loops.reverse_for", @@ -183,7 +183,7 @@ "typing_FStar.UInt32.v" ], 0, - "b947df3ea7c45c4d8ffdf4a0af43e7fd" + "572adba105c2ae44d7acd993ff52b612" ], [ "C.Loops.reverse_for", @@ -224,7 +224,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "3c1161a58f41e403a6637f66187e7c33" + "369605e1b023b9861665f1e104849612" ], [ "C.Loops.reverse_for", @@ -246,7 +246,7 @@ "typing_FStar.UInt32.v" ], 0, - "23bd58a3b6d402cf0147f3cdb5bed0da" + "e325577831563dfdcfbf889dfe6a7dad" ], [ "C.Loops.interruptible_for", @@ -266,7 +266,7 @@ "typing_FStar.UInt32.v" ], 0, - "ed764bf9f547afc9e6416dff1a2ca898" + "454a743d52fcb1db7821bfc10394c9b8" ], [ "C.Loops.interruptible_for", @@ -310,7 +310,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "aad8233c12ebca4ea3bf699340326278" + "4ca2a6fc7d3350df602e6d85aba14c7c" ], [ "C.Loops.interruptible_for", @@ -330,7 +330,7 @@ "typing_FStar.UInt32.v" ], 0, - "df3ace88925fc3021633308287dd9032" + "40856fa5476237a5fe41d11b5e2ff5ba" ], [ "C.Loops.do_while", @@ -355,7 +355,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "3b4597d90945e88a92cbea28458784b7" + "21be47ffcb9f316196c60a5e0eafafc2" ], [ "C.Loops.while", @@ -369,7 +369,7 @@ "refinement_interpretation_Tm_refine_b16bf82b210653a34e4d7322fab91ffb" ], 0, - "289bab31e610275175fac08781264e3c" + "4a2846235499872f3dceba6104f297d2" ], [ "C.Loops.interruptible_reverse_for", @@ -391,7 +391,7 @@ "typing_FStar.UInt32.v" ], 0, - "f567662764d9e586580b96f607334041" + "812de286f477999b896333c3540851ac" ], [ "C.Loops.interruptible_reverse_for", @@ -436,7 +436,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "c3ef2d97aaec56feaeba04fd9cfd1893" + "5993bd9524678943465a88dbb23e30e5" ], [ "C.Loops.interruptible_reverse_for", @@ -458,7 +458,7 @@ "typing_FStar.UInt32.v" ], 0, - "d12c364490e163492ab7f19ced0253f1" + "c0ae2c7b57ffbd6c1620049eeaa99b2b" ], [ "C.Loops.map", @@ -467,7 +467,7 @@ 1, [ "@query" ], 0, - "9d4f87f895c2c8a14b4612879c29665c" + "7cc923b9ee7e33f6e1f0fdc5589a6163" ], [ "C.Loops.map", @@ -514,7 +514,7 @@ "typing_Spec.Loops.seq_map" ], 0, - "034c8db7ae3ee923bcef4730fded0c75" + "0f061991b6948400eaa59cbd91196acc" ], [ "C.Loops.map", @@ -523,7 +523,7 @@ 1, [ "@query" ], 0, - "55a83fac920df87c1b316bbada08ba28" + "83a484e4700dfd83a7f2d70918bd601c" ], [ "C.Loops.map2", @@ -538,7 +538,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "82720701b9e7aea4fd3d5a5e2bbac2ea" + "b92c682e4cf1e4b25246bc16366df632" ], [ "C.Loops.map2", @@ -587,7 +587,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "35958be347378923aa30f98660ac6541" + "6090402a40d1274f94582860dea62efb" ], [ "C.Loops.map2", @@ -596,7 +596,7 @@ 1, [ "@query" ], 0, - "9ce05b8c2dfbbdf65437c279039d6603" + "aab4a7426410e36519e4fd8910facc8e" ], [ "C.Loops.in_place_map", @@ -605,7 +605,7 @@ 1, [ "@query" ], 0, - "7fb7c55c655c672ff69b30613a5a58b9" + "18050ad6144e29942dc58b95e3122950" ], [ "C.Loops.in_place_map", @@ -650,7 +650,7 @@ "typing_Spec.Loops.seq_map" ], 0, - "56e2a91655cf247a77c1c5736dab88e9" + "578baf6683252e5cea8d692fb8a3b19b" ], [ "C.Loops.in_place_map", @@ -659,7 +659,7 @@ 1, [ "@query" ], 0, - "577fe30c37b85fb7efad2a3a324160c4" + "8f1ec95f1820e54797853cf866cacd5b" ], [ "C.Loops.in_place_map2", @@ -674,7 +674,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "2520937cecdd3bf6d58459ea522759b1" + "1c129e09794734f9f045eb60cec226d1" ], [ "C.Loops.in_place_map2", @@ -721,7 +721,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "f819b48fb07299e7bbb04950ff288e10" + "00ee345d2c5416a1a987c6a474f76251" ], [ "C.Loops.in_place_map2", @@ -730,7 +730,7 @@ 1, [ "@query" ], 0, - "9db997f86a94ed9a7c5d194412b16467" + "7aecdb30a7db73f3bd275ca5373b77f1" ], [ "C.Loops.repeat", @@ -753,7 +753,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "78d2e6dd90f761b9ff1c98725d1506aa" + "b75138414897836b7a175eff56e33205" ], [ "C.Loops.repeat", @@ -786,7 +786,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "5f84c76894cc92f65456b7ada0328175" + "d2ec962fcce3a30a1ceadb7c7fc36a52" ], [ "C.Loops.repeat", @@ -804,7 +804,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "c871a4afa4db99157dc8b8d923c82060" + "400748a561a77f2216fa57a5d778d179" ], [ "C.Loops.repeat_range_body_impl", @@ -823,7 +823,7 @@ "typing_FStar.UInt32.v" ], 0, - "9aa1033a77c51153a25d51d6008241ce" + "1ff9e705de7fbe045663ccfed62a55c9" ], [ "C.Loops.repeat_range_body_impl", @@ -837,7 +837,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "ddd856e3ab39ff4ea25de153ddb1ed45" + "17e010e70f17218381d98ef436b3e3db" ], [ "C.Loops.repeat_range", @@ -856,7 +856,7 @@ "typing_FStar.UInt32.v" ], 0, - "aa16c87e721affaa1af67a7daaf762e0" + "751985651769bb8d74f4623f66ed7594" ], [ "C.Loops.repeat_range", @@ -881,7 +881,7 @@ "typing_FStar.UInt32.v" ], 0, - "13d65a19f15d6e756f29a53ee8561187" + "45e8eeba288d46916b7a7b0fd564f3c5" ], [ "C.Loops.repeat_range", @@ -895,7 +895,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "e2e058a384f2309a96d232c463f5a2ec" + "6f88eb83131db9b38aab194a6607dd8b" ], [ "C.Loops.total_while_gen", @@ -908,7 +908,7 @@ "binder_x_245a4248f315846e90b81e2d076a282b_6", "bool_inversion" ], 0, - "671133c8d5fb5767bf58d5e2618efabd" + "d0af0202ac95fa0a21ad998403da6272" ], [ "C.Loops.total_while", @@ -927,7 +927,7 @@ "well-founded-ordering-on-nat" ], 0, - "0d714ffc63ae803ade1bd78c1b03df7a" + "c1276fee1e75efb2241bd2f3f7bcc6fb" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.String.fst.hints b/krmllib/hints/C.String.fst.hints index 9b783a43..48132c1b 100644 --- a/krmllib/hints/C.String.fst.hints +++ b/krmllib/hints/C.String.fst.hints @@ -11,7 +11,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "92641bd010bea2c31a6a159c7d1cfb02" + "4f4c39ee984b3b39637f903b307c0dd8" ], [ "C.String.well_formed", @@ -23,7 +23,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "b1315fb7c107453d18e232d7d63b9426" + "67d23301d37ce7f46b3771c9896d9248" ], [ "C.String.t", @@ -35,7 +35,7 @@ "lemma_FStar.Seq.Base.hasEq_lemma" ], 0, - "37ee92da2eb6f46c7100b0b354704955" + "78af7551e268b972b6b308a5e05ca1c3" ], [ "C.String.length", @@ -50,7 +50,7 @@ "refinement_interpretation_Tm_refine_ed6e8a85e123e1e628ba0dad885f3031" ], 0, - "5d9ab71cd8531b26f3122e4afd360286" + "ef164c2cf246a8335ee4c2690d662848" ], [ "C.String.get", @@ -66,7 +66,7 @@ "refinement_interpretation_Tm_refine_dfcb8c150fd42ce38050af33905be19c" ], 0, - "d292420db14a178390d6a648bf520fbe" + "8bc1bb9cda12c0b7eacd2709e58036f6" ], [ "C.String.get", @@ -85,7 +85,7 @@ "typing_FStar.UInt32.v" ], 0, - "9281048051009ee7abcf41f69a062233" + "f878250aed55eeeba1fc476580770d99" ], [ "C.String.nonzero_is_lt", @@ -98,7 +98,7 @@ "fuel_guarded_inversion_C.String.t" ], 0, - "eeffe9f905b9fe8d3faea0eece2d34ec" + "9a4c022e340f86c98619747979931095" ], [ "C.String.nonzero_is_lt", @@ -119,7 +119,7 @@ "typing_FStar.UInt32.v" ], 0, - "34673f0d8b17302c46025374dd256dd7" + "3a684703021af27508dff6a25e2451d4" ], [ "C.String.memcpy", @@ -133,7 +133,7 @@ "typing_FStar.UInt8.t" ], 0, - "e7d3ba6f99e02c559a2c7dd11568ddfb" + "b50430f9ab1638e1673e53005755a7b6" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.String.fsti.hints b/krmllib/hints/C.String.fsti.hints index af6cb8a0..f6b6c8b2 100644 --- a/krmllib/hints/C.String.fsti.hints +++ b/krmllib/hints/C.String.fsti.hints @@ -11,7 +11,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "f8870333d9d242de95428ed9b7c39446" + "78c9dfbe8c789fe9be7d077e20b88a5b" ], [ "C.String.well_formed", @@ -23,7 +23,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "b2921a58c5ccf5f02a28629238fd8bf5" + "2aa3f9674ecc2972d706e8b2e9d89bfd" ], [ "C.String.get", @@ -39,7 +39,7 @@ "refinement_interpretation_Tm_refine_dfcb8c150fd42ce38050af33905be19c" ], 0, - "f1d396317bfb3497b7af8614522bdf23" + "9587f57edfbec578ad644246966159e8" ], [ "C.String.nonzero_is_lt", @@ -52,7 +52,7 @@ "typing_C.String.length" ], 0, - "721b6fecaaf220a02713b90ef6263270" + "7a45f98844d85973d875a94d92629e2c" ], [ "C.String.memcpy", @@ -66,7 +66,7 @@ "typing_FStar.UInt8.t" ], 0, - "7307f66c2f4b282adfb4460fa7cb719b" + "f8f3eca1717137088f0660feef326d66" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/C.fst.hints b/krmllib/hints/C.fst.hints index 36c690a9..6c5ae978 100644 --- a/krmllib/hints/C.fst.hints +++ b/krmllib/hints/C.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query", "assumption_C.HasEq_char" ], 0, - "5cd8132a85b172f37757d1ef57582411" + "9e32311070b1850dc9baeda961e4d90f" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/FStar.Krml.Endianness.fst.hints b/krmllib/hints/FStar.Krml.Endianness.fst.hints index e1fbfc61..73bc1dae 100644 --- a/krmllib/hints/FStar.Krml.Endianness.fst.hints +++ b/krmllib/hints/FStar.Krml.Endianness.fst.hints @@ -32,7 +32,7 @@ "well-founded-ordering-on-nat" ], 0, - "c79f4364832152c9f7b11017207a91b2" + "94d83e79333816e7159f3d2a7edb577b" ], [ "FStar.Krml.Endianness.be_to_n", @@ -65,7 +65,7 @@ "well-founded-ordering-on-nat" ], 0, - "1dc8a4c08b9f7db049e8f28b2a6b656e" + "d320e0eb0e0e96c644fcfe95131aba8f" ], [ "FStar.Krml.Endianness.lemma_euclidean_division", @@ -77,7 +77,7 @@ "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0" ], 0, - "7dd71593cbb70fbb9176d146d3612674" + "0a5fbfb35d62cb6e2b85c88f8726675b" ], [ "FStar.Krml.Endianness.lemma_factorise", @@ -90,7 +90,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "946d7f08644b3c377e26ec17819716dc" + "3d4c7c3d1adea19190ea710f4dd9d88d" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -107,7 +107,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "0f909451fefd446a4cbe27017afeaaf6" + "2e4bf6c60f726a9bb2fe4f0fb3a1b46c" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -149,7 +149,7 @@ "typing_Prims.pow2", "well-founded-ordering-on-nat" ], 0, - "50304ccc19f157bc2f1795622ef6cf57" + "4567290e07da70ad366666e575cf8ec7" ], [ "FStar.Krml.Endianness.lemma_le_to_n_is_bounded", @@ -167,7 +167,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "865c2a7e00d846de760d6445a1b92b93" + "a52751f905528623487fca288cfc1e33" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -184,7 +184,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "50295069f9ce19f8cf6a7ee444ce97ae" + "20420abba210fec0e4eeffbe6a0bee89" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -223,7 +223,7 @@ "typing_Prims.pow2", "well-founded-ordering-on-nat" ], 0, - "862f16fcfc630d37df6d4625c00ec977" + "4a02b5fa3d584b1467efbfe82f2edec8" ], [ "FStar.Krml.Endianness.lemma_be_to_n_is_bounded", @@ -241,7 +241,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "d5764b4910d8d996ba1c459edc66adde" + "7d5a03a4aa073fbb12e57f409c44a502" ], [ "FStar.Krml.Endianness.n_to_le", @@ -260,7 +260,7 @@ "typing_FStar.UInt32.v" ], 0, - "5178d1a9011fc814899617016b99ab1c" + "9cbb259bd98f55ababebca5990008cbc" ], [ "FStar.Krml.Endianness.n_to_le", @@ -322,7 +322,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "2087f83642e68213175152de9c8e6828" + "f696b653b690bf71bfcfd24be0bc3f9b" ], [ "FStar.Krml.Endianness.n_to_le", @@ -341,7 +341,7 @@ "typing_FStar.UInt32.v" ], 0, - "bbec1c4ee4cc447fbae9acabfc813fa5" + "59db08d8bc1e664423cb4fa664a3fb03" ], [ "FStar.Krml.Endianness.n_to_be", @@ -360,7 +360,7 @@ "typing_FStar.UInt32.v" ], 0, - "1e6586619c2239a34a7e0d3f42de77ff" + "6099a994f7e2186c4eb42a02753ffcd2" ], [ "FStar.Krml.Endianness.n_to_be", @@ -423,7 +423,7 @@ "well-founded-ordering-on-nat" ], 0, - "0ea6c49ded312eba8cdd3e143962a993" + "f094a152a4e0c96929d4b799b2aa177e" ], [ "FStar.Krml.Endianness.n_to_be", @@ -442,7 +442,7 @@ "typing_FStar.UInt32.v" ], 0, - "6927e2e24ec4c66e458f69c2d529f777" + "b2ea55c5de3b134919d45b38941d62e2" ], [ "FStar.Krml.Endianness.n_to_le_inj", @@ -464,7 +464,7 @@ "typing_FStar.Krml.Endianness.n_to_le", "typing_FStar.UInt32.v" ], 0, - "96801716443ef9625859f55311205e27" + "43015a047da95e6228b7f862cd398c3e" ], [ "FStar.Krml.Endianness.n_to_le_inj", @@ -483,7 +483,7 @@ "typing_FStar.UInt32.v" ], 0, - "ff02464c3a651f59fdd8259c23d7b9bc" + "12f51daa4caaccacc7a75df8702f8085" ], [ "FStar.Krml.Endianness.n_to_be_inj", @@ -505,7 +505,7 @@ "typing_FStar.Krml.Endianness.n_to_be", "typing_FStar.UInt32.v" ], 0, - "a8e2fa66db7c3b9077723c8b2c3d683f" + "d7119ed2a591500a1cb7c291f6a1c82e" ], [ "FStar.Krml.Endianness.n_to_be_inj", @@ -524,7 +524,7 @@ "typing_FStar.UInt32.v" ], 0, - "3fded3048d322609dfe2eed7ca15e713" + "da8cb88e3816955ee671716887949595" ], [ "FStar.Krml.Endianness.be_to_n_inj", @@ -580,7 +580,7 @@ "well-founded-ordering-on-nat" ], 0, - "d21579a0858d57f9c463d22089827452" + "3d60d6b284e8180a9ed02496715dfc9b" ], [ "FStar.Krml.Endianness.le_to_n_inj", @@ -637,7 +637,7 @@ "typing_FStar.UInt8.v", "well-founded-ordering-on-nat" ], 0, - "696f6707f148dd01ed29d293a9cf64d7" + "e6ab0137d48ead3d62420cec01c543b5" ], [ "FStar.Krml.Endianness.n_to_be_be_to_n", @@ -656,7 +656,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "2c6ddc86bd0474de7781968b9120a0ce" + "c06264d21835854b2f441e5ec2910802" ], [ "FStar.Krml.Endianness.n_to_le_le_to_n", @@ -675,7 +675,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t" ], 0, - "7f76ac4b159a442c42fdcdb41f71314a" + "97fe5b8dabf87e5ed0e9bb3d27a6d73d" ], [ "FStar.Krml.Endianness.uint32_of_le", @@ -695,7 +695,7 @@ "refinement_interpretation_Tm_refine_073e087ab5f9fabfeddf43c4ff72a1d0" ], 0, - "a4ed0955e6a5f7063f3630b8f1c3ad53" + "b6bf31446d551527097427f96460af71" ], [ "FStar.Krml.Endianness.le_of_uint32", @@ -712,7 +712,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "34942e9b231cd01c39485fce8d1cde37" + "b4aa74dc2db50f073ffbbc8691f3decd" ], [ "FStar.Krml.Endianness.uint32_of_be", @@ -732,7 +732,7 @@ "refinement_interpretation_Tm_refine_073e087ab5f9fabfeddf43c4ff72a1d0" ], 0, - "bcea582135df01451e76d0d9b6c49d40" + "8082032425a32141e7a33a8af07181db" ], [ "FStar.Krml.Endianness.be_of_uint32", @@ -749,7 +749,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "bb2e8be32b61442bd2dea0abafaa902f" + "9228c8e49ca4b58d2a9f968d41e97712" ], [ "FStar.Krml.Endianness.uint64_of_le", @@ -769,7 +769,7 @@ "refinement_interpretation_Tm_refine_1cb22d5b190a69600ef23f524d7a6d8a" ], 0, - "56f1e86b7451b2caefea11ab39fa2711" + "a264f48d9b4cccbdd31b565d61df8705" ], [ "FStar.Krml.Endianness.le_of_uint64", @@ -786,7 +786,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "5691fc46f3364b90e2a059c7da01aa72" + "82f3dba935ec1c24a65da2b449b6fdcb" ], [ "FStar.Krml.Endianness.uint64_of_be", @@ -806,7 +806,7 @@ "refinement_interpretation_Tm_refine_1cb22d5b190a69600ef23f524d7a6d8a" ], 0, - "a25c0c019395ca7e7df251e826974368" + "718f295e39f07d92129bf79b3cc023f1" ], [ "FStar.Krml.Endianness.be_of_uint64", @@ -823,7 +823,7 @@ "projection_inverse_BoxInt_proj_0" ], 0, - "8241d798fcc5ed8a72727e584101b274" + "df3372e4a6d44f0f470cdbe6300247be" ], [ "FStar.Krml.Endianness.seq_uint32_of_le", @@ -863,7 +863,7 @@ "well-founded-ordering-on-nat" ], 0, - "5c53302a576f2eb62cb02b4ada6e20ee" + "fa927430e801029537e3f35d561579bb" ], [ "FStar.Krml.Endianness.seq_uint32_of_le", @@ -877,7 +877,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "3691a7e30492e78b9a58e7b9e7fe6e54" + "642561b6e11d07e74f5353aca3ec8ef8" ], [ "FStar.Krml.Endianness.le_of_seq_uint32", @@ -913,7 +913,7 @@ "well-founded-ordering-on-nat" ], 0, - "eff05267fddb18fb5c083e53ed9b5101" + "11a44ff0ba52a66ad93518c70f3337cb" ], [ "FStar.Krml.Endianness.seq_uint32_of_be", @@ -953,7 +953,7 @@ "well-founded-ordering-on-nat" ], 0, - "774e41a26cbac8a4b8917b0fd18d522f" + "9871f14c703c0309f30a91d020735a6c" ], [ "FStar.Krml.Endianness.seq_uint32_of_be", @@ -967,7 +967,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "741c57d883773f12164aac365d7931c6" + "8664e444a0f3918d7cbe2524c506dbf9" ], [ "FStar.Krml.Endianness.be_of_seq_uint32", @@ -1003,7 +1003,7 @@ "well-founded-ordering-on-nat" ], 0, - "016d88370dc75dc01ba690ade6a8f013" + "5c58413a62c88f2e26f07745a3fe5e79" ], [ "FStar.Krml.Endianness.seq_uint64_of_le", @@ -1043,7 +1043,7 @@ "well-founded-ordering-on-nat" ], 0, - "4751ac68f0ca015e95aca8d48b4957c5" + "0210261c822e13b07f3f3dee8924654a" ], [ "FStar.Krml.Endianness.seq_uint64_of_le", @@ -1057,7 +1057,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "83e4f97430753f8a6921f13f362b23f5" + "b53c36c4a6eb7f197166d7446a27c2dc" ], [ "FStar.Krml.Endianness.le_of_seq_uint64", @@ -1093,7 +1093,7 @@ "well-founded-ordering-on-nat" ], 0, - "664fce496812ca0acf0543c59a7189ea" + "fdb61461b247ffdfc0a91919871a4636" ], [ "FStar.Krml.Endianness.seq_uint64_of_be", @@ -1133,7 +1133,7 @@ "well-founded-ordering-on-nat" ], 0, - "4c6e4456cfcb909ab64bc4b619b9468c" + "3332f1551661a1ba0106e742d1989877" ], [ "FStar.Krml.Endianness.seq_uint64_of_be", @@ -1147,7 +1147,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "8dca6f86be95e4fab0c774b01dbc5071" + "d23a045a668ccd11be895602dea24a7a" ], [ "FStar.Krml.Endianness.be_of_seq_uint64", @@ -1183,7 +1183,7 @@ "well-founded-ordering-on-nat" ], 0, - "99ef4e98495c406a394592febdb56194" + "8de75f1155a4b23f59122035af8f0d9b" ], [ "FStar.Krml.Endianness.offset_uint32_be", @@ -1251,7 +1251,7 @@ "well-founded-ordering-on-nat" ], 0, - "a386c2204740a7596a4573a2318008fc" + "e8154c6b78e9960f537502965d173e2d" ], [ "FStar.Krml.Endianness.offset_uint32_be", @@ -1277,7 +1277,7 @@ "typing_FStar.UInt8.t" ], 0, - "e127e9fff3de71ab67184fa76fec1e14" + "77e33c8e93d4da1870a104694eaa2408" ], [ "FStar.Krml.Endianness.offset_uint32_le", @@ -1342,7 +1342,7 @@ "unit_typing", "well-founded-ordering-on-nat" ], 0, - "80a099b984a20ac56d52e2f4d3573aaa" + "1981698a212782935ac4bdec0a74f171" ], [ "FStar.Krml.Endianness.offset_uint32_le", @@ -1368,7 +1368,7 @@ "typing_FStar.UInt8.t" ], 0, - "984cd8890746a353046ef7da63e4adf6" + "c1d4d5871c22e211a7225026492a4302" ], [ "FStar.Krml.Endianness.offset_uint64_be", @@ -1430,7 +1430,7 @@ "well-founded-ordering-on-nat" ], 0, - "1de1f6fc3742e6d0e55969c670e4330c" + "8a75dc9e9f34c399cfc2a5bd5c9da3d8" ], [ "FStar.Krml.Endianness.offset_uint64_be", @@ -1456,7 +1456,7 @@ "typing_FStar.UInt8.t" ], 0, - "73375533bf466ff47e0eba22f1a4c0c7" + "7a8033e76f636e990ecc3e4370a95284" ], [ "FStar.Krml.Endianness.offset_uint64_le", @@ -1521,7 +1521,7 @@ "unit_typing", "well-founded-ordering-on-nat" ], 0, - "8e66cbaef79486bbe347fa214db856e4" + "636d7ce1727546ce31065367475cc592" ], [ "FStar.Krml.Endianness.offset_uint64_le", @@ -1547,7 +1547,7 @@ "typing_FStar.UInt8.t" ], 0, - "48516921aca8dd8ecedf4ea7be7618fb" + "fd099507510268781a5c55cf085120dd" ], [ "FStar.Krml.Endianness.tail_cons", @@ -1579,7 +1579,7 @@ "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.tail" ], 0, - "c43688d3815e1d084c0f1cba10f28095" + "8c6ca5e7bf5592286cc1cb4f5a490451" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_append", @@ -1641,7 +1641,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "c36c3c2b003c59dc2644bfa0066006c2" + "77a3503c862d5bc1299def1c470e8379" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_base", @@ -1697,7 +1697,7 @@ "typing_FStar.UInt8.t" ], 0, - "acdbd4baf4684f22128731f29b8d754c" + "9113a331ce6de9ee00b08334fc495d8b" ], [ "FStar.Krml.Endianness.le_of_seq_uint32_append", @@ -1759,7 +1759,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "59dea65e3918e4b407b0bf65cb8c8aa3" + "afb2176304567b428ac6019dff75f630" ], [ "FStar.Krml.Endianness.le_of_seq_uint32_base", @@ -1815,7 +1815,7 @@ "typing_FStar.UInt8.t" ], 0, - "b023e579bf4a00fc441e9a6965ecdf01" + "80c7e0c48666e8df9dde6a9fce986066" ], [ "FStar.Krml.Endianness.be_of_seq_uint64_append", @@ -1877,7 +1877,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "5761ee448aa3716dfa0db65d78128eb9" + "65e81766ed788f6d49c51728d50b3e35" ], [ "FStar.Krml.Endianness.be_of_seq_uint64_base", @@ -1934,7 +1934,7 @@ "typing_FStar.UInt8.t" ], 0, - "ecc0c88b8793dbc509e76b7df637c4b6" + "1c0ded3cdf434420ff474b7cedb897a7" ], [ "FStar.Krml.Endianness.seq_uint32_of_be_be_of_seq_uint32", @@ -2010,7 +2010,7 @@ "typing_FStar.UInt8.t", "well-founded-ordering-on-nat" ], 0, - "d5d451c9c0c9c72ce027fc21805999af" + "0367c6ca9fb672ffe078d21990b21aab" ], [ "FStar.Krml.Endianness.seq_uint32_of_be_be_of_seq_uint32", @@ -2022,7 +2022,7 @@ "refinement_interpretation_Tm_refine_a84773c2eb377e624aba800b71ec3ba0" ], 0, - "df7f85540b79e491b8ee93a08ef4ab91" + "96a5cb5cd5645ef155af66110c0dd9ac" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_seq_uint32_of_be", @@ -2099,7 +2099,7 @@ "typing_FStar.UInt8.v", "well-founded-ordering-on-nat" ], 0, - "514bf34328513a17d09c4dd036893678" + "d2413a78ec62ce47e017b8d546b7e77c" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_seq_uint32_of_be", @@ -2111,7 +2111,7 @@ "refinement_interpretation_Tm_refine_4239cb7a019da00e7afc3bc55aa05dd7" ], 0, - "e9f9b959122257abe69fa817969eb925" + "d8fdd6f3cc95955867b26f5bd60ed503" ], [ "FStar.Krml.Endianness.slice_seq_uint32_of_be", @@ -2162,7 +2162,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt8.t" ], 0, - "eb7780fb20b75d4ab55d09e91abc4270" + "76c670f7b05e884b890d50f031bee6fc" ], [ "FStar.Krml.Endianness.be_of_seq_uint32_slice", @@ -2200,7 +2200,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt8.t" ], 0, - "09b8105c2366bfad995a5fffc4a1ad69" + "b6f2e5a68abae9453d9945bed25c3632" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.AssocList.fst.hints b/krmllib/hints/LowStar.Lib.AssocList.fst.hints index dbaa7d5e..0269c4ce 100644 --- a/krmllib/hints/LowStar.Lib.AssocList.fst.hints +++ b/krmllib/hints/LowStar.Lib.AssocList.fst.hints @@ -8,7 +8,7 @@ 0, [ "@query", "equation_LowStar.Lib.AssocList.invariant" ], 0, - "a3b8bc1c085233b551f7f7da5b025c27" + "14039be5fd47312a2640122f12215831" ], [ "LowStar.Lib.AssocList.frame", @@ -74,7 +74,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "6254f8946a7100a828a984625a015abe" + "41feee5c2d45fb8a0e37f77d54020dfd" ], [ "LowStar.Lib.AssocList.footprint_in_r", @@ -87,7 +87,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "f07a1f2eda153c60edff35efa8fa40bc" + "a0b87758e99778a6b6398583a22c5714" ], [ "LowStar.Lib.AssocList.footprint_in_r", @@ -103,7 +103,7 @@ "fuel_guarded_inversion_LowStar.Lib.LinkedList2.t" ], 0, - "10631e99fb6a62ec9088ea757633f75e" + "213461a3c3338471e956bdb8cc8f0f2f" ], [ "LowStar.Lib.AssocList.create_in", @@ -137,7 +137,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "01f72b085bccfa074489314a5ce1319c" + "8f8d84b30f99260d2f53214d0ca476e8" ], [ "LowStar.Lib.AssocList.find_", @@ -146,7 +146,7 @@ 0, [ "@query" ], 0, - "c83cc96057205f5ea406221321f1e391" + "ba028d9168bb2f2bfa26dc7a0860a320" ], [ "LowStar.Lib.AssocList.find_", @@ -226,7 +226,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "deb9dd406e93b49de12c8944b7380926" + "f051ef63b56e8c128fdc25a6f8b1e252" ], [ "LowStar.Lib.AssocList.find", @@ -244,7 +244,7 @@ "refinement_interpretation_Tm_refine_b582da5b18980dd549f83acfd27b47df" ], 0, - "ddce1376f3a4ce473c14b6e2d91e92aa" + "6348a2c5b299b09065db1e6cc2a30e1c" ], [ "LowStar.Lib.AssocList.add", @@ -340,7 +340,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "cc44ad71dd1552b724baf4341e92b7c1" + "2c17a6bc5025015f14e0a00519275a20" ], [ "LowStar.Lib.AssocList.remove_all_", @@ -352,7 +352,7 @@ "refinement_interpretation_Tm_refine_666cbc765faa85ecb6368ba0ccf434cd" ], 0, - "6810649fddca00b2f90bf28b5642ab9c" + "71c85f8f01e5a0a731ba5750c1b80c0c" ], [ "LowStar.Lib.AssocList.remove_all_", @@ -481,7 +481,7 @@ "typing_Tm_abs_05dbb0bdbe4a61cef8fed1432b1b98e9" ], 0, - "e24d48baaad0180075fcc172480487d3" + "043529f9db2e0b99ffbac6950ce453e8" ], [ "LowStar.Lib.AssocList.remove_all", @@ -593,7 +593,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions" ], 0, - "a0e13da7b7fcd05b65f7d005be6707b9" + "09e99f704b5e0ebf49e313c19a637fa5" ], [ "LowStar.Lib.AssocList.clear", @@ -752,7 +752,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "0130f286edc9d95f33ee55e5bd789ebf" + "0918c16285689e1a69024341963a4050" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.LinkedList.fst.hints b/krmllib/hints/LowStar.Lib.LinkedList.fst.hints index 8f162d74..7e5c72f0 100644 --- a/krmllib/hints/LowStar.Lib.LinkedList.fst.hints +++ b/krmllib/hints/LowStar.Lib.LinkedList.fst.hints @@ -15,7 +15,7 @@ "projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "ca5914396edb41089c71fade30d3cd3c" + "68068b010b6a5f7ca586118e3e9145fa" ], [ "LowStar.Lib.LinkedList.cells", @@ -43,7 +43,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "aa3f7e4301c206059a0bc5778d354841" + "a6bd5c28ffd7a6d3ecb019e35730b30c" ], [ "LowStar.Lib.LinkedList.same_cells_same_pointer", @@ -79,7 +79,7 @@ "unit_typing" ], 0, - "c6d7ed949220d1efea4bb020de4f7102" + "043da3de850147d8bb0635a0f2457eb9" ], [ "LowStar.Lib.LinkedList.footprint", @@ -107,7 +107,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "26dcf62773e8fa101f348017309eb23e" + "15026d52e60d055b4a993df388ff6fc2" ], [ "LowStar.Lib.LinkedList.cells_pairwise_disjoint", @@ -137,7 +137,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "bce024ea9810fffde43f85fb28224338" + "5483063d8bb372f4c6c886b50bdd9f38" ], [ "LowStar.Lib.LinkedList.cells_live_freeable", @@ -167,7 +167,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "92edc677682a38073b2832c1781d64fe" + "21f6897342baeef13e3a4f32ed1c316a" ], [ "LowStar.Lib.LinkedList.invariant", @@ -176,7 +176,7 @@ 1, [ "@query", "equation_Prims.logical" ], 0, - "1b821398aa20470f00f1796f121e73ed" + "fee340963085ec0496494edbad6dddcf" ], [ "LowStar.Lib.LinkedList.invariant_loc_in_footprint", @@ -234,7 +234,7 @@ "typing_LowStar.Monotonic.Buffer.loc_not_unused_in" ], 0, - "d1474fb4b1594fa3a812e624919e9370" + "e6bc281dfe63aefdd005577a03e424df" ], [ "LowStar.Lib.LinkedList.invariant_loc_in_footprint", @@ -248,7 +248,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "7d7be6f72eb84190cf92cd892f92089f" + "1d8c14241b369dd4fbbad6c990d741e0" ], [ "LowStar.Lib.LinkedList.frame", @@ -339,7 +339,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "83bbd9b4f5c6c168a296f0ca23a0e65b" + "d26126fae995079d0dd3483c3c851035" ], [ "LowStar.Lib.LinkedList.frame", @@ -351,7 +351,7 @@ "refinement_interpretation_Tm_refine_9dfd5ec664d04b1adbe6909975d3119f" ], 0, - "6527bd65857c176495ae0b9153d88575" + "629025ca937943f01b7dddb2f0ef22cf" ], [ "LowStar.Lib.LinkedList.length_functional", @@ -389,7 +389,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "136b9b429b4f294c68391948c869ffd5" + "714cc4351f9e9dba36b59a2473be0a72" ], [ "LowStar.Lib.LinkedList.gmap", @@ -404,7 +404,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "860b54090bbc01fbcec7c8ffd466453a" + "21476f56dc50281b1516143f2142f2a9" ], [ "LowStar.Lib.LinkedList.gfold_right", @@ -419,7 +419,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "0dec8e63c64a0454f6566f1275a446b8" + "e8086accdcc320cb5418f774f241b947" ], [ "LowStar.Lib.LinkedList.deref_cells_is_v", @@ -483,7 +483,7 @@ "typing_LowStar.Lib.LinkedList.cells" ], 0, - "63dc21bf05c69e843425a50ea33b1274" + "bde7e19518b1fbe48c25ee6b189efa59" ], [ "LowStar.Lib.LinkedList.deref_cells_is_v", @@ -495,7 +495,7 @@ "refinement_interpretation_Tm_refine_2cdb1d22d11cea5954bcab0f89d645ec" ], 0, - "74d7d78707f314195f2c37d4c347c10a" + "534c36d70eb028b326ef9c730b1875be" ], [ "LowStar.Lib.LinkedList.footprint_via_cells_is_footprint", @@ -577,7 +577,7 @@ "typing_Tm_abs_3d46d953d7df849c026fcef6c4941216" ], 0, - "aaee70553c86a9e849408d9442e5dca8" + "b35774d59606832529a9109fa816d972" ], [ "LowStar.Lib.LinkedList.footprint_via_cells_is_footprint", @@ -591,7 +591,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "6bd339dd02419ade6adaad0b349a7649" + "02375d808316e9993b736292d5a6f152" ], [ "LowStar.Lib.LinkedList.push", @@ -603,7 +603,7 @@ "refinement_interpretation_Tm_refine_2e3312cd41d7f5efbbbae3b2eeef697e" ], 0, - "8d98cbeb44107f8b91f41d9e33d284a9" + "7ee7eebbfe2cae4604da93554ffa3c79" ], [ "LowStar.Lib.LinkedList.push", @@ -729,7 +729,7 @@ "typing_LowStar.Monotonic.Buffer.loc_unused_in" ], 0, - "b86fe90b0233c7af6aa1fd4279a373cf" + "281a5874aa5e14d15df699dc60b248ce" ], [ "LowStar.Lib.LinkedList.pop", @@ -760,7 +760,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "77ef1255bb9ac6f6daf90d0169b38394" + "b4f2d20f9438cc9cf8cade6debee7e25" ], [ "LowStar.Lib.LinkedList.pop", @@ -868,7 +868,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "919bf5080c2adf3aedd99d5b7476d54b" + "b2921f12e24d70fbce672e75b4178571" ], [ "LowStar.Lib.LinkedList.free_", @@ -880,7 +880,7 @@ "refinement_interpretation_Tm_refine_994dd8cb51034b7a0776f9bb28ca6f71" ], 0, - "641441de1f6dcde276465339ced87509" + "e9310526c8b97e40a6a11f3bf4fcf31e" ], [ "LowStar.Lib.LinkedList.free_", @@ -970,7 +970,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "695178c2d3cb2208b8406b7328060b1d" + "9227302f026bda18ccd711a669a7a2c5" ], [ "LowStar.Lib.LinkedList.free", @@ -982,7 +982,7 @@ "refinement_interpretation_Tm_refine_baa6a0434e5b51218cc000deadc8f6bc" ], 0, - "ddb943a49bcc1e573b03f63d43180207" + "86eaab1ebe546e22061ed4c3e100c442" ], [ "LowStar.Lib.LinkedList.free", @@ -1069,7 +1069,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "cf38c39b319fa0114bc16fe8009bad87" + "ba8a8f02d12d8a75c77716a5fdf36b13" ], [ "LowStar.Lib.LinkedList.length", @@ -1078,7 +1078,7 @@ 1, [ "@query" ], 0, - "ddbd5d24d3a5315fcd07452e30c4721e" + "b25b160a263ac111add773a164be7612" ], [ "LowStar.Lib.LinkedList.length", @@ -1137,7 +1137,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "52e66b1d85cf019f2bd7a032d5e57603" + "0c2e0ac429410132faf40c2a4ba2e95b" ], [ "LowStar.Lib.LinkedList.test", @@ -1274,7 +1274,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "2919d8b7f4a65b25bee35d8db74ca993" + "4d83cb317786230e3df9bef9eb7e7af4" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints b/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints index 73871c2c..4cdc6e48 100644 --- a/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints +++ b/krmllib/hints/LowStar.Lib.LinkedList2.fst.hints @@ -17,7 +17,7 @@ "typing_LowStar.Lib.LinkedList2.__proj__Mkt__item__r" ], 0, - "6329e0d929aa85ff276067c01d52a7f4" + "69743dbac004f057165843b194406b7f" ], [ "LowStar.Lib.LinkedList2.footprint", @@ -29,7 +29,7 @@ "l_and-interp" ], 0, - "129cecdf487e5e5772776fa3f41a2516" + "db87268e9fc3df3bdac8be52e74b6f90" ], [ "LowStar.Lib.LinkedList2.cells", @@ -41,7 +41,7 @@ "l_and-interp" ], 0, - "21d6b9c0973b8a774d40e6eb5c508021" + "c9d612246c1ac9be774ef8ceb5e2625f" ], [ "LowStar.Lib.LinkedList2.footprint_in_r", @@ -112,7 +112,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "e7c8b8a6e1f86341f8232c963ef4f9f0" + "9309f38b7a64881f2d140360ac4bc1f8" ], [ "LowStar.Lib.LinkedList2.frame_footprint", @@ -124,7 +124,7 @@ "refinement_interpretation_Tm_refine_09ad67b9d90ed7b17ddf31c45c68b636" ], 0, - "ad6a4d221ee363f3b137537aae5a60b4" + "3fe2be6cda7a9489790557400d3dd1a2" ], [ "LowStar.Lib.LinkedList2.frame_footprint", @@ -184,7 +184,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "ae9c0c5fe2ece0b2c2ae3edc01b5c37f" + "cef5a6e9ab0bd7d8ad087e1eddfd06b0" ], [ "LowStar.Lib.LinkedList2.frame_region", @@ -196,7 +196,7 @@ "refinement_interpretation_Tm_refine_76a8d76aec5fe95490cf6c28517bab40" ], 0, - "2241ba1fb514cf59e22f9382459c214a" + "48f222b275ec30554b74a3f56382446f" ], [ "LowStar.Lib.LinkedList2.frame_region", @@ -257,7 +257,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "faf16814f5bffa11975a38b973b01545" + "a98adcbf0fbf550f8c31b07c5b73c8c2" ], [ "LowStar.Lib.LinkedList2.create_in", @@ -266,7 +266,7 @@ 0, [ "@query" ], 0, - "2e50aa7156a7e2093e3631f073f39fe3" + "b03a4ea46265a0633f676e676e73fe77" ], [ "LowStar.Lib.LinkedList2.create_in", @@ -397,7 +397,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "fad58dc0590380d0bad677a3be4bad72" + "db922440592273f881f6500501fadfbc" ], [ "LowStar.Lib.LinkedList2.push", @@ -409,7 +409,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "8bdc14bde2ecbf6a0ab9f6cc2e7d8406" + "5ef0708184e5535178e2de270de0ef08" ], [ "LowStar.Lib.LinkedList2.push", @@ -526,7 +526,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "d0ffd5551ebe178ac6e14a9dbf4a38c2" + "6c59b92e1b6d20a2eb1e29ee71ab3ae2" ], [ "LowStar.Lib.LinkedList2.pop", @@ -572,7 +572,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "d28de71453098d1db8f59c39d4f11597" + "74556bd1d4af688faf7e3eeeb3ff6538" ], [ "LowStar.Lib.LinkedList2.pop", @@ -695,7 +695,7 @@ "typing_Prims.uu___is_Cons" ], 0, - "33e2082af30b2a5d441e31a02d67d274" + "9d88b635c52f9254795103fafc7310a5" ], [ "LowStar.Lib.LinkedList2.maybe_pop", @@ -744,7 +744,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "fab4f44d2f558260ff199ce52804311a" + "b35929f26f33a629599d26e80d475014" ], [ "LowStar.Lib.LinkedList2.maybe_pop", @@ -884,7 +884,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "9685c1356174725c06be830d5e9f7989" + "fea0258a4afbd8c9e4d95fd8aa0d37f0" ], [ "LowStar.Lib.LinkedList2.clear", @@ -896,7 +896,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "287a939be73c7cfcb4bf55fbbe6d1a69" + "2091562e67688fdffefe48329f8faa03" ], [ "LowStar.Lib.LinkedList2.clear", @@ -1007,7 +1007,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "4d1bd707ed76872a3e398341542b9146" + "ebb1ce8b28c3a9a1ef3495bb2aede101" ], [ "LowStar.Lib.LinkedList2.free", @@ -1019,7 +1019,7 @@ "refinement_interpretation_Tm_refine_89e26769e50512fd6a99e61c0fe00f0a" ], 0, - "71fcf44fd055c9e0296af369ca4705de" + "a546a4f8fee609b42b8847c7802bef3b" ], [ "LowStar.Lib.LinkedList2.free", @@ -1098,7 +1098,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "3d9eb82c1d1b01c3724670d1bee8aaa8" + "51c8233da15d47494ab0bfe055317ecd" ], [ "LowStar.Lib.LinkedList2.test", @@ -1235,7 +1235,7 @@ "typing_LowStar.Monotonic.Buffer.loc_unused_in" ], 0, - "758ca22040dfcd6a9cd6a98704516d6f" + "c3059ef06470bffdd2e57f5c34f1fa85" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/TestLib.fsti.hints b/krmllib/hints/TestLib.fsti.hints index 4b2bd54b..fe20eea5 100644 --- a/krmllib/hints/TestLib.fsti.hints +++ b/krmllib/hints/TestLib.fsti.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "32d501b824246acda9cfd5e759e01fe3" + "1f7195e173a18dc88f7e481a3b827255" ], [ "TestLib.unsafe_malloc", @@ -17,7 +17,7 @@ 1, [ "@query" ], 0, - "e3fb68ff172ff16f8ebedd1fb82452aa" + "cebfbd03c1291595d17b55465c45329e" ] ] ] \ No newline at end of file diff --git a/krmllib/hints/WasmSupport.fst.hints b/krmllib/hints/WasmSupport.fst.hints index f228911e..36072881 100644 --- a/krmllib/hints/WasmSupport.fst.hints +++ b/krmllib/hints/WasmSupport.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "b735870da1d514f9b6c4a924ac3f173f" + "98713d4b7fec36c9f8f87497f2ab473a" ], [ "WasmSupport.betole64", @@ -29,7 +29,7 @@ 1, [ "@query" ], 0, - "69a0f8bb4daf92c5e89b257aaa035bb3" + "2af06823ff7e7c628664c648a078d0ed" ], [ "WasmSupport.memzero", @@ -63,7 +63,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "6e4e80872f01e0e6638df2654c76722d" + "46ca8a0f0324c6e2deefe3c09b7c8a5a" ] ] ] \ No newline at end of file diff --git a/lib/PrintC.ml b/lib/PrintC.ml index f5ae70fc..0f72c637 100644 --- a/lib/PrintC.ml +++ b/lib/PrintC.ml @@ -291,8 +291,11 @@ and p_expr' curr = function p_stmts stmts and p_comment s = - (* TODO: escape *) - string "/* " ^^ nest 2 (flow space (words s)) ^^ string " */" + if s <> "" then + (* TODO: escape *) + string "/* " ^^ nest 2 (flow space (words s)) ^^ string " */" + else + empty and p_expr e = p_expr' 15 e diff --git a/lib/Simplify.ml b/lib/Simplify.ml index ba7748b8..0534e2d9 100644 --- a/lib/Simplify.ml +++ b/lib/Simplify.ml @@ -1468,6 +1468,7 @@ class scope_helpers = object (self) let local_scope = Hashtbl.find local_scopes current_file in let attempt_shortening = is_private && not is_external in let target = GlobalNames.target_c_name ~attempt_shortening ~kind lident in + (* KPrint.bprintf "%a --> %s\n" plid lident (fst target); *) let c_name = GlobalNames.extend global_scope local_scope is_private lident target in if not is_private then Hashtbl.add original_of_c_name c_name lident diff --git a/test/.hints/Abbrev.fst.hints b/test/.hints/Abbrev.fst.hints index 3bd2fd4b..8454e59f 100644 --- a/test/.hints/Abbrev.fst.hints +++ b/test/.hints/Abbrev.fst.hints @@ -34,7 +34,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "c839e1263e1e5e81dac0884e4bba7022" + "2f58660a5d86e5dc8ca6322838cdf5e0" ] ] ] \ No newline at end of file diff --git a/test/.hints/AbstractStruct.fst.hints b/test/.hints/AbstractStruct.fst.hints index a02a044e..1dedbd98 100755 --- a/test/.hints/AbstractStruct.fst.hints +++ b/test/.hints/AbstractStruct.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "c8c6d209ae05559e7c3c32f3596255c6" + "2005146a80a417f618290491b2200720" ], [ "AbstractStruct.main", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "55c363ed76836b9bc7a5e91d4ba9b897" + "86ce00183817fa35c0d1f2b95c7f2a6e" ] ] ] \ No newline at end of file diff --git a/test/.hints/AbstractStruct2.fst.hints b/test/.hints/AbstractStruct2.fst.hints index 5c2d5e1d..2a06ca57 100644 --- a/test/.hints/AbstractStruct2.fst.hints +++ b/test/.hints/AbstractStruct2.fst.hints @@ -31,7 +31,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "4e2879f8bfc4b624e3d51c597d699a8b" + "55c1907e2e7e6d8d05b36fe364b3be04" ], [ "AbstractStruct2.main", @@ -40,7 +40,7 @@ 1, [ "@query" ], 0, - "cacc0807eb0932ed3de88778874dca73" + "4707b4b22b8f9c2196743e5ee9919140" ] ] ] \ No newline at end of file diff --git a/test/.hints/Attributes.fst.hints b/test/.hints/Attributes.fst.hints index fedbd09a..e5896492 100644 --- a/test/.hints/Attributes.fst.hints +++ b/test/.hints/Attributes.fst.hints @@ -44,7 +44,7 @@ "typing_FStar.Set.union" ], 0, - "98456b4131e9323f51d66cf9ce965cee" + "b1aa2b94671a2982c6a1db06bf940667" ] ] ] \ No newline at end of file diff --git a/test/.hints/BadMatch.fst.hints b/test/.hints/BadMatch.fst.hints index fc2443d7..d12fcbf7 100644 --- a/test/.hints/BadMatch.fst.hints +++ b/test/.hints/BadMatch.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "bbeef39209718547a25046f19766089a" + "e1a5b1c8bff8b6226b2a3849841cdf59" ], [ "BadMatch.baz", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_BadMatch.bar__uu___haseq" ], 0, - "b14509794a49720af5749bc8b9067277" + "94df54321e24671986b2219c7102973e" ] ] ] \ No newline at end of file diff --git a/test/.hints/BlitNull.fst.hints b/test/.hints/BlitNull.fst.hints index 9340f737..2665bca5 100644 --- a/test/.hints/BlitNull.fst.hints +++ b/test/.hints/BlitNull.fst.hints @@ -58,7 +58,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "f40d9640cd1eab059f342101ec62344a" + "c37a38e72a3a1d1d0a3373e47a0f8b1d" ] ] ] \ No newline at end of file diff --git a/test/.hints/C.Nullity.fsti.hints b/test/.hints/C.Nullity.fsti.hints index cb9fddf5..46f0eb86 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, - "ddd2b5996b7ef27ba97f1e0b7c81b2a3" + "cf66de405713025732d32695d0150f7b" ], [ "C.Nullity.pointer_distinct_sel_disjoint", @@ -76,7 +76,7 @@ "typing_FStar.Monotonic.HyperStack.sel", "typing_FStar.UInt32.v" ], 0, - "e9d2dd818414f05ee3b2fc471e8a95b1" + "ab10534881c866d6b92210e7a144027b" ] ] ] \ No newline at end of file diff --git a/test/.hints/C89.fst.hints b/test/.hints/C89.fst.hints index 3ea4bc57..0446d9f3 100644 --- a/test/.hints/C89.fst.hints +++ b/test/.hints/C89.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "5a3d1b4e2d28c34fdcc8e7096f56898e" + "4b984b8b8a1a49562c6800b5d378a8e6" ], [ "C89.g", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "147eafd8c64ad4487ccc8aef5727ca2a" + "6f40c10d7816918ecde21c73652c58cf" ], [ "C89.h", @@ -62,7 +62,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "65db57629a68aefde6caef7329019d21" + "6057885dd873d36ead927203f279ca23" ], [ "C89.i", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "b6651670b364991fa82684dc23216693" + "60acac6da69bb62523c84d8e6f526d99" ], [ "C89.touch", @@ -104,7 +104,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "fc51be6ab65f117cb55bfafcdd7735da" + "51889eb2fca319336e9fec325356d254" ], [ "C89.t", @@ -117,7 +117,7 @@ "typing_FStar.Int32.t", "typing_FStar.Int64.t" ], 0, - "298bf622c0aab69312e776dc2f71b70b" + "d0f9b9cbf248d9b435343f2ee146c1f1" ], [ "C89.__proj__A__item___0", @@ -129,7 +129,7 @@ "refinement_interpretation_Tm_refine_dfc04c5c79d942a90086cac1eb7b1ae6" ], 0, - "de7f5fb486a72f30aa800f1323ed9a8a" + "209c438ab739c4f08963f719d8a7381b" ], [ "C89.__proj__B__item___0", @@ -141,7 +141,7 @@ "refinement_interpretation_Tm_refine_1a06de69b44dc8c0429a5d7e27c9f480" ], 0, - "e473a26fcabeae178f2a4ea1776e5a9c" + "4786530352bdb97c99a9bdb9bea349e3" ], [ "C89.point", @@ -154,7 +154,7 @@ "typing_FStar.Int32.t" ], 0, - "5844fd12efab7a20b6faacbbddd397f6" + "3156fac60a7fc567056309ecfa990120" ], [ "C89.__proj__Point2d__item___0", @@ -166,7 +166,7 @@ "refinement_interpretation_Tm_refine_17ea200a8473bdb82b8d303711705436" ], 0, - "cff4b4b49a7cd241e12185a0390cb11f" + "95976cd01464e2ab2f41fba93a73bf62" ], [ "C89.__proj__Point2d__item___1", @@ -178,7 +178,7 @@ "refinement_interpretation_Tm_refine_17ea200a8473bdb82b8d303711705436" ], 0, - "695cbbe88bababf2d2865bd11e9b5d8d" + "33bb172813edacd651104fc5b57ecd90" ], [ "C89.__proj__Point3d__item___0", @@ -190,7 +190,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "007ed2f533c40790a3d9a93527fec654" + "f66ff966f00769b3e689bb1020574afb" ], [ "C89.__proj__Point3d__item___1", @@ -202,7 +202,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "fc91bd9591be0f41a827c4dbd0b60d94" + "57da618c36ad024ddd1165ee64e03ee8" ], [ "C89.__proj__Point3d__item___2", @@ -214,7 +214,7 @@ "refinement_interpretation_Tm_refine_8a3bd36ce8fbd7cbd87cdc6980d27ae6" ], 0, - "a888da86d2ff03058ae4f5f85d45db5a" + "bcff9abe846b34b7fd56d066d3678757" ], [ "C89.main", @@ -314,7 +314,7 @@ "typing_FStar.UInt32.t", "typing_Prims.pow2" ], 0, - "9d112053ec4da615f779456d1e1a8408" + "6a0d0fe4849fd50e87375836d35b413e" ] ] ] \ No newline at end of file diff --git a/test/.hints/CheckedInt.fst.hints b/test/.hints/CheckedInt.fst.hints index 330b900a..bba588ad 100644 --- a/test/.hints/CheckedInt.fst.hints +++ b/test/.hints/CheckedInt.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "396d24e94b6b9f183083fd7293737628" + "af8e852f4bd056f86f2aef97a6463a5b" ], [ "CheckedInt.two", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "587199f1d55438e35e7edefbf7e7054e" + "9c0af2096a09b4e4ba4320c28564faed" ], [ "CheckedInt.main", @@ -54,7 +54,7 @@ "primitive_Prims.op_Subtraction" ], 0, - "2690b61e0785fa1634f08a99815f0870" + "71b0dd882137510f52aea483ee4bdec9" ] ] ] \ No newline at end of file diff --git a/test/.hints/ColoredRegion.fst.hints b/test/.hints/ColoredRegion.fst.hints index ea9938d0..0d43f5b3 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, - "6964dd4e80b0a02d88767912cd9f6d9a" + "6df929d3dee5ca09fabaf0d5aeb545b6" ] ] ] \ No newline at end of file diff --git a/test/.hints/Comment.fst.hints b/test/.hints/Comment.fst.hints index 771e6436..8fd11393 100644 --- a/test/.hints/Comment.fst.hints +++ b/test/.hints/Comment.fst.hints @@ -11,7 +11,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "2c521d65eb5eda7a4bccbfef1d9e3ae8" + "d4c85d9735110f4040f96320c1a93d3d" ] ] ] \ No newline at end of file diff --git a/test/.hints/ConstBuffer.fst.hints b/test/.hints/ConstBuffer.fst.hints index 61cd263b..dde10d0c 100644 --- a/test/.hints/ConstBuffer.fst.hints +++ b/test/.hints/ConstBuffer.fst.hints @@ -31,7 +31,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "a1c2254e47ddd14d3e7798537a0bfd75" + "638ae222b2c8a16d15821886b8121585" ], [ "ConstBuffer.main", @@ -92,7 +92,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "f4d271e0d25da8aeb9ef696baaa2e1e3" + "41f0bacd481e1bc7c0fdf48d273e2871" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes1.fst.hints b/test/.hints/Ctypes1.fst.hints index 04b3df0e..17a6a9c8 100644 --- a/test/.hints/Ctypes1.fst.hints +++ b/test/.hints/Ctypes1.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "df0550e59a5b9b6880386b2f72e5e198" + "b249faffffd7e1eee2673f8800bfba60" ], [ "Ctypes1.point_no_bind", @@ -25,7 +25,7 @@ "typing_FStar.UInt32.t" ], 0, - "01f1526f1e4b18032d707097270ff95d" + "4fbc2882466b8b4162080eb80436cb7c" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes2.fst.hints b/test/.hints/Ctypes2.fst.hints index 0f759c40..05f9b7a4 100644 --- a/test/.hints/Ctypes2.fst.hints +++ b/test/.hints/Ctypes2.fst.hints @@ -24,7 +24,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "35b6edea80dd6a7b0e1a4091c154e3fc" + "6004e8626e89bab062d75a8d932a41a0" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes3.fst.hints b/test/.hints/Ctypes3.fst.hints index eca72b71..cbd915a3 100644 --- a/test/.hints/Ctypes3.fst.hints +++ b/test/.hints/Ctypes3.fst.hints @@ -13,7 +13,7 @@ "typing_FStar.UInt32.t" ], 0, - "1d47cfe901aa05939a95223941c2306e" + "f3a35852f7926bf04fef07a0d2803358" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ctypes4.fst.hints b/test/.hints/Ctypes4.fst.hints index 7caf8c26..28f653f3 100644 --- a/test/.hints/Ctypes4.fst.hints +++ b/test/.hints/Ctypes4.fst.hints @@ -24,7 +24,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "e534a3f07f744635a0ff2ddd06f494e2" + "fcb2e78d8af3cf48f6398e8fa4819db0" ], [ "Ctypes4.move_circle", @@ -37,7 +37,7 @@ "typing_Ctypes3.__proj__Mkcircle__item__r" ], 0, - "f6c9a8f2eabc1bd30b6392e2673d25ae" + "64f993f96934546f266d63d6f52be131" ], [ "Ctypes4.my_not", @@ -62,7 +62,7 @@ "true_interp" ], 0, - "705cf5a69667a0b8166f50d58eda201a" + "1f03acbaf76b7d9ee14c2cb9664ec915" ], [ "Ctypes4.tr", @@ -77,7 +77,7 @@ "typing_FStar.UInt32.t" ], 0, - "c4abbcca968aa9a80474ca179293a44d" + "b11b079f6a30e9e33f9b409e6d933062" ], [ "Ctypes4.replicate", @@ -90,7 +90,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "b8cfbf01ab5ea963f952a9720f72b477" + "36f0ce54de36f8d47b91e3b7bfc0a9ec" ], [ "Ctypes4.int_opt", @@ -103,7 +103,7 @@ "typing_FStar.UInt32.t" ], 0, - "ea2466e8f68d17342ca404e2a2e15c82" + "df4d66414e2f87e448b81fe691217f52" ], [ "Ctypes4.__proj__IntSome__item___0", @@ -115,7 +115,7 @@ "refinement_interpretation_Tm_refine_747e8dbcdadc1011beb312d289ca27b1" ], 0, - "da55af8d894302d017beb2d718caa8d0" + "b156c701b2903d62863217396fd46cb6" ], [ "Ctypes4.maybe_double", @@ -138,7 +138,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "73579e3d60d7fe5457d8e658028caeed" + "d8271422e13a025f2e608614f50b6661" ], [ "Ctypes4.maybe_double", @@ -174,7 +174,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "a1e2e52d1708ef55ce9f36c4a6021daa" + "0a1d13fbb531235c0b18e2e6775938b4" ], [ "Ctypes4.__proj__L__item___0", @@ -186,7 +186,7 @@ "refinement_interpretation_Tm_refine_369514edfb0ad292ed962e8252b9565a" ], 0, - "ea54b0dcc5a6a27fad37cd63490577f9" + "cf8687d47b8788b4e99a7370bff0b235" ], [ "Ctypes4.__proj__R__item___0", @@ -198,7 +198,7 @@ "refinement_interpretation_Tm_refine_692b693643b05e0d1ba47aa0fabd554b" ], 0, - "3923729a445961c5b725a8edfbf666ab" + "51b6333b45f473842b15d0ea81075bf4" ], [ "Ctypes4.make_L", @@ -211,7 +211,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "7a2f331c8f2af47a66597041b7e06a58" + "c1d772c3dac097ecb44de8b519815143" ], [ "Ctypes4.make_R", @@ -224,7 +224,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "30e34e28cba607c82931f763e269b48a" + "7abf9cc925fe81dd9f1ecc93d9a24346" ], [ "Ctypes4.flip_t", @@ -248,7 +248,7 @@ "true_interp" ], 0, - "55b38bc267344144951f3f9f723cc7e9" + "269efd3a64b657b5a2d750548c4302b6" ], [ "Ctypes4.unsupported_t", @@ -261,7 +261,7 @@ "typing_FStar.UInt128.t", "typing_FStar.UInt32.t" ], 0, - "340baa90563afcd327a497174bac7d9f" + "aa4f9aa11a936125a9a7ba71a4bf99ac" ], [ "Ctypes4.unsupported_abstract_t", @@ -274,7 +274,7 @@ "typing_FStar.UInt128.t", "typing_FStar.UInt32.t" ], 0, - "1b924fcde713af489db11d0ec1c25b51" + "033224334574a2194a5a289be8d760c1" ], [ "Ctypes4.create_u", @@ -307,7 +307,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "2be140338700c33ea53b60b16c872034" + "e97e8b78f928debe9b0cca99c5463b31" ], [ "Ctypes4.read_u_a2", @@ -323,7 +323,7 @@ "typing_Ctypes4.__proj__Mkunsupported_abstract_t__item__a2" ], 0, - "a03bfeb3fce1d216e90ca4f2cbe0a7d8" + "7d471a975d1758abf089764ba7f970e9" ] ] ] \ No newline at end of file diff --git a/test/.hints/CustomEq.fst.hints b/test/.hints/CustomEq.fst.hints index 30d9655c..9009ce2a 100644 --- a/test/.hints/CustomEq.fst.hints +++ b/test/.hints/CustomEq.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "74b6ed642b52393fa2d516adc382f127" + "d30d71653c51bb81eb6ddc554444dc21" ], [ "CustomEq.t", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_CustomEq.point__uu___haseq" ], 0, - "64947633de9b53ee4559f1262c747bbb" + "718ed9b967560c0b9ebcc704d37d56a8" ], [ "CustomEq.__proj__A__item__p1", @@ -33,7 +33,7 @@ "refinement_interpretation_Tm_refine_b42bbc5acfd996b49e25c6ab17e83c41" ], 0, - "06240475dc0149fd8a4f97402d47e5dd" + "329ff34e3cf8ef09c3e160f2e6125600" ], [ "CustomEq.__proj__A__item__p2", @@ -45,7 +45,7 @@ "refinement_interpretation_Tm_refine_b42bbc5acfd996b49e25c6ab17e83c41" ], 0, - "9e0a512635c69f9a9b615877e0081a2e" + "a692e50604189cfe21ae0509c1bec3b5" ], [ "CustomEq.__proj__B__item___0", @@ -57,7 +57,7 @@ "refinement_interpretation_Tm_refine_499f060f30a6559751f4282e23af22de" ], 0, - "ddc5c7ea847c4ccd0cb2fcbe4b1cd8d2" + "d2d00b0cd37428f81612ac504b547b7e" ], [ "CustomEq.p1", @@ -78,7 +78,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "8b721b5d7554a56891d050dd36693ab4" + "b562c20c97c06ec8b854e6951d64bc81" ], [ "CustomEq.f", @@ -99,7 +99,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "c3289f9ea908b63c8039f582b82e769d" + "a84d01929c426a5a5d83350c62e6555d" ], [ "CustomEq.p2", @@ -125,7 +125,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "0685331ca2b1a0cc4da99fcdf32cb1fa" + "f75b2860cc7430e485e0971cbd767d71" ], [ "CustomEq.t1", @@ -140,7 +140,7 @@ "typing_FStar.Int64.t" ], 0, - "cc5d67884f69df8ca74f7e9e7f585c15" + "7a3d70a27b8b9d2cf708ee9c673ba28b" ], [ "CustomEq.t2", @@ -161,7 +161,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "777b85be33daf74289ede0b2d619c4a3" + "ff56ec152de8cc89b671e507ece866da" ], [ "CustomEq.id", @@ -182,7 +182,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "8ea0f3435d097564ffaffcfce6167104" + "e88718e46fd2773b3629dab66c802c1c" ], [ "CustomEq.main", @@ -202,7 +202,7 @@ "typing_FStar.Int64.t" ], 0, - "717359e23378c06caec473e5ea4fd1e7" + "ea9362b15ebdb9edfef8bd824f027c7b" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypes.fst.hints b/test/.hints/DataTypes.fst.hints index 48f43d14..49e98658 100644 --- a/test/.hints/DataTypes.fst.hints +++ b/test/.hints/DataTypes.fst.hints @@ -11,7 +11,7 @@ "refinement_interpretation_Tm_refine_599cdc3d9160d7b695e8959f132bb409" ], 0, - "81a60cf58b5557a9bf4208b921b991fb" + "6decf5c7cef2e0cd54a2b2d890f76493" ], [ "DataTypes.__proj__A__item__b", @@ -23,7 +23,7 @@ "refinement_interpretation_Tm_refine_599cdc3d9160d7b695e8959f132bb409" ], 0, - "ab6c50fd3ad61fc909f01edd210273c4" + "746975921c4853947d750182f1eee1eb" ], [ "DataTypes.__proj__B__item__c", @@ -35,7 +35,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "ca9a4ef608a5142e38d3656d30164d17" + "1f799cd9ca3d037c356183a7c1933f3b" ], [ "DataTypes.__proj__B__item__d", @@ -47,7 +47,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "4c42b8e07acb8767380f1532100db806" + "c3f3e92596e607bf5af1d9b599d02244" ], [ "DataTypes.__proj__B__item__e", @@ -59,7 +59,7 @@ "refinement_interpretation_Tm_refine_e0fbb0ccb14c7057144f6a5a325e8ddd" ], 0, - "4e6e573ea4e5a3a97757e61d510a1780" + "f6286a8c11778c1ace5e7005675eebcf" ], [ "DataTypes.__proj__C__item__f", @@ -71,7 +71,7 @@ "refinement_interpretation_Tm_refine_b63a9a8aecee956770bb1476545b326e" ], 0, - "279acb2e30137faf75326e914dce9c36" + "0da833caceba112d4c204e6e99049316" ], [ "DataTypes.__proj__C__item__g", @@ -83,7 +83,7 @@ "refinement_interpretation_Tm_refine_b63a9a8aecee956770bb1476545b326e" ], 0, - "4506cf65eecedfa772f5c4bf4b588547" + "35ed4a704a8c1374a8347ac465a5b256" ], [ "DataTypes.__proj__D__item__h", @@ -95,7 +95,7 @@ "refinement_interpretation_Tm_refine_4c835444c923ef29c3c5e4f8248f0c1c" ], 0, - "0232cdb5e3050f661588a4dd55d1b041" + "5b77211c56f63ba95936af9772e22bf0" ], [ "DataTypes.__proj__D__item__i", @@ -107,7 +107,7 @@ "refinement_interpretation_Tm_refine_4c835444c923ef29c3c5e4f8248f0c1c" ], 0, - "070a4d74b618056e83c5be6b945bf6d8" + "0d8bd8d9bec1cbf035dcf1cd0867deae" ], [ "DataTypes.test", @@ -129,7 +129,7 @@ "typing_tok_DataTypes.E@tok" ], 0, - "a175a306b0ac9ca27e40f33ca0996806" + "0381d724111da379c24d29df2323757b" ], [ "DataTypes.something", @@ -150,7 +150,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "ddefc5be0477a1243005779b341ce353" + "8cedfff903dbc1d69ad87e8c52d5adda" ], [ "DataTypes.whatever", @@ -171,7 +171,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "bcd121760680f6ac0ab335f7a5aa23cc" + "004adbb8ef02d88ed6eee4444ee7065b" ], [ "DataTypes.point", @@ -184,7 +184,7 @@ "typing_FStar.UInt32.t" ], 0, - "9221e8763f7561b08a1b92405374a138" + "9da3b68e0fb69dbd2c94ebf9618f39de" ], [ "DataTypes.f", @@ -203,7 +203,7 @@ "true_interp" ], 0, - "66a54e9e9f0d75cf9248e390a8471149" + "37a33f698df5accfbc6edcc3d3c3f512" ], [ "DataTypes.f'", @@ -222,7 +222,7 @@ "true_interp" ], 0, - "0899942b8f6df1ae5aa651a2330251e3" + "b4a9b53b501e287239f50c2f23b58364" ], [ "DataTypes.main", @@ -265,7 +265,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "a37985bb42b867a60db50dc0aaf2bd2f" + "6eef1e986a1cbf21aa78fa724d2612b6" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypesEq.fst.hints b/test/.hints/DataTypesEq.fst.hints index 7e1089cc..ecf88cba 100644 --- a/test/.hints/DataTypesEq.fst.hints +++ b/test/.hints/DataTypesEq.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "02c4cf2008ca938982cdc55c21b3848e" + "049551fa2f812518e036663863c4839c" ], [ "DataTypesEq.__proj__A__item___0", @@ -24,7 +24,7 @@ "refinement_interpretation_Tm_refine_7fe4ec39530be71d09622e6ea631b362" ], 0, - "f90f750ba45f7bc6997179679d8a002d" + "585692a775e19ec7e29e06f5c9d3005d" ], [ "DataTypesEq.__proj__B__item___0", @@ -36,7 +36,7 @@ "refinement_interpretation_Tm_refine_4d5e6c06bbfb6471b81e2745aebd0ea5" ], 0, - "a06fc542270c5fea08c79157453fba6e" + "d1cb9c23b7dc28d5a09e8e23b8f10b42" ], [ "DataTypesEq.f", @@ -57,7 +57,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "b719baca34fbb58b9d6f6041f733923d" + "fcb0d8f16cfdea24d4d6b0f95b0987d9" ], [ "DataTypesEq.main", @@ -66,7 +66,7 @@ 1, [ "@query", "assumption_DataTypesEq.t__uu___haseq" ], 0, - "bc5455c92ea7bfe8aec610838d60b407" + "49b2cfa8c44e975c4db381af80d4b5f9" ] ] ] \ No newline at end of file diff --git a/test/.hints/DataTypesSimple.fst.hints b/test/.hints/DataTypesSimple.fst.hints index 5c35ec11..8678a283 100644 --- a/test/.hints/DataTypesSimple.fst.hints +++ b/test/.hints/DataTypesSimple.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "da5941889262d871dcea592bf84007e1" + "d1486824fed45f0ede32327f333a635c" ], [ "DataTypesSimple.f", @@ -35,7 +35,7 @@ "typing_tok_DataTypesSimple.Cons1@tok" ], 0, - "7f9fb309250c9f22a3f18cefada49071" + "f4c81f60eb7832c724768c6d30d3c8ca" ], [ "DataTypesSimple.main", @@ -57,7 +57,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "95c86cba0fef65e4294fa3335ef694ea" + "caa0c4a940fca72feb14334ce3f2e43e" ] ] ] \ No newline at end of file diff --git a/test/.hints/DepPair.fst.hints b/test/.hints/DepPair.fst.hints index 8cbffde6..3efd51bc 100644 --- a/test/.hints/DepPair.fst.hints +++ b/test/.hints/DepPair.fst.hints @@ -14,7 +14,7 @@ "refinement_interpretation_Tm_refine_07df04c09226e2c84c0e481d49caecb3" ], 0, - "498782c19c8a1a220bbd8462ba3df855" + "237cf127604527dfc43d2b65acd59d9f" ] ] ] \ No newline at end of file diff --git a/test/.hints/Deref.fst.hints b/test/.hints/Deref.fst.hints index cd2511f7..0643c185 100644 --- a/test/.hints/Deref.fst.hints +++ b/test/.hints/Deref.fst.hints @@ -11,7 +11,7 @@ "refinement_interpretation_Tm_refine_a4c630dd50df89c6126905a64f1064c1" ], 0, - "fb1e4d593b3da7cd6d52be77e17a0fac" + "d5eb02793125ac13d43dc0de9d7fc905" ], [ "Deref.test2", @@ -43,7 +43,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "dc82bc689526642c5c40f8839be73ec8" + "b48682cf69c84ab993ef7a28096622ee" ], [ "Deref.test3", @@ -112,7 +112,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "40a016db3b89e6dd5d00efae44a94063" + "71800721ce4a05bdb573ed1bb3b425da" ], [ "Deref.test4", @@ -186,7 +186,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "17c9290bfcc120e419783403c88e3f77" + "c71bc5c400670e6f73101fcb6fd05103" ] ] ] \ No newline at end of file diff --git a/test/.hints/Endianness.fst.hints b/test/.hints/Endianness.fst.hints index 1302dbed..bdb41864 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, - "d528bbeae5880eb2393f051066cd28a2" + "4c2723b1da1803a482dbc6c5a35de7ac" ] ] ] \ No newline at end of file diff --git a/test/.hints/EqB.fst.hints b/test/.hints/EqB.fst.hints index 55828d9f..f48f625d 100644 --- a/test/.hints/EqB.fst.hints +++ b/test/.hints/EqB.fst.hints @@ -73,7 +73,7 @@ "typing_FStar.UInt32.t" ], 0, - "f119176186cce86d9d16e768dbcab1e4" + "10fafd048e29af994ac0052df1247143" ] ] ] \ No newline at end of file diff --git a/test/.hints/EtaStruct.fst.hints b/test/.hints/EtaStruct.fst.hints index 9cf415ea..33dd6f73 100644 --- a/test/.hints/EtaStruct.fst.hints +++ b/test/.hints/EtaStruct.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "e46ee4e66a616aab48f1ea803bac6823" + "d2dee27d4161069466e0d4c5a7fe5a8a" ], [ "EtaStruct.f", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "4fd9cda64618612ca427bf18abf8be0c" + "f900440858ee716b63051c5ee1208d66" ], [ "EtaStruct.main", @@ -34,7 +34,7 @@ 1, [ "@query" ], 0, - "7413614fb97b452770898ca195880506" + "382d28015f78f3811a118fa52ea8c277" ] ] ] \ No newline at end of file diff --git a/test/.hints/ExitCode.fst.hints b/test/.hints/ExitCode.fst.hints index dc0b59cf..9d2ac5c2 100644 --- a/test/.hints/ExitCode.fst.hints +++ b/test/.hints/ExitCode.fst.hints @@ -21,7 +21,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "1c1632c698dc488f070337d645d30f6f" + "112115714c1c38d74b032bb9c5616883" ] ] ] \ No newline at end of file diff --git a/test/.hints/Failwith.fst.hints b/test/.hints/Failwith.fst.hints index a497a2d0..fb21b056 100644 --- a/test/.hints/Failwith.fst.hints +++ b/test/.hints/Failwith.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "35a17b7cc68331fb742b7e7955d24079" + "ca7d9d526e1e10f15308ca9d192cb575" ], [ "Failwith.main", @@ -29,7 +29,7 @@ 1, [ "@query" ], 0, - "5614c815674036bd77b7ee3c98bfd715" + "83b7ecb5c5fe4e6c7d6e6898339decee" ] ] ] \ No newline at end of file diff --git a/test/.hints/Fill.fst.hints b/test/.hints/Fill.fst.hints index e39b7d81..b2aa98bb 100644 --- a/test/.hints/Fill.fst.hints +++ b/test/.hints/Fill.fst.hints @@ -17,7 +17,7 @@ "true_interp" ], 0, - "1da954a0b8b091c908977fb162651b43" + "b658f01d84516fa3bbb47f5966d46a70" ], [ "Fill.fill_out_uint8", @@ -34,7 +34,7 @@ "true_interp" ], 0, - "077aa7732e6883e4653f3f4e4b637ec3" + "1c65bca2165a1ff876699ae6a53aa239" ], [ "Fill.test", @@ -106,7 +106,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "57b2431b5220f123b2a56672e30f8cb5" + "a597d133fb816c46b88b2845962197bb" ], [ "Fill.main", @@ -157,7 +157,7 @@ "typing_FStar.Set.singleton", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "99ce4b056aca9d99523bc3f777b63446" + "f7b247081848a8f2fb5d79b0a03268ee" ] ] ] \ No newline at end of file diff --git a/test/.hints/Flat.fst.hints b/test/.hints/Flat.fst.hints index f331dabb..1921547a 100644 --- a/test/.hints/Flat.fst.hints +++ b/test/.hints/Flat.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "e8f4d0511642e627f0033b1a8c543bed" + "014b58b6c5eb86c26ad2d394e634ba9b" ], [ "Flat.main", @@ -90,7 +90,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "0d30d3518a3905b32e8c2d2639475e27" + "56b77c70462fc2bcc4ab6bd0c2b2e1ba" ] ] ] \ No newline at end of file diff --git a/test/.hints/FunPtr.fst.hints b/test/.hints/FunPtr.fst.hints index 4f4aada5..504a2c5c 100644 --- a/test/.hints/FunPtr.fst.hints +++ b/test/.hints/FunPtr.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "19fc063add061b526cb84648f4c9301d" + "8e9a2ce22a6c5248384404d7ddd9a83f" ], [ "FunPtr.main", @@ -27,7 +27,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "bafd71343fdb17a063a497016a8ea5bc" + "ae972fc01abe9959cf5dd6ce8e91c62b" ] ] ] \ No newline at end of file diff --git a/test/.hints/FunctionalEncoding.fst.hints b/test/.hints/FunctionalEncoding.fst.hints index b2ac9ad9..8ebcb240 100644 --- a/test/.hints/FunctionalEncoding.fst.hints +++ b/test/.hints/FunctionalEncoding.fst.hints @@ -16,7 +16,7 @@ "typing_FunctionalEncoding.__proj__Mkanimal__item__species" ], 0, - "c4c3ae72447797b457eb3339c36f8dba" + "c6c4ea772713a5eb8e9b3840a2cf3f5f" ] ] ] \ No newline at end of file diff --git a/test/.hints/GcTypes.fst.hints b/test/.hints/GcTypes.fst.hints index 2268f94d..becb1191 100644 --- a/test/.hints/GcTypes.fst.hints +++ b/test/.hints/GcTypes.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "49d8b04d7469384ea7dff25c96c65b06" + "4d9d4fc873fb60ccb2a5a60b042db7cd" ], [ "GcTypes.main", @@ -33,7 +33,7 @@ "refinement_interpretation_Tm_refine_abf749ae3c800f91a6f1dcf2ecb5621e" ], 0, - "cadcb6c39a387b787528818cd0801662" + "12a646496a3bccee13a9e3542744705d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Ghost1.fst.hints b/test/.hints/Ghost1.fst.hints index 49c8bb0b..073e22b3 100644 --- a/test/.hints/Ghost1.fst.hints +++ b/test/.hints/Ghost1.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "960aaf0f585e1df978c98f8121698c18" + "31d0a494824ca7aaa58a660dc4d8753b" ], [ "Ghost1.test", @@ -29,7 +29,7 @@ 1, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "6656621c4a0c947369b4c91194145528" + "194c2e05afe4f8662bf4fd6c413c5afb" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder.fst.hints b/test/.hints/HigherOrder.fst.hints index de888640..50fe661e 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, - "4e4f026f93e1c22f6907e34f0d4bb07b" + "2781d406d61666eece2870cf2f8c62eb" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder2.fst.hints b/test/.hints/HigherOrder2.fst.hints index f943f836..b15cb1e4 100644 --- a/test/.hints/HigherOrder2.fst.hints +++ b/test/.hints/HigherOrder2.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "a7fe89c21f83bcc3451bb90b3a714111" + "19b7289298d5119bae7ddfaf4555948a" ], [ "HigherOrder2.exampleFunc", @@ -31,7 +31,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "881df8333d6abb01bdf1e8eaabd3f20a" + "b24e5b2106f27d5f17cb1ccde78ca8b4" ], [ "HigherOrder2.main", @@ -60,7 +60,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "3a8dd1adaa621f4b29cabbccac2848c7" + "e6569894c4dc0641cacd7a9a85443f47" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder3.fst.hints b/test/.hints/HigherOrder3.fst.hints index 0eb837e2..08da26d1 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, - "98f16ef3a1ea306e3d38c2c1f8e1c849" + "13ea04284db2a3fe2e797f3964fe8213" ], [ "HigherOrder3.exampleFunc", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "fb3c81dd8a2b47e3348fe2c7309d04fe" + "5e13e3a051f7a2c49ee1bb5308c66cc3" ], [ "HigherOrder3.main", @@ -50,7 +50,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "1e712b9fc2444b5f5eea22a4f3f2238d" + "1328a9b60358567c31b8e6507720e318" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder4.fst.hints b/test/.hints/HigherOrder4.fst.hints index 1ca3cecf..b7756c7c 100644 --- a/test/.hints/HigherOrder4.fst.hints +++ b/test/.hints/HigherOrder4.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "201dca5b1c4490c360cb82bf5e4d7214" + "a293477da0c646022ec674907b469eaa" ], [ "HigherOrder4.createContainer", @@ -66,7 +66,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "cf9c92ec97d895d0040ae873bc442261" + "d9561633ec41631154a92ad71b296536" ], [ "HigherOrder4.main", @@ -118,7 +118,7 @@ "typing_Prims.pow2" ], 0, - "7062c022a9b93c89c6f7e0e4c6df0846" + "24ee925319fb79dc6310964e53a55306" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder5.fst.hints b/test/.hints/HigherOrder5.fst.hints index 2d1f7ea7..c078484e 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, - "e87f34e1ae02623975a2f669e862e958" + "86b88e48970fef30a4e076d87916ee01" ], [ "HigherOrder5.t_D", @@ -25,7 +25,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperHeap.rid" ], 0, - "d66899a403766eb94621543770ba9149" + "0a0a20fa163d7fe9a822e9e2ca6a35f6" ], [ "HigherOrder5.foo", @@ -38,7 +38,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "d95f3b69a5185cf95a73e0852c235b1e" + "26740f6457c973e0b99af70cc91d0374" ], [ "HigherOrder5.main", @@ -87,7 +87,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "337cb0c1ee24705b5d43e0a3a308886d" + "edbfac95c3e48bbff1c3f0cd4fe092f3" ] ] ] \ No newline at end of file diff --git a/test/.hints/HigherOrder6.fst.hints b/test/.hints/HigherOrder6.fst.hints index 08012798..8a2d6cff 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, - "17eaf8580b15ca0f8d07f9cbc2bde81f" + "bcbd26ce216b8ceee9a35983acb6ae4d" ], [ "HigherOrder6.t_D", @@ -25,7 +25,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperHeap.rid" ], 0, - "29181ff1a77360da1c1c1d43747455a5" + "868ef1551f6ad81a40fd393a52e133a6" ], [ "HigherOrder6.foo", @@ -38,7 +38,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "a887f01110b0f9a4a616b469e935918c" + "352aa21244d87f6560d476f1b2f85e48" ], [ "HigherOrder6.main", @@ -87,7 +87,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, - "d7e128652cf40627baa913f379fa4abe" + "c2e2f8366972831fd600e842581d9535" ] ] ] \ No newline at end of file diff --git a/test/.hints/Hoisting.fst.hints b/test/.hints/Hoisting.fst.hints index f97fcc5c..d0ecdd2b 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, - "e259211404fc956c2c9cf058e60ce378" + "856810d482a5585134eaa51efef1735f" ], [ "Hoisting.main", @@ -124,7 +124,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "cb4388db51156f9fcea9dfc6d76abbe4" + "befe53c561666c755648a651b0725149" ] ] ] \ No newline at end of file diff --git a/test/.hints/IfDef.fst.hints b/test/.hints/IfDef.fst.hints index ac46ead9..acdecc38 100644 --- a/test/.hints/IfDef.fst.hints +++ b/test/.hints/IfDef.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "a5ab044d82ea7c6b4058c7bb360e6636" + "22811c6996416051d807ec380a30c53e" ], [ "IfDef.foo'", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "05f6be678e16d7b7db0150ec1d51c654" + "b555354421d728e3c07e5cafcc39eb23" ], [ "IfDef.test", @@ -63,7 +63,7 @@ "unit_typing" ], 0, - "2fa7e3ce91092dd19aa51c59678874ac" + "82ff5bbccc3267a6c97134e89353bb2d" ], [ "IfDef.bar", @@ -84,7 +84,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "7a83022acedcb697ce8f748c6326c9d4" + "f0ce6d71619e147e2b45af875979ce71" ], [ "IfDef.test3", @@ -93,7 +93,7 @@ 1, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "cdaa41a507b0ca8415a08409f6a0f5ac" + "3b86d9f61ca38a052e3db22c1fbefd5b" ] ] ] \ No newline at end of file diff --git a/test/.hints/IfDefKrml.fst.hints b/test/.hints/IfDefKrml.fst.hints index 31fe0c83..30b57335 100644 --- a/test/.hints/IfDefKrml.fst.hints +++ b/test/.hints/IfDefKrml.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "da974d484ca5da9b0ece7ed184937086" + "24dfd912ca4d86130289569202247592" ] ] ] \ No newline at end of file diff --git a/test/.hints/IfThenElse.fst.hints b/test/.hints/IfThenElse.fst.hints index b3473ff9..81fb1f02 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, - "2bab16067012398f7e7c2eb7b59225f4" + "7a6027e1461b77dfaa9dc50772a16f52" ], [ "IfThenElse.main", @@ -35,7 +35,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "45473c9be6a9f180390263d0b4a1394b" + "68826989a0b130c04bc1a4830758b266" ] ] ] \ No newline at end of file diff --git a/test/.hints/InitializerLists.fst.hints b/test/.hints/InitializerLists.fst.hints index ff6a6d93..685cfd52 100644 --- a/test/.hints/InitializerLists.fst.hints +++ b/test/.hints/InitializerLists.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "473b08cdd18a90a707595aadc28d91d1" + "b5d7a2b1a90b918831dd5dbbeb8abcf0" ], [ "InitializerLists.x2", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "402cd6eb9934e47f8ea7ea71647bdb10" + "23c0837a580ec2fba61507022fd632a8" ], [ "InitializerLists.x3", @@ -83,7 +83,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "736127ac8ab3519c45831346108df045" + "0f2b1132d6e02f019298fe46dacdf434" ], [ "InitializerLists.f", @@ -96,7 +96,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "b5b978efddf3f39db58f3c2eefc4a1b3" + "66d3a53d6470f991924ba21eb81e9dcc" ], [ "InitializerLists.main", @@ -147,7 +147,7 @@ "typing_InitializerLists.x" ], 0, - "c47612c719ea24e66a6efb3a3cb717c7" + "756901fd80886f048a6256d6f70a734e" ] ] ] \ No newline at end of file diff --git a/test/.hints/Inline.fst.hints b/test/.hints/Inline.fst.hints index b3cb0f85..57ac6d4b 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, - "674c15e9b36b527c05b62780debbacf8" + "4e8519a2258316b45efa0259e890dde6" ], [ "Inline.main", @@ -117,7 +117,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "50f2f8846f25245f056c75a5127c825f" + "1c8e29ef7519f623d155fae2d81a927e" ] ] ] \ No newline at end of file diff --git a/test/.hints/InlineNoExtract.fst.hints b/test/.hints/InlineNoExtract.fst.hints index 6c241c90..8a34a236 100644 --- a/test/.hints/InlineNoExtract.fst.hints +++ b/test/.hints/InlineNoExtract.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "01b1ea8d9b44cfa3a0adc8acbaad8d90" + "9ecd5193dfae35f289640300c6f40d53" ], [ "InlineNoExtract.b", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "de92b3e7066d946d0d7f87085df7f546" + "0b0a910a3fc45157b6150c3417135de5" ] ] ] \ No newline at end of file diff --git a/test/.hints/InlineTest.fst.hints b/test/.hints/InlineTest.fst.hints index 1e7b5818..ffb8bea2 100644 --- a/test/.hints/InlineTest.fst.hints +++ b/test/.hints/InlineTest.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "f25813eb13b56ae4453b1ab3998e3642" + "a22eac8a47dd97af25b0a5cf36f44e55" ], [ "InlineTest.__proj__Error__item___0", @@ -20,7 +20,7 @@ "refinement_interpretation_Tm_refine_dc1c4313057dcc858ffa9fd88c3f020d" ], 0, - "74d4846b597c38275ad4f23cfa440b50" + "75053785d995078ad473420f6d1ca1a1" ], [ "InlineTest.__proj__Correct__item___0", @@ -32,7 +32,7 @@ "refinement_interpretation_Tm_refine_dc046c5c58c78691ac946f81662277ac" ], 0, - "a7a974bac94b702375e871b9dcf0edfd" + "f09a0d0bedcf9325e18c9de854330eb9" ], [ "InlineTest.main", @@ -50,7 +50,7 @@ "projection_inverse_InlineTest.Correct__b" ], 0, - "ee5ccd9f8dc6af780f981e3394d36abd" + "376b3327deac5b04aad38c020f400b1f" ] ] ] \ No newline at end of file diff --git a/test/.hints/Intro.fst.hints b/test/.hints/Intro.fst.hints index 42b4fd1a..8f965fa7 100644 --- a/test/.hints/Intro.fst.hints +++ b/test/.hints/Intro.fst.hints @@ -82,7 +82,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "591949ecaed8d1c04c739289ea03fe53" + "12e8cd1603729796dc066d4bad7ebf86" ] ] ] \ No newline at end of file diff --git a/test/.hints/Layered.fst.hints b/test/.hints/Layered.fst.hints index 4c9a45d9..0d2132c6 100644 --- a/test/.hints/Layered.fst.hints +++ b/test/.hints/Layered.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "f26c0ffb7dfa998b23df4fd8f8f4a8b2" + "045c53979160b138b80f8465bb8f1898" ], [ "Layered.return", @@ -29,7 +29,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "c65b73517a103125abaf6500dff5a062" + "7fb3f1f24a543a30ec1ccaebf132d36b" ], [ "Layered.bind_wp", @@ -53,7 +53,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "209031574db92df70cbacc07637afbb0" + "e90ecc06b5dc7e2cf2aa7126409b0a33" ], [ "Layered.bind", @@ -89,7 +89,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "4735e8f5fe185db32b79f4f4b08cb0b2" + "94c13a42ed944b8c0e9f5cdcc0d55c8d" ], [ "Layered.subcomp", @@ -109,7 +109,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "aa64ae81324f025677e82e0a4aa56be7" + "361bb1a12dcde7e2de73060ac832bebc" ], [ "Layered.if_then_else_wp", @@ -124,7 +124,7 @@ "refinement_interpretation_Tm_refine_b5b7150a72165c5a72019df5afbe737b" ], 0, - "6e73a2188e8a364f703e4dc4f675fdf3" + "10fabfcc66df3c8b6a97e311c6038d3c" ], [ "Layered.BUG", @@ -133,7 +133,7 @@ 1, [ "@query" ], 0, - "b30053e7b95b7c2dee712231e4c5173c" + "624377fa51da131bd36314807a1a3842" ], [ "Layered.BUG", @@ -145,7 +145,7 @@ "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, - "8fee2b94819ee30cd3baf312dc573011" + "62d1fe9fab7932ac85dfc31972e78283" ], [ "Layered.BUG", @@ -157,7 +157,7 @@ "refinement_interpretation_Tm_refine_de09779676242898794a0b057d5f5bb4" ], 0, - "c9d3f1e10f099decd74fd669a7af3275" + "699bd885e9dcd0c7377b77d3cdd91c7a" ], [ "Layered.get_ctx", @@ -183,7 +183,7 @@ "typing_tok_Layered.Context@tok" ], 0, - "e22f895720602d7097387e833b802bb8" + "cb8166c21b026cefbd54a87cba0c1454" ], [ "Layered.lift_pure_wp", @@ -204,7 +204,7 @@ "typing_Tm_abs_d0f415a5361a9d7988d8e425dc193472" ], 0, - "b04f4755c08bbc891947aa93e0b7933b" + "2580b432b43c2e3b65680c2fb16d2b0d" ], [ "Layered.lift_pure", @@ -235,7 +235,7 @@ "typing_Tm_abs_efa2eac81cd2c08d7047b2fc27fb6578" ], 0, - "9d5336bb3b19f5e080fe9507c693d28b" + "f0de4331968b97b264ff2d435dd7b9a3" ], [ "Layered.test", @@ -262,7 +262,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "641a477f68a5e32574ff45d6dc7a8603" + "5cd5648fa56e5d25199e3c6343eca7b2" ], [ "Layered.main", @@ -291,7 +291,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "d09b44c52e8e2851bf836cfeee36c52b" + "4112481548ac9d102773e9a880497682" ] ] ] \ No newline at end of file diff --git a/test/.hints/Library.fst.hints b/test/.hints/Library.fst.hints index 11104d0a..b4177a56 100644 --- a/test/.hints/Library.fst.hints +++ b/test/.hints/Library.fst.hints @@ -82,7 +82,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "f99f1246de6c4522f4b2b6ae67ef02a7" + "f4cf912e4926afb0bbdb7be2fd3fc9b0" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList1.fst.hints b/test/.hints/LinkedList1.fst.hints index 3c6fc7d3..44548f27 100644 --- a/test/.hints/LinkedList1.fst.hints +++ b/test/.hints/LinkedList1.fst.hints @@ -11,7 +11,7 @@ "refinement_interpretation_Tm_refine_a3ca1ff7326b0e9a8828d37afc6032a0" ], 0, - "7a8768b7f6637ab743e8c93d274edc01" + "ee9b6643de4610a1c1336ad825688116" ], [ "LinkedList1.__proj__Cons__item__data", @@ -23,7 +23,7 @@ "refinement_interpretation_Tm_refine_a3ca1ff7326b0e9a8828d37afc6032a0" ], 0, - "9520aa9a3ae641274214294660e973df" + "3f459a6fc96893098fcd2fa91e55a1db" ], [ "LinkedList1.well_formed", @@ -45,7 +45,7 @@ "well-founded-ordering-on-nat" ], 0, - "d39a413c45b013e225a24f7e21f23ee9" + "277432da4542408b690f61b04f3abdcc" ], [ "LinkedList1.cons_nonzero_length", @@ -65,7 +65,7 @@ "projection_inverse_BoxBool_proj_0" ], 0, - "7fa8e0f4b986b36d5538244665c5a80f" + "7d68e7a16b5842015d8a35ae1af3f36d" ], [ "LinkedList1.length_functional", @@ -117,7 +117,7 @@ "well-founded-ordering-on-nat" ], 0, - "637d9a8a19b52b1dfadef7e883ab14ef" + "5e478751c71c0277c72c036454a89bb9" ], [ "LinkedList1.length_functional", @@ -131,7 +131,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "1377ee80b83833cc2f2beaf489755631" + "c212c5a66925b33963f74d1f6e5c4df6" ], [ "LinkedList1.live_nil", @@ -162,7 +162,7 @@ "typing_FStar.Monotonic.HyperStack.sel" ], 0, - "823f7c342c6006b63784ecf5d471d664" + "5d6b945464e88749700d56b6690f86ca" ], [ "LinkedList1.live_cons", @@ -200,7 +200,7 @@ "typing_FStar.Monotonic.HyperStack.sel" ], 0, - "ce03c674b34ff8ff0e5504d9fd34a2d6" + "89de4b3ff72eca7e10ee2c8b49e63f64" ], [ "LinkedList1.disjoint", @@ -214,7 +214,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "96afdc5b3aa769fb910bab71b9e61993" + "d6fee3403a9c26f7e7eb3fac8c24d3a4" ], [ "LinkedList1.disjoint_from_list", @@ -230,7 +230,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "01bfc2ee122c69be570eb14a3bda3da2" + "7c4a2b6cf38ff550f7a40508008517ed" ], [ "LinkedList1.footprint", @@ -244,7 +244,7 @@ "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "55360ce5af8b50f87eaad840177390c5" + "37742ea6811a55e22880f6ac0cf3ea59" ], [ "LinkedList1.footprint", @@ -312,7 +312,7 @@ "typing_LinkedList1.footprint", "well-founded-ordering-on-nat" ], 0, - "da293e5aaf28fa028b2dc6418fbd0ec9" + "c86b5112a53d78f676e65fbfb086d25e" ], [ "LinkedList1.footprint", @@ -327,7 +327,7 @@ "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, - "8b12bbbaa4d0f2180bb34d5107a35f51" + "453a591ebcf953b624706a127915eff8" ], [ "LinkedList1.modifies_disjoint_footprint", @@ -444,7 +444,7 @@ "well-founded-ordering-on-nat" ], 0, - "31943e2dcc95755b2699d08b78ce4626" + "c36968589ec54034fbef55df1d8cd06b" ], [ "LinkedList1.modifies_disjoint_footprint", @@ -473,7 +473,7 @@ "typing_FStar.Monotonic.HyperStack.as_addr" ], 0, - "b4e89ef7df74bb10f81b9570635ac14b" + "e18d1b0de68628cf54e00b948013f8fc" ], [ "LinkedList1.well_formed_distinct_lengths_disjoint", @@ -544,7 +544,7 @@ "typing_LinkedList1.disjoint", "well-founded-ordering-on-nat" ], 0, - "772f4dbe4e80bb5436b16200d11f606c" + "050df14a9eda9172f5673014a323d15a" ], [ "LinkedList1.well_formed_distinct_lengths_disjoint", @@ -558,7 +558,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "d78a5d50eba765158e7072469015033b" + "ac0524378b66f4fc2e86774e8418f7f9" ], [ "LinkedList1.well_formed_gt_lengths_disjoint_from_list", @@ -636,7 +636,7 @@ "well-founded-ordering-on-nat" ], 0, - "8fa8b271fe81abd115bdcecde6746f4b" + "4b9aa81385c0597bcd7e2e28314e4198" ], [ "LinkedList1.well_formed_gt_lengths_disjoint_from_list", @@ -648,7 +648,7 @@ "refinement_interpretation_Tm_refine_5d2eff6d62a1f8cf87698b717524ff0a" ], 0, - "7bf800217acd11686cc8441bbd16cc3f" + "0c7c6288eadd4c0f534c8e81cbd5b891" ], [ "LinkedList1.well_formed_head_tail_disjoint", @@ -714,7 +714,7 @@ "typing_LinkedList1.footprint", "unit_typing" ], 0, - "c068d1716dcd1875c5585a5c3e41e972" + "e99d2867bea152f9d247ab47b7cef419" ], [ "LinkedList1.unused_in_well_formed_disjoint_from_list", @@ -803,7 +803,7 @@ "well-founded-ordering-on-nat" ], 0, - "dfd3a8c6a694309b49dc3912ed0bcb33" + "ccfd7c577acffc1fdcb56577bdce961f" ], [ "LinkedList1.unused_in_well_formed_disjoint_from_list", @@ -815,7 +815,7 @@ "refinement_interpretation_Tm_refine_d13b0fb52a9600c17fa50bb483f44837" ], 0, - "fc2ef81496cbf11f1022a09eae430f9e" + "18455202e08dae3c63383a6e86bf2c45" ], [ "LinkedList1.pop", @@ -827,7 +827,7 @@ "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0" ], 0, - "4035c6e2a82644b2bca72a7f1b03e833" + "83750ae0c8dcec5686ae7f5e8ad66c0e" ], [ "LinkedList1.pop", @@ -959,7 +959,7 @@ "typing_LowStar.Monotonic.Buffer.loc_addresses" ], 0, - "1ded5dfd3383e3081bfcb8bff498c761" + "86240b38974dcf1a5bfd77bd196ea788" ], [ "LinkedList1.push", @@ -974,7 +974,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "c8e4837cb42061b4637601a380e886ae" + "0ff35e4c4e72bd9fba17ab564ae8763c" ], [ "LinkedList1.push", @@ -1119,7 +1119,7 @@ "typing_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs" ], 0, - "b09e861d80dee2090cc20f0a3fa2bfe1" + "a1cb58a06d652bc1375a82a7ffede8eb" ], [ "LinkedList1.length", @@ -1128,7 +1128,7 @@ 1, [ "@query" ], 0, - "bcfca7ab96bb9b77f357ba5656fc10ef" + "36dd8c3aca9cae74a979bea96fa03ef3" ], [ "LinkedList1.length", @@ -1194,7 +1194,7 @@ "typing_FStar.Monotonic.HyperStack.is_mm", "typing_FStar.UInt32.v" ], 0, - "719146071ddd0ede42bf0e7c10ac51ee" + "94b9bdda3551d34cf33c2dc1a0ca7688" ], [ "LinkedList1.main", @@ -1270,7 +1270,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "85f0fb10c6c908385764cf3954621e18" + "7e9773e7b7073246dda1b4c924b7efac" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList2.fst.hints b/test/.hints/LinkedList2.fst.hints index 32b8c782..77df8fc2 100644 --- a/test/.hints/LinkedList2.fst.hints +++ b/test/.hints/LinkedList2.fst.hints @@ -17,7 +17,7 @@ "well-founded-ordering-on-nat" ], 0, - "59b8727bce1e289a342888b9bdc93132" + "0569751919c785fc9a2d296719afb9e3" ], [ "LinkedList2.cons_nonzero_length", @@ -43,7 +43,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "fa2306920016d68c9d87de3953254b82" + "83106a9eaaf67935fb8d68ebedba07b1" ], [ "LinkedList2.length_functional", @@ -77,7 +77,7 @@ "well-founded-ordering-on-nat" ], 0, - "689b7c444dca62c665fea38b7525cde7" + "a0788906c919a746b75f7e9d09e236a6" ], [ "LinkedList2.length_functional", @@ -91,7 +91,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "387fd2a0d25b36091bcda8d5a076328f" + "21410ac3cfa93b26d9480a2dc2ccc8db" ], [ "LinkedList2.live_nil", @@ -121,7 +121,7 @@ "typing_FStar.Buffer.length", "typing_FStar.UInt32.v" ], 0, - "706ee7287959261e5fe1ac29120c4f3e" + "8593dd521eb1d2f460636dc13036a139" ], [ "LinkedList2.live_cons", @@ -164,7 +164,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "fe28d456a0e691f4f89a3e587ab2d2c3" + "6ad527f3ef230c96ba6308fbe18a1224" ], [ "LinkedList2.footprint", @@ -194,7 +194,7 @@ "well-founded-ordering-on-nat" ], 0, - "d0c5438a86d6f3f6c9f9546697571b39" + "e8ee13ffda3ea91072697de8f43a16c4" ], [ "LinkedList2.modifies_disjoint_footprint", @@ -255,7 +255,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "bba2f6c55ed8356a5bbd9513fd5ba24e" + "f3bb9bbda26f11abece24d450f7a3b7e" ], [ "LinkedList2.modifies_disjoint_footprint", @@ -267,7 +267,7 @@ "refinement_interpretation_Tm_refine_1a7a399b01bde27a9da612a33e4f7eff" ], 0, - "ab4bf01f0fe0767fbbbcc35243298e5f" + "6b391ff00d4687093403d15e9e0ab1e9" ], [ "LinkedList2.well_formed_distinct_lengths_disjoint", @@ -322,7 +322,7 @@ "well-founded-ordering-on-nat" ], 0, - "53b3b6a0caee831cad73221a988e6c69" + "7782ef6c41f9f134549025b324d9942f" ], [ "LinkedList2.well_formed_distinct_lengths_disjoint", @@ -336,7 +336,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "085a127564c45e9e3f5dfaa1d937be93" + "375df0f88e0ad01407320979ccc71966" ], [ "LinkedList2.well_formed_gt_lengths_disjoint_from_list", @@ -395,7 +395,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "55eff2cf9b91d2b01386c2451adde452" + "70e23a8a703dfdc300f62c9969b3e067" ], [ "LinkedList2.well_formed_gt_lengths_disjoint_from_list", @@ -407,7 +407,7 @@ "refinement_interpretation_Tm_refine_c81c79fe6d6f45972f0574fd4ca431db" ], 0, - "ec17a28b6f1cf0743006e91cfa8aec8b" + "1e1a469cae6a6c331acc645a38d71cf2" ], [ "LinkedList2.well_formed_head_tail_disjoint", @@ -453,7 +453,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "c098a16327db11932c5cd216f08f3956" + "6bbd70f0b38262cca0a09bc20f55a895" ], [ "LinkedList2.unused_in_well_formed_disjoint_from_list", @@ -511,7 +511,7 @@ "typing_LinkedList2.footprint", "well-founded-ordering-on-nat" ], 0, - "0b022f5338e582664f12e519059b0520" + "08d560f66ee35cf9ce7794f43312f7af" ], [ "LinkedList2.unused_in_well_formed_disjoint_from_list", @@ -523,7 +523,7 @@ "refinement_interpretation_Tm_refine_71060f1b21c11070c805e09158382b50" ], 0, - "fecd0c82fefa6f45b3c7757f18e224cc" + "6fa6ccbaa3d98c11950879312cfeac30" ], [ "LinkedList2.pop", @@ -539,7 +539,7 @@ "refinement_interpretation_Tm_refine_610746826f8faaaa969bcb2a27509311" ], 0, - "4acf4504896436e412f382756d311774" + "d461cc965e5ca2a7e0c912ba44f61904" ], [ "LinkedList2.pop", @@ -605,7 +605,7 @@ "typing_LinkedList2.footprint", "typing_LinkedList2.t" ], 0, - "85a31c88133da9ffa6251edf5d3f8267" + "1d9173ff7653bc0a36fc56168d025639" ], [ "LinkedList2.push", @@ -622,7 +622,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "5b3202f4c148a66a4c05f2b5360f4d00" + "2b0215f10f340f0c6a25202b06142bf2" ], [ "LinkedList2.push", @@ -735,7 +735,7 @@ "typing_LinkedList2.footprint", "typing_LinkedList2.t" ], 0, - "e892359506f876b7d9c87851cab0a63f" + "56c3f39a6a7c7fc85f98c2154fe77555" ], [ "LinkedList2.length", @@ -744,7 +744,7 @@ 1, [ "@query" ], 0, - "fb43654ca03fc5c6bd52b9e8df322e85" + "63ffbdce00a4621f9d4d97bd7aa046fc" ], [ "LinkedList2.length", @@ -807,7 +807,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v" ], 0, - "efb42d06cae0ae5bb944b2cc38fada34" + "7d7fb0a63f64c5417dce751b2d58fa4b" ], [ "LinkedList2.main", @@ -883,7 +883,7 @@ "typing_FStar.UInt32.v", "typing_LinkedList2.t" ], 0, - "a5fcc3fc48f57af389ca183535fd96c0" + "a76e50529d395090f0346b13ef8b068a" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList3.fst.hints b/test/.hints/LinkedList3.fst.hints index 2b7965b4..b8bea63f 100644 --- a/test/.hints/LinkedList3.fst.hints +++ b/test/.hints/LinkedList3.fst.hints @@ -17,7 +17,7 @@ "well-founded-ordering-on-nat" ], 0, - "9bf5118826203caf9dc479f8175016b1" + "7090578ddbc6002bff853c449916def5" ], [ "LinkedList3.cons_nonzero_length", @@ -49,7 +49,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null" ], 0, - "3a34e337f590fe56fb49599f03765c00" + "eca96a25433c98d33f6d3f9d0f64430b" ], [ "LinkedList3.length_functional", @@ -84,7 +84,7 @@ "well-founded-ordering-on-nat" ], 0, - "2d367285a143a667ff0fe3e9392db05e" + "8f8ac50fa888bbfa75d9e4e9781151da" ], [ "LinkedList3.length_functional", @@ -98,7 +98,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "5befc8118f73d9a580408741fde06d21" + "b3571fd82f0fa0ccfee67703204f8e50" ], [ "LinkedList3.live_nil", @@ -130,7 +130,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "1ed6905bc97ca7e892d69ce37483f53e" + "49594c9bb280fdf89eb5f3e74a0bcbac" ], [ "LinkedList3.live_cons", @@ -175,7 +175,7 @@ "typing_LowStar.Monotonic.Buffer.get" ], 0, - "3cd4886329ca161f717e64b3b9f7b85a" + "9573260767ecbf5297ac18c918dc5d0d" ], [ "LinkedList3.footprint", @@ -205,7 +205,7 @@ "well-founded-ordering-on-nat" ], 0, - "397f0751b6b19809970568816cce5f4e" + "cc1e06ac251f2711a0e44366080271ea" ], [ "LinkedList3.modifies_disjoint_footprint", @@ -256,7 +256,7 @@ "well-founded-ordering-on-nat" ], 0, - "21fe7f54f7aa3dd8c9055b53527c3ed1" + "75deacf25a6e7124ba4a6b5374dbfff7" ], [ "LinkedList3.modifies_disjoint_footprint", @@ -268,7 +268,7 @@ "refinement_interpretation_Tm_refine_0b57dddc68898b9619355f21ce0c9e40" ], 0, - "337f2996860a5df94f45c93f351127bf" + "4f27be72da4a3e3ff653659847ae7abe" ], [ "LinkedList3.well_formed_distinct_lengths_disjoint", @@ -326,7 +326,7 @@ "well-founded-ordering-on-nat" ], 0, - "fa8191ef0b0e53c2289e594342e26341" + "568deb8f3563c71900832a34f6005a93" ], [ "LinkedList3.well_formed_distinct_lengths_disjoint", @@ -340,7 +340,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "ac42c8f3207837f7a706e89b8aaeef4f" + "803d9420b57d78ebbe818a46a7a07134" ], [ "LinkedList3.well_formed_gt_lengths_disjoint_from_list", @@ -397,7 +397,7 @@ "well-founded-ordering-on-nat" ], 0, - "9ed3314ec986fc7de1579fa64e69a3bb" + "162c3b39e00a04550b6d69aa8eac0518" ], [ "LinkedList3.well_formed_gt_lengths_disjoint_from_list", @@ -409,7 +409,7 @@ "refinement_interpretation_Tm_refine_26e4ab6728a562f67991d35daefeca22" ], 0, - "c2d8ac537c0992711699ef3dbdfb60a9" + "10cf58a109be0307f7973cc7333c027d" ], [ "LinkedList3.well_formed_head_tail_disjoint", @@ -449,7 +449,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "bfebc00729e07c8e2fe9e02f6888bfcf" + "7aadaa68c21fb48aa4f3d472148b26d5" ], [ "LinkedList3.unused_in_well_formed_disjoint_from_list", @@ -524,7 +524,7 @@ "well-founded-ordering-on-nat" ], 0, - "7607fc19e2e768cbe0a2b631c5b93fc3" + "911aa8610e15938ebbb0e6c631061274" ], [ "LinkedList3.unused_in_well_formed_disjoint_from_list", @@ -536,7 +536,7 @@ "refinement_interpretation_Tm_refine_7861eb32c6fa156a1b5a5b9496f25f14" ], 0, - "6164f9c31dd8931e30f657d77fce7c59" + "670a28749adb89acbf371ed11b413f1d" ], [ "LinkedList3.pop", @@ -551,7 +551,7 @@ "refinement_interpretation_Tm_refine_849dd87a0704847cf995021569fd0af6" ], 0, - "efbbf9d567f41aeae8e6f000befbdb68" + "5a955192d6ed981fa0abdabfa07526cf" ], [ "LinkedList3.pop", @@ -606,7 +606,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "8dadb8b82f8be1109aec3d205aaa1cc9" + "4e8c458cf567ccbad7175d4fed7b3ccb" ], [ "LinkedList3.push", @@ -623,7 +623,7 @@ "typing_FStar.Ghost.reveal" ], 0, - "c2b9b5cf0079722800299a4603dc271e" + "433aaa33f0568ff19f0dfa82b1119506" ], [ "LinkedList3.push", @@ -724,7 +724,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "8e83a85dd1d0cb750a221bea19b768e0" + "97897c3d1d956106c1e94503e6b6491a" ], [ "LinkedList3.length", @@ -733,7 +733,7 @@ 1, [ "@query" ], 0, - "10665a4682563a12baf22b357745c83d" + "6b287d160be198e7dc3598703a76fdbe" ], [ "LinkedList3.length", @@ -789,7 +789,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "c78594682a7eedd6c439fccc14581832" + "cdadb0b915f7b5cc91110f00b1931d9e" ], [ "LinkedList3.main", @@ -861,7 +861,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "ebd9c3af0834a4b2b187389796ff593b" + "484b1070b48a15bb83138dda5fd4bb7e" ] ] ] \ No newline at end of file diff --git a/test/.hints/LinkedList4.fst.hints b/test/.hints/LinkedList4.fst.hints index a833e6e5..bae2131f 100644 --- a/test/.hints/LinkedList4.fst.hints +++ b/test/.hints/LinkedList4.fst.hints @@ -13,7 +13,7 @@ "projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "59a1319af58d4e0201d51086fec58654" + "848b5c2b67496a88a2c5281ab2d77a2d" ], [ "LinkedList4.length_functional", @@ -53,7 +53,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "8697e8de3074dd9e57d85d2dd668e7d0" + "040df2b9b29ac85715d7fee8fd1076ac" ], [ "LinkedList4.footprint", @@ -80,7 +80,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "f53332f62298731de073430f7d121822" + "3a1a7648ceee9678d164fc0da24de8de" ], [ "LinkedList4.modifies_disjoint_footprint", @@ -134,7 +134,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "0ea24a9347f5d66331ab0b3137c86251" + "08b9b9d1a629111c249a0067d31bbd94" ], [ "LinkedList4.modifies_disjoint_footprint", @@ -146,7 +146,7 @@ "refinement_interpretation_Tm_refine_d727ca06ab1d2e19ab86ac8a0ebec43a" ], 0, - "0ee7d7c64e03d8cf33afa208fac6a01b" + "4bcdf1eba80d86bfa0b51a807862dc1d" ], [ "LinkedList4.well_formed_distinct_lengths_disjoint", @@ -200,7 +200,7 @@ "well-founded-ordering-on-nat" ], 0, - "2847649be618c5dca438a84021398a34" + "97f5edc354c5430963c8dc2742c2e20f" ], [ "LinkedList4.well_formed_distinct_lengths_disjoint", @@ -214,7 +214,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "b0f9103e60df0c4fea0bc721e58c821f" + "3a0691cb5c09318f5ba8a57c035efc43" ], [ "LinkedList4.well_formed_gt_lengths_disjoint_from_list", @@ -282,7 +282,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "ef89c1dc94e0cd82476d94f9c6cd5970" + "879d2cbb7cb21d42017e587c9d5ae401" ], [ "LinkedList4.well_formed_gt_lengths_disjoint_from_list", @@ -294,7 +294,7 @@ "refinement_interpretation_Tm_refine_7a66ed8ab1149aa32c4f07ae5b36b85c" ], 0, - "2a65c4e19fca5bc53f69129489a7d041" + "cd19a8960c516b5bd0f984f779ee8fe8" ], [ "LinkedList4.well_formed_head_tail_disjoint", @@ -327,7 +327,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "6d04c38b3049c46780f45a962baf5c39" + "6378c9159c5b49bf43d36ae1cf033aad" ], [ "LinkedList4.unused_in_well_formed_disjoint_from_list", @@ -406,7 +406,7 @@ "typing_Prims.uu___is_Nil" ], 0, - "46fbc747ff3dc5a0a2404b3290dfa7f1" + "3462628067aacae12ab8e7bb4f6af947" ], [ "LinkedList4.unused_in_well_formed_disjoint_from_list", @@ -418,7 +418,7 @@ "refinement_interpretation_Tm_refine_d06d91ecfb2529ebdc073668be613711" ], 0, - "d31ecf03ff1d252ab4691f2155cf1195" + "172de4bbcaaaaa08d1047b97781e4f81" ], [ "LinkedList4.pop", @@ -433,7 +433,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "95f8e9ffdf3eb67171ac9f0fcf520efe" + "950fb809bd827042f35f1216a34cf4da" ], [ "LinkedList4.pop", @@ -488,7 +488,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "f5ececb1d3bdb925041cb74ca651ee5a" + "4defbb24677119a52fd7d0598dd733ae" ], [ "LinkedList4.push", @@ -502,7 +502,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "c2d3297af1927f3629a2f5ead6342824" + "e24113dc83659e895b6ac1ffe74a5321" ], [ "LinkedList4.push", @@ -612,7 +612,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "bed5a78e4e42bf9c9770212414fb2167" + "db22cb87367f8923b3ceca074d0ef4d0" ], [ "LinkedList4.length", @@ -621,7 +621,7 @@ 1, [ "@query" ], 0, - "0f1a09607f085f7f69440a0898b2aa95" + "538f6b3a7ecf9422bcd8eae86046455f" ], [ "LinkedList4.length", @@ -682,7 +682,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "13078c8ac44fea4d4691e515f9e5a349" + "5e30789ea0fd9c1ee6be13174b77ee54" ], [ "LinkedList4.main", @@ -761,7 +761,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "4657a1aa8e20af6d0d02e86f63efa318" + "b038718bcb2a3f49b46d88ba69fb3d5c" ] ] ] \ No newline at end of file diff --git a/test/.hints/Literal.fst.hints b/test/.hints/Literal.fst.hints index 87a44c58..29439182 100644 --- a/test/.hints/Literal.fst.hints +++ b/test/.hints/Literal.fst.hints @@ -23,7 +23,7 @@ "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, - "aa16ab051e97c0ebb93fe5654cc22317" + "d2c53023e20ea41380c0e5a14e1bd9c4" ] ] ] \ No newline at end of file diff --git a/test/.hints/Loops.fst.hints b/test/.hints/Loops.fst.hints index f1458d2b..4282cecd 100644 --- a/test/.hints/Loops.fst.hints +++ b/test/.hints/Loops.fst.hints @@ -86,7 +86,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "5a7932d2b1efbe7248c078221b0a6c54" + "477957dda60da5b30c30c85572657bde" ], [ "Loops.sum_to_n_buf", @@ -190,7 +190,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "c4e2fd044b5c15fc637cb8bcb6b0f4d4" + "d98679d071f5683564fd490b9c85a0ae" ], [ "Loops.count_to_n", @@ -275,7 +275,7 @@ "typing_LowStar.Monotonic.Buffer.length" ], 0, - "fa90d40eaf452fa608b7d16f859fcd09" + "ce8de5fd981a9b5fbce825c3b948091e" ], [ "Loops.wait_for_false", @@ -305,7 +305,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "6bbb5b882804c761007cecfa9c53fc1b" + "241b9ff2b5133afb89753a3cbaf8b3d6" ], [ "Loops.test_pre", @@ -314,7 +314,7 @@ 1, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, - "fdd70d730bc243fb5e890a7b033e8f9e" + "bde3b8ad671299aeb215ac65eb0b2c93" ], [ "Loops.test_post", @@ -323,7 +323,7 @@ 1, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, - "a1dc81b62d33deefcf30950c4007777e" + "5048778d31c652bebab5ad83aa233129" ], [ "Loops.square_while", @@ -448,7 +448,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "7b164852787ea69fa3db89cce2d49507" + "b1e6e792be77f4d72517d60eda0113e2" ], [ "Loops.test_map", @@ -562,7 +562,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "0177dba8a6f6631b0aaff131596cfe17" + "010cef836b56971dc16deab8028e6464" ], [ "Loops.main", @@ -660,7 +660,7 @@ "typing_LowStar.Monotonic.Buffer.len", "typing_Prims.pow2" ], 0, - "b4352638c691998b33c420ee8161bec0" + "cce0f77f668a7692e003360f4d245210" ] ] ] \ No newline at end of file diff --git a/test/.hints/ML16.fst.hints b/test/.hints/ML16.fst.hints index c3d85421..c5e56a7d 100644 --- a/test/.hints/ML16.fst.hints +++ b/test/.hints/ML16.fst.hints @@ -68,7 +68,7 @@ "typing_FStar.UInt32.v" ], 0, - "f1d77fbaf572053fae972da497de8ff3" + "0d5791df980927b4c92acbea247f121a" ], [ "ML16.test2", @@ -131,7 +131,7 @@ "typing_FStar.UInt32.v" ], 0, - "961251fcae2487d9af03f5c5fd13681b" + "4720271ddb3f8b6309e0478045ef9a84" ], [ "ML16.main", @@ -208,7 +208,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "c2913b9ab12b61cdd075d2aefe0e9b3d" + "af68fcd684da28213280a7bf8b4e2a17" ] ] ] \ No newline at end of file diff --git a/test/.hints/Macro.fst.hints b/test/.hints/Macro.fst.hints index d43e9ec1..aba5c2b1 100644 --- a/test/.hints/Macro.fst.hints +++ b/test/.hints/Macro.fst.hints @@ -24,7 +24,7 @@ "typing_Prims.pow2" ], 0, - "0cca94bb68b21e1df0eea89a049a148d" + "4a32ac2cc45d1e930e4e352401a45f13" ] ] ] \ No newline at end of file diff --git a/test/.hints/MallocFree.fst.hints b/test/.hints/MallocFree.fst.hints index 46d0d9e3..9b3c86f6 100644 --- a/test/.hints/MallocFree.fst.hints +++ b/test/.hints/MallocFree.fst.hints @@ -83,7 +83,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "6383e216eba46595135cb03f18092d6e" + "554651dcdb44e03698a92c641393fa44" ] ] ] \ No newline at end of file diff --git a/test/.hints/MemCpy.fst.hints b/test/.hints/MemCpy.fst.hints index 175f25ac..cb400bc1 100644 --- a/test/.hints/MemCpy.fst.hints +++ b/test/.hints/MemCpy.fst.hints @@ -36,7 +36,7 @@ "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length" ], 0, - "7b584629460e343e4dcb412cd9143364" + "ec4edee5a38ea1a61c12b25d4e7f2ef4" ], [ "MemCpy.memcpy", @@ -45,7 +45,7 @@ 0, [ "@query" ], 0, - "db42ecbb6f1e61db5f105279e92b806d" + "1147482f00a4a794b140db392a3873cc" ], [ "MemCpy.memcpy", @@ -96,7 +96,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "b84a87da9bc9756b2598476a14fe7043" + "0852dff833ae4697572a07f32c21bb39" ], [ "MemCpy.main", @@ -192,7 +192,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "34ecbede838f93cc2881054f2c6508bf" + "9b9a87661aec7c51a6e1bc4823ab4308" ] ] ] \ No newline at end of file diff --git a/test/.hints/MemCpyModel.fst.hints b/test/.hints/MemCpyModel.fst.hints index 62dbad03..6672ba88 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, - "f7101c826c58c92e30a5dc19f00d0029" + "c4407d82acc876c39b789a39998a45bd" ], [ "MemCpyModel.memcpy", @@ -125,7 +125,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "0610d9841e55340b28190b3324799c4e" + "8ca4e11beb860c84f14ea3e3bb490833" ] ] ] \ No newline at end of file diff --git a/test/.hints/Mini.fst.hints b/test/.hints/Mini.fst.hints index 5ca74841..67497dd0 100644 --- a/test/.hints/Mini.fst.hints +++ b/test/.hints/Mini.fst.hints @@ -11,7 +11,7 @@ "refinement_interpretation_Tm_refine_8fd6f269a3ccd743e70c909024d76576" ], 0, - "eb5e216e824de395363525941ac4ca55" + "38a99732b3b92ae3978b143d9e8a37c3" ], [ "Mini.g", @@ -37,7 +37,7 @@ "typing_FStar.UInt32.v" ], 0, - "cf4c3068cef22aeac6f51aecfa53ab40" + "b4c75ea1eb3c1c51e747a52fecea4249" ] ] ] \ No newline at end of file diff --git a/test/.hints/MonomorphizationCrash.fst.hints b/test/.hints/MonomorphizationCrash.fst.hints index 810498e7..fb0cc631 100644 --- a/test/.hints/MonomorphizationCrash.fst.hints +++ b/test/.hints/MonomorphizationCrash.fst.hints @@ -12,7 +12,7 @@ "typing_Abstract.t" ], 0, - "c9e4db8df4bf2349bb808454198820e8" + "86a0dbd0cae1f6fe84eb12aab63233b2" ], [ "MonomorphizationCrash.test", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_MonomorphizationCrash.pair__uu___haseq" ], 0, - "013a61d77a220495043b1366b8d228d0" + "994d96c79afb0d179a2e83a757afb442" ] ] ] \ No newline at end of file diff --git a/test/.hints/MutRec.fst.hints b/test/.hints/MutRec.fst.hints index ad93530b..63704614 100644 --- a/test/.hints/MutRec.fst.hints +++ b/test/.hints/MutRec.fst.hints @@ -11,7 +11,7 @@ "proj_equation_FStar.Buffer.MkBuffer_length" ], 0, - "108a46f89f2ea124a23091e4b805c750" + "a801a8b11a055da13d114f9dee1d97c3" ], [ "MutRec.f", @@ -66,7 +66,7 @@ "typing_FStar.Set.singleton" ], 0, - "660468bd096e62380e33cae426124610" + "4827d823fcf6ca92f724a3721a8a10cf" ], [ "MutRec.f1", @@ -98,7 +98,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "de7c88c6eeea5c582578e6229cda196a" + "e3111b85f9fe839015044c28928203ff" ], [ "MutRec.f1", @@ -130,7 +130,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "34215c60dcf401c9f072a706e60c584c" + "e3111b85f9fe839015044c28928203ff" ], [ "MutRec.main", @@ -143,7 +143,7 @@ "refinement_interpretation_Tm_refine_e89747788e3bddb72132ff6bc99864af" ], 0, - "8f7b26753cdc7889705e7b23047b6145" + "6fc210a2f917a4ad469b71bfd3361cae" ] ] ] \ No newline at end of file diff --git a/test/.hints/NameCollisionHelper.fst.hints b/test/.hints/NameCollisionHelper.fst.hints index 5dbdcbdf..9aac14df 100644 --- a/test/.hints/NameCollisionHelper.fst.hints +++ b/test/.hints/NameCollisionHelper.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "a3fb5a45159a270071164570985c4a95" + "f59870cfcdff47dd30f7ae8e3fc477c0" ] ] ] \ No newline at end of file diff --git a/test/.hints/NoExtract.fst.hints b/test/.hints/NoExtract.fst.hints index 0395e951..e820c080 100644 --- a/test/.hints/NoExtract.fst.hints +++ b/test/.hints/NoExtract.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "2d6ba5212a82a9bf7628a895e36f2df9" + "cf74fdb59e2a4ee89280097b362aedff" ], [ "NoExtract.b", @@ -25,7 +25,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "8a3f2dd156d7b78f416c1b5ddfdad97e" + "5e14b6ee0314b70215cb511c6c2f9ef8" ] ] ] \ No newline at end of file diff --git a/test/.hints/NoShadow.fst.hints b/test/.hints/NoShadow.fst.hints index b70cf7ca..c21c1e48 100644 --- a/test/.hints/NoShadow.fst.hints +++ b/test/.hints/NoShadow.fst.hints @@ -22,7 +22,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "ccce40d91d63913a1176b9202ec7e5f1" + "bdb3c44cf5ebe626f83321334e76ca48" ], [ "NoShadow.g", @@ -45,7 +45,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "77a203d8be54cf41aea81a39e3a26eff" + "fd8a5a6adeeafccc5a2aa65d4160ea8e" ], [ "NoShadow.b", @@ -66,7 +66,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "6bd3cf62daf125e092774a27922e5750" + "e90c648f18921bfa8fc56d1bd0632ac1" ], [ "NoShadow.h", @@ -122,7 +122,7 @@ "typing_FStar.Set.singleton" ], 0, - "3c8a0197a8f3d87b4f42d815ed14e576" + "571485f06979a523c2e956a0b7695f03" ], [ "NoShadow.main", @@ -147,7 +147,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "3d17db08d748f417f269654a97754fa2" + "f16af4b769fe2aee18b4710cf5c1dcdf" ] ] ] \ No newline at end of file diff --git a/test/.hints/Null.fst.hints b/test/.hints/Null.fst.hints index fbfef921..23160c5c 100644 --- a/test/.hints/Null.fst.hints +++ b/test/.hints/Null.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc" ], 0, - "b5d303c4e488a4b96e73edf210ed0222" + "565f14aea76b1989193e45852180fb9e" ], [ "Null.main", @@ -31,7 +31,7 @@ "typing_LowStar.Monotonic.Buffer.mnull" ], 0, - "aff57b7fe51f03e6ac0baef9a9c86d77" + "1015c9b799bdcd88484db88d4de8a0dd" ] ] ] \ No newline at end of file diff --git a/test/.hints/OptimizedOption.fst.hints b/test/.hints/OptimizedOption.fst.hints index 8a7ea3a5..a2cfb305 100644 --- a/test/.hints/OptimizedOption.fst.hints +++ b/test/.hints/OptimizedOption.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "99225567d3311206cde75946f37c95ce" + "19f254d8b47b5200efc516f4f6664d05" ] ] ] \ No newline at end of file diff --git a/test/.hints/ParamAbbrev.fst.hints b/test/.hints/ParamAbbrev.fst.hints index f3c29926..c7656619 100644 --- a/test/.hints/ParamAbbrev.fst.hints +++ b/test/.hints/ParamAbbrev.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "8dea70e2e4b20bbbf6ace2be7e93b066" + "ea57d1f1071e2629f24f276689c548be" ], [ "ParamAbbrev.g", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "88ca4276d7b0f4a4d5942b1663b5608d" + "b8118c8a9775f7c74e5cb27343d07d96" ], [ "ParamAbbrev.touch", @@ -62,7 +62,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d0e4967622d3ed3edf7c76913be485fe" + "9acbd2b8fe5ec4581d40618a25d23531" ], [ "ParamAbbrev.main", @@ -88,7 +88,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "1a0adb7c95e4d585bb7f6cbb8901813e" + "78d4eb966925fb4230e95ad03f895c70" ] ] ] \ No newline at end of file diff --git a/test/.hints/Parameterized.fst.hints b/test/.hints/Parameterized.fst.hints index 59d52146..50396be1 100644 --- a/test/.hints/Parameterized.fst.hints +++ b/test/.hints/Parameterized.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "6c7c3fb75125f03843514138c7655035" + "84e1be7c1c7701b1b33ae2c5acf375de" ], [ "Parameterized.get", @@ -25,7 +25,7 @@ "refinement_interpretation_Tm_refine_7661503e258cd8eb6e95252fc3102979" ], 0, - "899507d86aca0ba331f9cc155ff69ac7" + "b26d50018030da1aaf0ae8b6e6077fb3" ], [ "Parameterized.main", @@ -72,7 +72,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "9159e2ac86f19db34ed31599e595b1a6" + "ecaa137d87628e22a45572865ba3bba6" ] ] ] \ No newline at end of file diff --git a/test/.hints/PatternAny.fst.hints b/test/.hints/PatternAny.fst.hints index 59438326..8a8d0b5a 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, - "6c74f7d84709f60724906386e11f2199" + "368e14f6c7805ea77cb44d5d2b5c8299" ] ] ] \ No newline at end of file diff --git a/test/.hints/PolyComp.fst.hints b/test/.hints/PolyComp.fst.hints index 635235a7..cd5104a1 100644 --- a/test/.hints/PolyComp.fst.hints +++ b/test/.hints/PolyComp.fst.hints @@ -8,7 +8,7 @@ 1, [ "@query" ], 0, - "04c6c3787a97b8b69e07bd192f33550a" + "2a0791a071af34e10b55c46e54f8a653" ], [ "PolyComp.__proj__B__item___0", @@ -20,7 +20,7 @@ "refinement_interpretation_Tm_refine_ace5180d8b9c0680cccc5c56d8744ca7" ], 0, - "b29bf6ee2b16767aa9c00186ad3a8326" + "0d402bee549579bfb18ea678b3812666" ], [ "PolyComp.one_t", @@ -33,7 +33,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "60a6393d3080d07e0ce04c87b8d4fa4c" + "dc1023084347df3a81418c16014aea59" ], [ "PolyComp.another_t", @@ -46,7 +46,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "10338fe95da1d62e26cea3b9ae32ea53" + "7d9aba486fdc15ebeaebf904f08cfc89" ], [ "PolyComp.yet_another_t", @@ -59,7 +59,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "4ab155f08f901fad84487dd0e9d2e33d" + "c28d175d24cbfc6c0d7cf05cb2894a88" ], [ "PolyComp.main", @@ -86,7 +86,7 @@ "typing_FStar.Int32.t", "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "01171725aa3fe6ac2b0e38d549765bec" + "2c06e477c3648beb8aa6c6e9724eb6c2" ] ] ] \ No newline at end of file diff --git a/test/.hints/Polymorphic.fst.hints b/test/.hints/Polymorphic.fst.hints index 133ca2f7..26d12a73 100644 --- a/test/.hints/Polymorphic.fst.hints +++ b/test/.hints/Polymorphic.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "df88093030ae9a633f6c6f107ccf0aa7" + "0428b26b917aaead9736b8bafadb6bcd" ], [ "Polymorphic.main", @@ -46,7 +46,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "fb77ef252e55db7f60d5b1fd6abd4ee7" + "c2519c968206fa7864d58ee4b2773c84" ] ] ] \ No newline at end of file diff --git a/test/.hints/Printf.fst.hints b/test/.hints/Printf.fst.hints index 84bc88f6..0e99b3b0 100644 --- a/test/.hints/Printf.fst.hints +++ b/test/.hints/Printf.fst.hints @@ -85,7 +85,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "408d8dbd4b74f69fde9634358c27d1f0" + "be3730f7d20f873a11d39cbd6d467d2d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Private.fst.hints b/test/.hints/Private.fst.hints index 19c36507..86815d6f 100644 --- a/test/.hints/Private.fst.hints +++ b/test/.hints/Private.fst.hints @@ -46,7 +46,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "5b23bb69cd571dfc6907a0374f13467f" + "7964b8302c52f55c58066cb46de51dfd" ] ] ] \ No newline at end of file diff --git a/test/.hints/PrivateInclude1.fst.hints b/test/.hints/PrivateInclude1.fst.hints index c2700695..5ce74833 100644 --- a/test/.hints/PrivateInclude1.fst.hints +++ b/test/.hints/PrivateInclude1.fst.hints @@ -26,7 +26,7 @@ "typing_Prims.pow2", "typing_PrivateInclude1.foobar" ], 0, - "881a436c6a7d4bf5c27ac63a9486d7d0" + "3850d2d5fcce9305cd5819e4328c0f16" ] ] ] \ No newline at end of file diff --git a/test/.hints/PrivateInclude2.fst.hints b/test/.hints/PrivateInclude2.fst.hints index 63146645..0a535c5a 100644 --- a/test/.hints/PrivateInclude2.fst.hints +++ b/test/.hints/PrivateInclude2.fst.hints @@ -21,7 +21,7 @@ "typing_FStar.Int32.v", "typing_PrivateInclude1.f", "unit_typing" ], 0, - "806f6369b24a126bfeb3e5885feaa2cb" + "343d56b361c7983127ebe83e4a5e39ae" ] ] ] \ No newline at end of file diff --git a/test/.hints/PushPop.fst.hints b/test/.hints/PushPop.fst.hints index 30855e42..07a29159 100644 --- a/test/.hints/PushPop.fst.hints +++ b/test/.hints/PushPop.fst.hints @@ -48,7 +48,7 @@ "typing_FStar.Set.union" ], 0, - "72b91960e388e1aca7ecd83ba15e2526" + "8122e8a539cfcfb6a1f8c4ab03e69076" ], [ "PushPop.main", @@ -80,7 +80,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "8282a4dd83c51bf7d033975fbc1d40d5" + "057f035dd3045c051a1bdb7fde43ec69" ] ] ] \ No newline at end of file diff --git a/test/.hints/RecordTypingLimitation.fst.hints b/test/.hints/RecordTypingLimitation.fst.hints index 3a01bddf..6ff43c24 100644 --- a/test/.hints/RecordTypingLimitation.fst.hints +++ b/test/.hints/RecordTypingLimitation.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "b26a8038a6c32dc5a7a47fd9eb0c0a62" + "e2bf852dafb47ad7239525f6acad2d21" ] ] ] \ No newline at end of file diff --git a/test/.hints/Recursive.fst.hints b/test/.hints/Recursive.fst.hints index 5b680066..27bf3f0e 100644 --- a/test/.hints/Recursive.fst.hints +++ b/test/.hints/Recursive.fst.hints @@ -11,7 +11,7 @@ "refinement_interpretation_Tm_refine_fe78738bbffac158d58c53f89b03a1b7" ], 0, - "55797e9ce97de340549422a493d838a7" + "6520db4db79b7b470879034f24f7b42d" ], [ "Recursive.__proj__Cons__item__next", @@ -23,7 +23,7 @@ "refinement_interpretation_Tm_refine_fe78738bbffac158d58c53f89b03a1b7" ], 0, - "1905930be68c873a8b01030134236a00" + "ef1929e0ac4dc349da7ce60c3e63a451" ] ] ] \ No newline at end of file diff --git a/test/.hints/RecursivePoly.fst.hints b/test/.hints/RecursivePoly.fst.hints index cc8bbb91..fa4b1f2b 100644 --- a/test/.hints/RecursivePoly.fst.hints +++ b/test/.hints/RecursivePoly.fst.hints @@ -11,7 +11,7 @@ "refinement_interpretation_Tm_refine_ec0be7ef8d42c8c1f9f883ea579d9abf" ], 0, - "e454b8f93c9fed29775755363e7fe0d7" + "454e0ff2f9990d11229662e82486f514" ], [ "RecursivePoly.__proj__Cons__item__next", @@ -23,7 +23,7 @@ "refinement_interpretation_Tm_refine_ec0be7ef8d42c8c1f9f883ea579d9abf" ], 0, - "e75522589919b74e15e92a7e54aaa4d1" + "28642528c6a6619ab56314abedab3e62" ], [ "RecursivePoly.f", @@ -44,7 +44,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "b7defa883c94e490dd11bf3db769906e" + "984fe3393637b24c519502bf1cd4751f" ], [ "RecursivePoly.g", @@ -65,7 +65,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "77e2d12930ce1ba5bdcc2b22b4861c77" + "1c02a2102a9597d2381f92e2068d9327" ] ] ] \ No newline at end of file diff --git a/test/.hints/Renaming.fst.hints b/test/.hints/Renaming.fst.hints index ad8b307d..498efc18 100644 --- a/test/.hints/Renaming.fst.hints +++ b/test/.hints/Renaming.fst.hints @@ -15,7 +15,7 @@ "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2" ], 0, - "514251268b8cbc1def82666f6afbe8d8" + "76a5347b670da0ab9e3f683cee0eb43e" ], [ "Renaming.main", @@ -32,7 +32,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "fdb5f7a5cf1ae5821af225f183f0db57" + "e403a1bc54b139882b2e6e70b334461b" ] ] ] \ No newline at end of file diff --git a/test/.hints/RingBuffer.fst.hints b/test/.hints/RingBuffer.fst.hints index 458da44a..b9b626a2 100644 --- a/test/.hints/RingBuffer.fst.hints +++ b/test/.hints/RingBuffer.fst.hints @@ -12,7 +12,7 @@ "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, - "254683ee5f96378262e2102866088b56" + "6b4abeec6e96ed2537e8cc2e5360fc2f" ], [ "RingBuffer.well_formed_f", @@ -21,7 +21,7 @@ 1, [ "@query" ], 0, - "8b38328ca86b14abfe4f79787d885ecf" + "e8db89ef6ba9d9ff0bc5995e7ee4094d" ], [ "RingBuffer.next", @@ -48,7 +48,7 @@ "typing_FStar.UInt32.v" ], 0, - "3a1c7d24f9431692fd00a94c8781634f" + "46da87508120c0d1c1853ffd492888cd" ], [ "RingBuffer.prev", @@ -74,7 +74,7 @@ "typing_FStar.UInt32.v" ], 0, - "e98c81ee840b959e8a7b21ce4d58d5af" + "68d95cdd0cd95fb6b284d5c5fa5f6442" ], [ "RingBuffer.remaining_space", @@ -100,7 +100,7 @@ "typing_RingBuffer.__proj__Mkt__item__total_length" ], 0, - "6d8b561fa6a63ea7788c7055175efd62" + "baa6830ca8f014acb63236d2a5d240b0" ], [ "RingBuffer.as_list_f", @@ -141,7 +141,7 @@ "well-founded-ordering-on-nat" ], 0, - "823350488833c8998442cac7957e8d29" + "c9885bbec73cdc98a6a450173ac57922" ], [ "RingBuffer.as_list_f", @@ -150,7 +150,7 @@ 1, [ "@query" ], 0, - "8ba20d6e248625cbb5f97fcccc12e9be" + "4d392ac9272ceb457aaec1b0c3a4265e" ], [ "RingBuffer.seq_update_unused_preserves_list", @@ -206,7 +206,7 @@ "well-founded-ordering-on-nat" ], 0, - "4e8f0a2da89a7e6b10dcbe26c4cfdb2d" + "a49d2db5b50ac8be89a17a3053a03aff" ], [ "RingBuffer.seq_update_unused_preserves_list", @@ -230,7 +230,7 @@ "typing_FStar.UInt32.v" ], 0, - "390e49ca41c8df1361a4bf718c60fa61" + "53b074842e1231ab1c7f01e82a7cb12a" ], [ "RingBuffer.as_list", @@ -239,7 +239,7 @@ 1, [ "@query", "equation_RingBuffer.well_formed" ], 0, - "3d7aac94fd4349760002acd65815f715" + "0cf7a72c3c70f4fdd42ce43569d36b13" ], [ "RingBuffer.pop", @@ -333,7 +333,7 @@ "typing_RingBuffer.as_list", "typing_RingBuffer.remaining_space" ], 0, - "91a7857db383622fa5a436fae00fb446" + "83643384dddb4d546c6d271a521cc6ce" ], [ "RingBuffer.push", @@ -433,7 +433,7 @@ "typing_RingBuffer.remaining_space" ], 0, - "78b26d83fc24c58964c604c8372e7966" + "c80a9e80356f03779405d31cb348c60d" ], [ "RingBuffer.one_past_last", @@ -460,7 +460,7 @@ "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v" ], 0, - "e9d7c61a5060133a92c2145f09d4da29" + "147c5e2c4f8e76803d11b9bb1e9b38e4" ], [ "RingBuffer.as_list_append_one", @@ -528,7 +528,7 @@ "well-founded-ordering-on-nat" ], 0, - "f1eb54d240e7e2f0abe7abbb1472e485" + "d2af012c604aadc7b6caf2400ac90b9e" ], [ "RingBuffer.as_list_append_one", @@ -549,16 +549,16 @@ "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", - "refinement_interpretation_Tm_refine_0b151868311eefa5eb7ef60c3c4c576c", "refinement_interpretation_Tm_refine_3ee14c71093580f7e91b780f4a2f8a09", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_5ac5e5c81f0ca9a125077a9b7afb2743", + "refinement_interpretation_Tm_refine_87b8ef367f6ed95588e2d76aba7644b2", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.lt", "typing_FStar.UInt32.v", "typing_RingBuffer.one_past_last" ], 0, - "25ceba1212c53554235323d04b6e03ff" + "f1a3990b14ef9cbbc0c8358e6a490e4e" ], [ "RingBuffer.push_back", @@ -657,7 +657,7 @@ "typing_RingBuffer.as_list_f", "typing_RingBuffer.remaining_space" ], 0, - "ebdce3d12ef8e87f7966e1a7d8856129" + "cc0f12eaa19b8bdc54127c1a188c08e4" ], [ "RingBuffer.as_list_minus_one", @@ -728,7 +728,7 @@ "well-founded-ordering-on-nat" ], 0, - "dded9f42dbf9a9f927ae9a5ffa673419" + "b97c26dd469e04d36ac4808b80ee5518" ], [ "RingBuffer.as_list_minus_one", @@ -763,7 +763,7 @@ "typing_RingBuffer.prev" ], 0, - "1b5b7421c2717e0466b1b8f4b762a493" + "e4d1959bf69eaf778383b0305882cd6e" ], [ "RingBuffer.pop_back", @@ -841,7 +841,7 @@ "typing_RingBuffer.as_list_f", "typing_RingBuffer.remaining_space" ], 0, - "d5a92ab7d563ac8c3238dddbe8381929" + "fc1982c03c95bd58751c045fa42127e1" ], [ "RingBuffer.create", @@ -938,7 +938,7 @@ "typing_RingBuffer.remaining_space" ], 0, - "3574cc438257078c6596db0073b1beed" + "4a1799afc8a8e6735446a84896baccea" ], [ "RingBuffer.main", @@ -1052,7 +1052,7 @@ "typing_RingBuffer.space_left" ], 0, - "f3fda9d3ee1d604f064dc4e7c12c9ebb" + "eacf1990b1fad4daf1c7e3c3ac3e87f0" ] ] ] \ No newline at end of file diff --git a/test/.hints/Rust1.fst.hints b/test/.hints/Rust1.fst.hints index e24fd45b..62a94bce 100644 --- a/test/.hints/Rust1.fst.hints +++ b/test/.hints/Rust1.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "018d7bf5e794b12603f8d8695b3698f3" + "ca402a9671b7fbff0f6e83c74174ae90" ], [ "Rust1.two", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "62d6cdbb971cbdf176d9ccf34b0b0124" + "7b0a13c4cc28d98dac138d608321fb01" ], [ "Rust1.zero", @@ -62,7 +62,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "8f3a9a659f850489f98abc90d70c54d2" + "2467bd01e0a2cfde3afb4c3840b88b0d" ], [ "Rust1.doesnt_work", @@ -149,7 +149,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "525830c64db8eeae52c27b83276a7a78" + "46db7d0eb73c0b0e86eddb55c5bbf44b" ], [ "Rust1.does_work", @@ -236,7 +236,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "5c4860be20de92c43cbd863d7ab6f61b" + "0f8bc4b4d5adf8c77760c0075c4ff198" ], [ "Rust1.fully_static", @@ -326,7 +326,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "217f2a8943e498b5088ceb0adf106b26" + "0517448067c03f8befc0bf77ff377718" ], [ "Rust1.main", @@ -335,7 +335,7 @@ 0, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "75a82d92de11aa35d5eee6bf35354f56" + "ba5269dee7e00fcded2f0a5a7805da3a" ] ] ] \ No newline at end of file diff --git a/test/.hints/Scope.fst.hints b/test/.hints/Scope.fst.hints index 3c2f5ee4..3a3421aa 100644 --- a/test/.hints/Scope.fst.hints +++ b/test/.hints/Scope.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "e122a0a9bc10e0e7d4cd3d0793e4d2f8" + "74d2fed946f5dd8f36e74eb3ba1485f5" ], [ "Scope.main", @@ -97,7 +97,7 @@ "typing_FStar.Seq.Base.create", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "99686e284a4bf88885b839c0c3552e64" + "d1232284401d0c31534dfea782d11f63" ] ] ] \ No newline at end of file diff --git a/test/.hints/Server.fst.hints b/test/.hints/Server.fst.hints index 6024f6af..44bfdb0e 100644 --- a/test/.hints/Server.fst.hints +++ b/test/.hints/Server.fst.hints @@ -15,7 +15,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "ae25f685610606ac7f7136f25a8648cc" + "38c2050b0c6e5f1886fb1021d82ea839" ], [ "Server.bufstrcmp", @@ -36,7 +36,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "720e2d2aecbe3790d2067ff779e54bf3" + "e9b8f5ca935a974c346d73977faca843" ], [ "Server.bufstrcmp", @@ -192,7 +192,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "db99db6eb38ec5f2c21872d75c776f13" + "3da2ffd8391ae024752a82035fe39492" ], [ "Server.bufstrcpy", @@ -218,7 +218,7 @@ "typing_LowStar.Buffer.trivial_preorder" ], 0, - "28179eaa73c72d2a33d012c3264c0ce0" + "78e84c60e0a94a4ca3fbe3b74013d355" ], [ "Server.bufcpy", @@ -242,7 +242,7 @@ "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder" ], 0, - "ca5a8a5ac5b744cb26781221d0e5919f" + "88b7a30898bab7b4d39c0833ac36fa4b" ], [ "Server.respond", @@ -300,7 +300,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "b9bff04fdbb98f6e763dd3be7408fdc4" + "45dca7be56457ee8c5f5bfbc4ae4da6e" ], [ "Server.respond_index", @@ -412,7 +412,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "4d7bd5c45ae7e5a4123a3784b7b8fab7" + "c11bf1a3957c63f867fccd6263b43655" ], [ "Server.respond_stats", @@ -543,7 +543,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "8c709e15cc15e527db5b60e60b462efc" + "f7f5e35bacc510781ced8288935811b2" ], [ "Server.respond_404", @@ -676,7 +676,7 @@ "typing_LowStar.Monotonic.Buffer.loc_union" ], 0, - "22a59a19d488efa4127e49bd83301bcf" + "6836e38864b66236dace17ac1b13498b" ], [ "Server.server", @@ -815,7 +815,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_Prims.pow2" ], 0, - "0ba8cc40a721e70df10f7ca1dd412c84" + "22c1158cb940e1ac01710979a805b2d4" ] ] ] \ No newline at end of file diff --git a/test/.hints/Shift.fst.hints b/test/.hints/Shift.fst.hints index 00e4c4b8..a29624d9 100644 --- a/test/.hints/Shift.fst.hints +++ b/test/.hints/Shift.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "ec8146129b41fc027845b01adf1fddfb" + "df996c62954141541fc33e77102676fd" ], [ "Shift.main", @@ -94,7 +94,7 @@ "typing_FStar.UInt32.v", "typing_FStar.UInt8.v", "typing_Prims.pow2" ], 0, - "155e4b24786bc37dc8097cb9892227e9" + "52bd4c7aa6faa5056030b0b528c941ec" ] ] ] \ No newline at end of file diff --git a/test/.hints/SimpleWasm.fst.hints b/test/.hints/SimpleWasm.fst.hints index 14b92c68..5c1f100c 100644 --- a/test/.hints/SimpleWasm.fst.hints +++ b/test/.hints/SimpleWasm.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d10fe0598dbcc3ebcaaf819e6dbf14ab" + "b55050d7e24fab3175fd0843706a2a8f" ], [ "SimpleWasm.main", @@ -37,7 +37,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "2cc47692ac8fb8d38d9367a87ed54d57" + "4d2dc0a2f1f686ea8c9436b5eb3f71ed" ] ] ] \ No newline at end of file diff --git a/test/.hints/StaticHeaderLib.fst.hints b/test/.hints/StaticHeaderLib.fst.hints index 9372d8d8..572c64c5 100644 --- a/test/.hints/StaticHeaderLib.fst.hints +++ b/test/.hints/StaticHeaderLib.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "ea12d4c1cdfad0d9a3101f4a4fd1719c" + "23a38b83b03959260e841e2cd601038a" ], [ "StaticHeaderLib.private_helper", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "ef7cf738cda8cb5ba15a570efbf43f73" + "f9334ad3128f53d896e0e72d804237ea" ], [ "StaticHeaderLib.helper", @@ -42,7 +42,7 @@ 1, [ "@query", "typing_StaticHeaderLib.__proj__Mkt__item__x" ], 0, - "a4bbdb5274760b2036de9c36aa4312f9" + "cb86633a2eeaba9521a5bfb002b2e5b9" ] ] ] \ No newline at end of file diff --git a/test/.hints/StaticHeaderLib.fsti.hints b/test/.hints/StaticHeaderLib.fsti.hints index b171538a..3c863d5b 100644 --- a/test/.hints/StaticHeaderLib.fsti.hints +++ b/test/.hints/StaticHeaderLib.fsti.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "ea12d4c1cdfad0d9a3101f4a4fd1719c" + "23a38b83b03959260e841e2cd601038a" ], [ "StaticHeaderLib.private_helper", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "ef7cf738cda8cb5ba15a570efbf43f73" + "f9334ad3128f53d896e0e72d804237ea" ] ] ] \ No newline at end of file diff --git a/test/.hints/StringLit.fst.hints b/test/.hints/StringLit.fst.hints index 1f1a323c..fc6b7ce3 100644 --- a/test/.hints/StringLit.fst.hints +++ b/test/.hints/StringLit.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "fbc68ce12b4e446db06d0735e699cf8b" + "2381fc2a0c09132ad10e3113179afafa" ], [ "StringLit.cat", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d52d216044b9b6c5dd1d1e6168dbfa4b" + "b1bc67c52d572409f80e8a28b19ef4c9" ], [ "StringLit.test_c_string", @@ -50,7 +50,7 @@ 1, [ "@query" ], 0, - "771bfcc69acf2467cb77894597053724" + "9848bac5edd9cdcdef8ec26d16d5bccc" ], [ "StringLit.main", @@ -68,7 +68,7 @@ "typing_FStar.Int.Cast.uint8_to_int32" ], 0, - "02c0e1c78d62f8b19ec449d1b21d082b" + "f62ad82f6a7ba0f8907d42251acc6b22" ] ] ] \ No newline at end of file diff --git a/test/.hints/Strlen.fst.hints b/test/.hints/Strlen.fst.hints index 10868ffa..101d06cb 100644 --- a/test/.hints/Strlen.fst.hints +++ b/test/.hints/Strlen.fst.hints @@ -15,7 +15,7 @@ "typing_tok_C.EXIT_FAILURE@tok", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "09c07ac3f2f1427790202fd1dcdb6c59" + "a1c0d214225425eeaa3beb9494165e38" ] ] ] \ No newline at end of file diff --git a/test/.hints/Structs.fst.hints b/test/.hints/Structs.fst.hints index 5695127c..9c836273 100644 --- a/test/.hints/Structs.fst.hints +++ b/test/.hints/Structs.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int32.t" ], 0, - "471517faa6fbc541592b7010670092f7" + "a4bdc65753394037e9973cfe32fd9456" ], [ "Structs.f", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "5ba80f77409c4d599fa41f2e4c5edd1f" + "437d353369969fe937485205a2a30250" ], [ "Structs.main", @@ -45,7 +45,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "1e1d517c9ebf936301b97dc6e7dea268" + "979c5a9cb90e9d65302611bd66d69e30" ] ] ] \ No newline at end of file diff --git a/test/.hints/Structs2.fst.hints b/test/.hints/Structs2.fst.hints index 7f5291f8..e6b21c14 100644 --- a/test/.hints/Structs2.fst.hints +++ b/test/.hints/Structs2.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt8.t" ], 0, - "0d2678d737d62ae0e0064cc4df2a1afb" + "05763a9674b5eecbcf213d52cf7406df" ], [ "Structs2.point", @@ -25,7 +25,7 @@ "typing_FStar.UInt32.t" ], 0, - "0bf9965bc01373a7e471e279812477d5" + "040f19afc372b30c556809d8e00c8ac9" ], [ "Structs2.t", @@ -37,7 +37,7 @@ "assumption_Structs2.point__uu___haseq" ], 0, - "f41347cf0a56c549d6613a2da7a54b0d" + "c566c7699f4402958adfff3d011130a4" ], [ "Structs2.test1", @@ -58,7 +58,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "074d77443441163639967863dfd580eb" + "44053177341204474d5d717f56b9ef6f" ], [ "Structs2.main", @@ -84,7 +84,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "234d8f3d75e7bfb9fd595a07b5832f3f" + "0be4b5288e5048ec07216b772eee373f" ] ] ] \ No newline at end of file diff --git a/test/.hints/Substitute.fst.hints b/test/.hints/Substitute.fst.hints index c8d980f2..5213290b 100644 --- a/test/.hints/Substitute.fst.hints +++ b/test/.hints/Substitute.fst.hints @@ -21,7 +21,7 @@ "typing_FStar.Int32.t" ], 0, - "60975fbe54070bfbbbf93852ba07e262" + "7a8192d18675b62bb36233c9bbd9d6f0" ], [ "Substitute.main", @@ -72,7 +72,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "e96b571bf1a02f9d50ff2681ee3f90cf" + "55ee88880238c2e9de2e79901567dffd" ] ] ] \ No newline at end of file diff --git a/test/.hints/TailCalls.fst.hints b/test/.hints/TailCalls.fst.hints index d4c398c6..91389ec9 100644 --- a/test/.hints/TailCalls.fst.hints +++ b/test/.hints/TailCalls.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "a1b093cd273129ab41ef6d3040a3f12b" + "6d84f373d885a1709065fc458f032a93" ] ] ] \ No newline at end of file diff --git a/test/.hints/TailCalls2.fst.hints b/test/.hints/TailCalls2.fst.hints index 19b629ba..cfa6da33 100644 --- a/test/.hints/TailCalls2.fst.hints +++ b/test/.hints/TailCalls2.fst.hints @@ -23,7 +23,7 @@ "typing_FStar.Int32.v", "well-founded-ordering-on-nat" ], 0, - "313efbdc0ffab85031e81fdadd989955" + "0650ceb5fe232b09f868f5bf675acd19" ] ] ] \ No newline at end of file diff --git a/test/.hints/TestAlloca.fst.hints b/test/.hints/TestAlloca.fst.hints index f661726f..3e0e167f 100644 --- a/test/.hints/TestAlloca.fst.hints +++ b/test/.hints/TestAlloca.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "ea35c22cd9203516845508c748cd6e09" + "2c714b77ea77c6ab256ba89f98afdfd5" ], [ "TestAlloca.main", @@ -77,7 +77,7 @@ "typing_FStar.Set.singleton", "typing_FStar.UInt32.v" ], 0, - "7a46698db30354995d76fcd5a7bfb1fc" + "56ad07753e0685e031b9973869ab82ff" ] ] ] \ No newline at end of file diff --git a/test/.hints/TopLevelArray.fst.hints b/test/.hints/TopLevelArray.fst.hints index 7b21150e..33f6ca0d 100644 --- a/test/.hints/TopLevelArray.fst.hints +++ b/test/.hints/TopLevelArray.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "be9468eef0ff5d6fb0b33f1ad7917b3e" + "fbe0105de916f4d117915cbff64c909e" ], [ "TopLevelArray.y", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "58c629a28262563603439205a85ada99" + "5d3b81b2142401e00916bc09d0a1fdef" ], [ "TopLevelArray.x", @@ -84,7 +84,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "1c1087856d4408d54bbb521ccbcee588" + "653830eba29b5495cb9d903c8edf64ad" ], [ "TopLevelArray.g", @@ -93,7 +93,7 @@ 1, [ "@query" ], 0, - "f4b6f9896df535c6297773ba41b273b6" + "e69e6dec52f73b96414a85a4e96c4f09" ], [ "TopLevelArray.main", @@ -115,7 +115,7 @@ "typing_TopLevelArray.x" ], 0, - "b9fca437d064510e6ea0ae2c748366ca" + "ade6477c2e1fc99ffddfc3279c7bb36f" ] ] ] \ No newline at end of file diff --git a/test/.hints/TotalLoops.fst.hints b/test/.hints/TotalLoops.fst.hints index 7674bd38..0445db41 100644 --- a/test/.hints/TotalLoops.fst.hints +++ b/test/.hints/TotalLoops.fst.hints @@ -16,7 +16,7 @@ "well-founded-ordering-on-nat" ], 0, - "229b00107adee3e388f39052ed87a6ae" + "19b0828e7c02fe62aa628078542a3f60" ], [ "TotalLoops.t", @@ -30,7 +30,7 @@ "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, - "641db090b73ad458f9d9186e95c9f26b" + "ccf0a89c69b5ca2751f765368becf53a" ], [ "TotalLoops.tfib", @@ -70,7 +70,7 @@ "typing_TotalLoops.__proj__Mkt__item__i", "typing_TotalLoops.fib" ], 0, - "7db8b9ea5ec2d723f6755094b14ce21b" + "c7f3bacc4303d3fa7c4617768532d53c" ] ] ] \ No newline at end of file diff --git a/test/.hints/Tuples.fst.hints b/test/.hints/Tuples.fst.hints index 2a349ca2..ee79c61b 100644 --- a/test/.hints/Tuples.fst.hints +++ b/test/.hints/Tuples.fst.hints @@ -46,7 +46,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "e0d8932fd654aaae73292e4f3c9f74b7" + "bf05629b78daf917e9fa8c8dda2314b4" ] ] ] \ No newline at end of file diff --git a/test/.hints/UBuffer.fst.hints b/test/.hints/UBuffer.fst.hints index 00a0cbc6..25363ba3 100644 --- a/test/.hints/UBuffer.fst.hints +++ b/test/.hints/UBuffer.fst.hints @@ -98,7 +98,7 @@ "typing_LowStar.UninitializedBuffer.initialization_preorder" ], 0, - "fc4c08ee422d7c089228ce68359d5329" + "12b6c2082359b2b473dc75cccb61e1d0" ], [ "UBuffer.test_ub_stack", @@ -188,7 +188,7 @@ "typing_LowStar.UninitializedBuffer.initialization_preorder" ], 0, - "ef5ecdeed7e869ff8bb48d8f4067c1b6" + "56a5c2f16f64850e4f76130079e6989a" ], [ "UBuffer.main", @@ -213,7 +213,7 @@ "typing_FStar.Int32.int_to_t", "typing_Prims.pow2" ], 0, - "f9ce32ffd8b33fa27a47e8ad78151e33" + "9fdc51606ebfeed46e05181201ea0741" ] ] ] \ No newline at end of file diff --git a/test/.hints/Underspec.fst.hints b/test/.hints/Underspec.fst.hints index cff8de2f..2600b912 100644 --- a/test/.hints/Underspec.fst.hints +++ b/test/.hints/Underspec.fst.hints @@ -1,5 +1,5 @@ [ - "B/\u0002\u000fF\u0017Ѳz\u0006", + "I/H+\u007f3p", [ [ "Underspec.test1", @@ -36,7 +36,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "99dab526a27ff2ff8a6b9b9f847572f3" + "52ffadf3d868a5248000271b950fbbc7" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unsound.fst.hints b/test/.hints/Unsound.fst.hints index dbafc13c..4ec22825 100644 --- a/test/.hints/Unsound.fst.hints +++ b/test/.hints/Unsound.fst.hints @@ -13,7 +13,7 @@ "refinement_interpretation_Tm_refine_652f0f3ffdde8cb9fe553db21d874aee" ], 0, - "29f8cf8bc461049714dad9899a175074" + "b731f80e9fc4259efc8630a52f22da44" ], [ "Unsound.g", @@ -22,7 +22,7 @@ 1, [ "@query" ], 0, - "7ae5b2db618241fbb8c49689335f9b4f" + "013da39d49062c679811a37879c2e01f" ], [ "Unsound.main", @@ -95,7 +95,7 @@ "typing_FStar.UInt32.t", "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "5e651005eff4ec9e6ebf80f9a3da6b81" + "a57d3ecd3b06fd11b3f3df3b6166f975" ] ] ] \ No newline at end of file diff --git a/test/.hints/UnusedParameter.fst.hints b/test/.hints/UnusedParameter.fst.hints index 71c7a10f..897dbe1f 100644 --- a/test/.hints/UnusedParameter.fst.hints +++ b/test/.hints/UnusedParameter.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.Int64.t" ], 0, - "7ff153e74bceb2e6ad3d78f348a2b03f" + "42a8f389914a34f8f7fe29ea01d52580" ], [ "UnusedParameter.touch", @@ -33,7 +33,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "3257a230a3a506d96b3beef23924dde3" + "6bf45e7fa020eca440e0a33f3e1a60b4" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unused_A.fst.hints b/test/.hints/Unused_A.fst.hints index 32d726b2..6b332429 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, - "fc342064b0f95612c70649065d9b7f22" + "9bc391abdaf7ae92d9b99044976875ed" ] ] ] \ No newline at end of file diff --git a/test/.hints/Unused_B.fst.hints b/test/.hints/Unused_B.fst.hints index 5201608a..46d6ec03 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, - "cbc3f34142d1bc3f70a7fbae2f964f59" + "4dd9ffa5e5194210f05ba7d911dc3868" ] ] ] \ No newline at end of file diff --git a/test/.hints/Uu.fst.hints b/test/.hints/Uu.fst.hints index 2c7d386a..c3d360f0 100644 --- a/test/.hints/Uu.fst.hints +++ b/test/.hints/Uu.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "3362131383e095e9335ece4793610c3e" + "1462a49df13e5167c68da270e8944b16" ] ] ] \ No newline at end of file diff --git a/test/.hints/VariableMerge.fst.hints b/test/.hints/VariableMerge.fst.hints index 9e03c8c4..53f591d6 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, - "f0e31fdbb2f63267ff2bab58ec671214" + "efb05702df26eb7f50153c4099facd71" ], [ "VariableMerge.test", @@ -34,7 +34,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "83ff0ffc155ca5ba7a502cb68333c968" + "6a2f919f3a2d383541fee58afa512e73" ], [ "VariableMerge.test1", @@ -56,7 +56,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "4f873083ff99cf8990d1477361618cda" + "bd22d39c0ab0aff2bd54fd5aca5fb961" ], [ "VariableMerge.test2", @@ -78,7 +78,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "25fa367c9e35112bd8085993a4ca6972" + "dc1cc10629c1ecbf45d09378da717e8f" ], [ "VariableMerge.main", @@ -101,7 +101,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "85641151d015cf59779e635331a52bbe" + "f26e24240d1ed7323a895f5e11cb4257" ] ] ] \ No newline at end of file diff --git a/test/.hints/Verbatim.fst.hints b/test/.hints/Verbatim.fst.hints index 038e01d3..8a9df70f 100644 --- a/test/.hints/Verbatim.fst.hints +++ b/test/.hints/Verbatim.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "23f9028ac67a14ed5332c1d0a8b24b49" + "745c9e018120b65f1bed36cbfef13714" ] ] ] \ No newline at end of file diff --git a/test/.hints/Vla.fst.hints b/test/.hints/Vla.fst.hints index 25bbf54d..e4df9f6b 100644 --- a/test/.hints/Vla.fst.hints +++ b/test/.hints/Vla.fst.hints @@ -47,7 +47,7 @@ "typing_FStar.UInt32.t", "typing_FStar.UInt32.v" ], 0, - "631e7336df2310ef0c68531b25e19a0f" + "4ba38e048e66b5f9b1cd8394ca69cbb4" ], [ "Vla.main", @@ -64,7 +64,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "67b2b3cc9873ca1d57daf363f179f79e" + "f45e334a40e731d986be31f7a01a0885" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm1.fst.hints b/test/.hints/Wasm1.fst.hints index 5e1087e5..72bb0945 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, - "f394120d91501864d2ec8ea3000873f6" + "f84b6ef7974fde500fc711bf244a7406" ], [ "Wasm1.maybe_true", @@ -59,7 +59,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "69035b05f580690f898bfc64c62e53b8" + "530a21cc562e2167b15838bfbaafc237" ], [ "Wasm1.fact'", @@ -68,7 +68,7 @@ 1, [ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ], 0, - "f9237d8299ce5fc1bb94e9925251872f" + "8b3484b125c0f9efc3f54fc69763d24e" ], [ "Wasm1.minus", @@ -91,7 +91,7 @@ "typing_FStar.UInt32.v" ], 0, - "adef2f7ca37400630e5c622122af302a" + "ba1534b8cfe62363262e6e8e92d977da" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm10.fst.hints b/test/.hints/Wasm10.fst.hints index f866fde0..9543c3c9 100644 --- a/test/.hints/Wasm10.fst.hints +++ b/test/.hints/Wasm10.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "119730bdc524619129861b1d1cecba72" + "b04e17b71f6724ec9f63c3e08c279c83" ], [ "Wasm10.b", @@ -40,7 +40,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "d963f633e968faf7252207c63e674772" + "97c765f878819eea94a8e83b44978aef" ], [ "Wasm10.main", @@ -57,7 +57,7 @@ "typing_Wasm10.b" ], 0, - "89b695f7599d695d52893be5ff775039" + "1a29a912903533a4746e24ffebd8382d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm2.fst.hints b/test/.hints/Wasm2.fst.hints index 83358f2f..f6df3b4e 100644 --- a/test/.hints/Wasm2.fst.hints +++ b/test/.hints/Wasm2.fst.hints @@ -78,7 +78,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_Prims.pow2" ], 0, - "89e334afe486cfb597c87ffc8e0f73ed" + "6540ce0b0c0decbb8362eaee6ff3e779" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm3.fst.hints b/test/.hints/Wasm3.fst.hints index be84cd59..1fcac974 100644 --- a/test/.hints/Wasm3.fst.hints +++ b/test/.hints/Wasm3.fst.hints @@ -63,7 +63,7 @@ "typing_tok_C.EXIT_SUCCESS@tok" ], 0, - "256dfe4a0266ddf38d220dea9454665a" + "a743d33857694a76653300e2534ac6c5" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm4.fst.hints b/test/.hints/Wasm4.fst.hints index 1d9ab024..b2032788 100644 --- a/test/.hints/Wasm4.fst.hints +++ b/test/.hints/Wasm4.fst.hints @@ -12,7 +12,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "404d1a8fb5d9087b8d7b8f51091aea66" + "96ba573c589b1f4a64cf2bc40b5db2b8" ], [ "Wasm4.test", @@ -21,7 +21,7 @@ 1, [ "@query", "assumption_Wasm4.t__uu___haseq" ], 0, - "8dee348a3e59be3b93d4fd63475d0ede" + "69408e5dd7fae27bc136d63414e78b6d" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm5.fst.hints b/test/.hints/Wasm5.fst.hints index 612707a2..00bae18f 100644 --- a/test/.hints/Wasm5.fst.hints +++ b/test/.hints/Wasm5.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "a07c9e549f47d919a440a3375387c7ec" + "d0c518230e2672b5f94ef8dc6bbde67a" ], [ "Wasm5.y", @@ -55,7 +55,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "166d4504b975dd1e0cd5b8eae2df3028" + "9a4afe1dc2b6dbc168c2a0102f19af24" ], [ "Wasm5.main", @@ -72,7 +72,7 @@ "typing_Wasm5.x" ], 0, - "4db211abb16556fa226e029d5d387fd6" + "4cd9e1e33295321fbe87c9601e6aa3d8" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm6.fst.hints b/test/.hints/Wasm6.fst.hints index acbe9094..6b595882 100644 --- a/test/.hints/Wasm6.fst.hints +++ b/test/.hints/Wasm6.fst.hints @@ -14,7 +14,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "204b45a54661b959e6d748dcdf04e322" + "7ecf408c6a2059dcf92a9ca7f01f0819" ], [ "Wasm6.snd", @@ -29,7 +29,7 @@ "typing_LowStar.Monotonic.Buffer.loc_none" ], 0, - "f990a31ee1535c865b5af9b00b3ad950" + "44e34f4b08175ac12b8beb10b6f70933" ], [ "Wasm6.main", @@ -97,7 +97,7 @@ "typing_LowStar.Monotonic.Buffer.g_is_null" ], 0, - "e343f42b58879c7d009204c62ecfb141" + "0b8ca863d236c2f8c4a65537103f53be" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm7.fst.hints b/test/.hints/Wasm7.fst.hints index d3fa1283..839ce760 100644 --- a/test/.hints/Wasm7.fst.hints +++ b/test/.hints/Wasm7.fst.hints @@ -12,7 +12,7 @@ "typing_FStar.UInt32.t" ], 0, - "f9702b420896d5f3227501f37c52c82c" + "55f97e3834f187c02c3935f0fcc4b3cd" ], [ "Wasm7.__proj__A__item___0", @@ -24,7 +24,7 @@ "refinement_interpretation_Tm_refine_ec10ccf333cf39e2d779a27ff25f9f69" ], 0, - "5ca7450480b8da65fc738c2eb4cc04e4" + "e20c0af01d3c2329c8ca9d0ebcb53b04" ], [ "Wasm7.__proj__A__item___1", @@ -36,7 +36,7 @@ "refinement_interpretation_Tm_refine_ec10ccf333cf39e2d779a27ff25f9f69" ], 0, - "496d8cbcd5892c4b8e93bf9047a38e52" + "d580b38f610274c4c13e7e61745a77cf" ], [ "Wasm7.__proj__B__item___0", @@ -48,7 +48,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "ea4702e0e94a9264aa7e8f203d8de4e3" + "7720ad1fdace9182329fe0b51b843a3b" ], [ "Wasm7.__proj__B__item___1", @@ -60,7 +60,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "a4b10548e315603249098b68a1a73e4c" + "bdf3b4eaa0042f1aa70dd823bd53c8aa" ], [ "Wasm7.__proj__B__item___2", @@ -72,7 +72,7 @@ "refinement_interpretation_Tm_refine_1ce3b1dcced40bb1a9aec7baaac607ca" ], 0, - "0bc3ab0af45932f520f9eaeb7a2ecf57" + "59aa8794163b9f5a1d0438d46dd6ea0f" ], [ "Wasm7.v2", @@ -85,7 +85,7 @@ "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro" ], 0, - "37017ebdc102e1a3aca0779b50858815" + "22d0fc1aa80168ffeee327a706fef275" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm8.fst.hints b/test/.hints/Wasm8.fst.hints index e7526701..5fdac6b9 100644 --- a/test/.hints/Wasm8.fst.hints +++ b/test/.hints/Wasm8.fst.hints @@ -27,7 +27,7 @@ "typing_FStar.Monotonic.HyperStack.get_tip" ], 0, - "58de8be84e08dd0f8af92d2785b9a409" + "7ddcefdee96687a8b7c7e2509bb96316" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wasm9.fst.hints b/test/.hints/Wasm9.fst.hints index 88a5b255..016852c9 100644 --- a/test/.hints/Wasm9.fst.hints +++ b/test/.hints/Wasm9.fst.hints @@ -81,7 +81,7 @@ "typing_LowStar.Monotonic.Buffer.len" ], 0, - "350de326f3dccfa4b8b0a1561e55a16b" + "d209a747e56bc4f8be4aee9e0acbe65b" ] ] ] \ No newline at end of file diff --git a/test/.hints/WasmTrap.fst.hints b/test/.hints/WasmTrap.fst.hints index 4f0ec09f..7946b93a 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, - "41d76fdec7b4c0ca124184975e5844bd" + "92e0949e125f4d5006790a11fca4e0a6" ] ] ] \ No newline at end of file diff --git a/test/.hints/WildCard.fst.hints b/test/.hints/WildCard.fst.hints index 2b7acd0b..be194715 100644 --- a/test/.hints/WildCard.fst.hints +++ b/test/.hints/WildCard.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "75aee31c4c9e102238db67e00e3b28e3" + "59d4d7dff2037f58985a829bc6131099" ] ] ] \ No newline at end of file diff --git a/test/.hints/Wireguard.fst.hints b/test/.hints/Wireguard.fst.hints index 8a8fee3f..6c5fc97b 100644 --- a/test/.hints/Wireguard.fst.hints +++ b/test/.hints/Wireguard.fst.hints @@ -15,7 +15,7 @@ "subterm_ordering_Prims.Cons" ], 0, - "50facece65d2f4f7a7ea60e6773ec34a" + "d271113a332c7d9e702113811a9712f0" ], [ "Wireguard.peers_footprint", @@ -30,7 +30,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "5fe5e3abd8d1e7ac6c9e26b09b7854f1" + "ef058c9cc473cff8883483f550899e75" ], [ "Wireguard.peers_disjoint", @@ -45,7 +45,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "0557594fe2824ad67ad453d13d3b4b69" + "a8dbb7b215ab124e33079e748f7a0042" ], [ "Wireguard.peers_invariants", @@ -60,7 +60,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "5bf20ab3353904c6bf5ea0d82442fb09" + "b611daf61881ca053c89ee125e29d401" ], [ "Wireguard.peer_by_id", @@ -75,7 +75,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "55137dca5847b45a9a091d44ab748a6f" + "110e239b0a2e5fc86575a880976ee2c7" ], [ "Wireguard.peer_of_id_in_peers", @@ -96,7 +96,7 @@ "typing_FStar.Map.sel", "typing_FStar.UInt64.t" ], 0, - "7b3e53facdb10778bed0217e140cc540" + "795a244006e550b3a3c6c87ff51530bc" ], [ "Wireguard.peers_back", @@ -111,7 +111,7 @@ "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, - "4936732768ce7767d07e9488bdc9e4ec" + "e81b61d8f8e857148ccb2dd82094379e" ], [ "Wireguard.invariant", @@ -129,7 +129,7 @@ "typing_Wireguard.__proj__Mkdevice__item__r" ], 0, - "86bac221cb742f3142e385f5e2854db3" + "28d16403549bae4731d59a5c68044656" ], [ "Wireguard.peer_footprint_in", @@ -194,7 +194,7 @@ "typing_Wireguard.peer_footprint", "typing_Wireguard.peers_footprint" ], 0, - "0130b5aad8a0b83bce19776a45a45171" + "181e3be74ad3e69fde34bb3a78a68be0" ], [ "Wireguard.device_peers_footprint_in", @@ -203,7 +203,7 @@ 0, [ "@query", "equation_Wireguard.invariant" ], 0, - "891c89021fa81777ddcd3a51b8bbe208" + "1c95239e2dc22cb4d7fcf7c4704f3e24" ], [ "Wireguard.frame_peers_back", @@ -278,7 +278,7 @@ "typing_Wireguard.__proj__Mkpeer__item__hs" ], 0, - "44395d524930987bb55fa18db6e8890e" + "3ba30e37a8e65187fc04d8bf1f28e19f" ], [ "Wireguard.frame_peers_invariants", @@ -361,7 +361,7 @@ "typing_Wireguard.peer_footprint" ], 0, - "3c235ab057fd01d03c5b42dd349705a4" + "753440b641daef59492e319e9fdff380" ], [ "Wireguard.cell_by_id_is_peer_by_id", @@ -468,7 +468,7 @@ "typing_Wireguard.cell_by_id", "typing_Wireguard.peer_by_id" ], 0, - "3e9207474063ff7b2f859a3e0637841e" + "c31ab59ca61a14cb3d537555226cfa33" ], [ "Wireguard.cell_by_id_is_peer_by_id", @@ -480,7 +480,7 @@ "refinement_interpretation_Tm_refine_e3e1e282af9636913d877dace707a50a" ], 0, - "2cab475482e245505cb4cf871a48d252" + "c375205c0aef0cee21ec8de8919c8ab4" ], [ "Wireguard.peer_by_id_invariant", @@ -513,7 +513,7 @@ "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons" ], 0, - "0941730afd97daf119f2bc6c25cdcf2c" + "71cc22806cbd2a25d18a725d909fad22" ], [ "Wireguard.frame_invariant", @@ -614,7 +614,7 @@ "typing_Wireguard.peers_footprint" ], 0, - "7e4bbbfb2aa2a6e7813a48b9e879df8d" + "85b07a16503a0641fe7fe13f32ddeff8" ], [ "Wireguard.create_in", @@ -754,7 +754,7 @@ "typing_LowStar.Monotonic.Buffer.loc_regions" ], 0, - "77837855f667285744bb5df5bb3e445d" + "966ce62e725b409ee43e23edfa1dbab9" ], [ "Wireguard.free_peer_list", @@ -859,7 +859,7 @@ "typing_Wireguard.peer_footprint" ], 0, - "bf2b93568eae5c095a9830c060dd6d9f" + "1ca4da47ddd3dd8976539ca47518a865" ], [ "Wireguard.free_", @@ -925,7 +925,7 @@ "typing_Wireguard.__proj__Mkdevice__item__r_peers_payload" ], 0, - "5a2402d7f4f62b8008334e930ef1f53a" + "cfb7c5530c5768c01e38d83d7327e45b" ], [ "Wireguard.insert_peer", @@ -934,7 +934,7 @@ 0, [ "@query" ], 0, - "ec127d1c5130d0f28b1dcc07decd0a5e" + "399d41465442863b299b69bfb97c2945" ], [ "Wireguard.insert_peer", @@ -1132,7 +1132,7 @@ "typing_Wireguard.peers_footprint" ], 0, - "3e9c53d149253fa6bd64c3992aac5258" + "9f2f01acdd61e27bc83bfc63aa6928ae" ], [ "Wireguard.find_peer_by_id_", @@ -1229,7 +1229,7 @@ "typing_Wireguard.cell_by_id" ], 0, - "d50237df5c68e2cc76bb9ab6a7ac9d60" + "9c3a753e312d01a539e66c66f97f15ef" ], [ "Wireguard.find_peer_by_id", @@ -1254,7 +1254,7 @@ "typing_Wireguard.__proj__Mkdevice__item__peers" ], 0, - "499ce4e4c99caef762683b7fe2ac247e" + "c03df6e72ce5abdf307fa97638da046c" ], [ "Wireguard.link_peer_by_id", @@ -1354,7 +1354,7 @@ "typing_Wireguard.peers_footprint" ], 0, - "6e8347ef3c830fe3914218272fa3f638" + "281fa71de503b3d210b85c7dcd4199bd" ], [ "Wireguard.main", @@ -1563,7 +1563,7 @@ "typing_Wireguard.peer_by_id", "typing_Wireguard.peers_footprint" ], 0, - "d0e7f564e3f2669c2b3621746ce8cf40" + "9d6b252280727847ce9b6d83b33f2db3" ] ] ] \ No newline at end of file