Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Simplify the compatibility story by getting rid of Spec.Compat.Loops
  • Loading branch information
protz committed Oct 5, 2018
1 parent 11344f1 commit b8f09bf
Show file tree
Hide file tree
Showing 42 changed files with 103 additions and 2,107 deletions.
6 changes: 6 additions & 0 deletions kremlib/Spec.Loops.fst
Expand Up @@ -74,15 +74,21 @@ let rec repeat_range_induction #a min max f x =
#reset-options "--max_fuel 0"

[@(deprecated "Spec.Loops.repeat")]
unfold
let repeat_spec = repeat
[@(deprecated "Spec.Loops.repeat_base")]
unfold
let lemma_repeat_0 = repeat_base
[@(deprecated "Spec.Loops.repeat_induction")]
unfold
let lemma_repeat = repeat_induction

[@(deprecated "Spec.Loops.repeat_range")]
unfold
let repeat_range_spec = repeat_range
[@(deprecated "Spec.Loops.repeat_range_base")]
unfold
let lemma_repeat_range_0 = repeat_range_base
[@(deprecated "Spec.Loops.repeat_range_induction")]
unfold
let lemma_repeat_range_spec = repeat_range_induction
4 changes: 2 additions & 2 deletions kremlib/compat/C.Compat.Loops.fst
Expand Up @@ -11,7 +11,7 @@ module HST = FStar.HyperStack.ST
module UInt32 = FStar.UInt32
module UInt64 = FStar.UInt64

include Spec.Compat.Loops
include Spec.Loops

#set-options "--initial_fuel 0 --max_fuel 0 --z3rlimit 20"

Expand Down Expand Up @@ -440,7 +440,7 @@ let repeat_range #a l min max f b fc =
fc b i;
lemma_repeat_range_spec (UInt32.v min) (UInt32.v i + 1) f (as_seq h0 b)
in
lemma_repeat_range_0 (UInt32.v min) (UInt32.v min) f (as_seq h0 b);
lemma_repeat_range_0 (UInt32.v min) f (as_seq h0 b);
for min max inv f'

let rec total_while_gen
Expand Down
162 changes: 1 addition & 161 deletions kremlib/compat/C.Endianness.fst.hints
@@ -1,161 +1 @@
[
"��z#\u0017���� �a)��d",
[
[
"C.Endianness.store16_le",
1,
2,
1,
[ "@query" ],
0,
"a150bd1b8d283167820c6d4eff5c43a4"
],
[
"C.Endianness.load16_le",
1,
2,
1,
[ "@query" ],
0,
"7bbbc420ba2ab00edf4cbf3a7124959d"
],
[
"C.Endianness.store16_be",
1,
2,
1,
[ "@query" ],
0,
"cae4b15e979a15dca0079592ba3eac25"
],
[
"C.Endianness.load16_be",
1,
2,
1,
[ "@query" ],
0,
"a384b8513b97919341cb1c5480f2a7ef"
],
[
"C.Endianness.store32_le",
1,
2,
1,
[ "@query" ],
0,
"5408834f74b7568af9a24606d7a48d81"
],
[
"C.Endianness.load32_le",
1,
2,
1,
[ "@query" ],
0,
"58f64273f7f4bb1bbf5dbb92f7e8b6f6"
],
[
"C.Endianness.store32_be",
1,
2,
1,
[ "@query" ],
0,
"b20e896016a678801ba064d9495a66ee"
],
[
"C.Endianness.load32_be",
1,
2,
1,
[ "@query" ],
0,
"0091a6a6750c51d359c5a55505a76ff4"
],
[
"C.Endianness.load64_le",
1,
2,
1,
[ "@query" ],
0,
"f63b7a8204291dca7fd98bce5f2b181f"
],
[
"C.Endianness.store64_le",
1,
2,
1,
[ "@query" ],
0,
"3f1ccc135b43775dadd43b0c5f98e7f8"
],
[
"C.Endianness.load64_be",
1,
2,
1,
[ "@query" ],
0,
"9d7f85a8e2aa00d1cd619da451a09b32"
],
[
"C.Endianness.store64_be",
1,
2,
1,
[ "@query" ],
0,
"0b22e6080efb136f3d29cf3befbd53a7"
],
[
"C.Endianness.load128_le",
1,
2,
1,
[
"@query", "equation_FStar.UInt128.n",
"projection_inverse_BoxInt_proj_0"
],
0,
"f5976fe6031763d56a5f110cee8a9f91"
],
[
"C.Endianness.store128_le",
1,
2,
1,
[
"@query", "equation_FStar.UInt128.n",
"projection_inverse_BoxInt_proj_0"
],
0,
"cddce3f1e668e5327d78a4608ca40297"
],
[
"C.Endianness.load128_be",
1,
2,
1,
[
"@query", "equation_FStar.UInt128.n",
"projection_inverse_BoxInt_proj_0"
],
0,
"1aadb24c0a8a097d7fba78c8d5ecff82"
],
[
"C.Endianness.store128_be",
1,
2,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt128.n",
"projection_inverse_BoxInt_proj_0"
],
0,
"78defbb11d5c6616293e2ed2124460fb"
]
]
]
[ "�\u0011��6�i1=���_���", [] ]
19 changes: 9 additions & 10 deletions kremlib/compat/C.Nullity.fsti.hints
Expand Up @@ -8,7 +8,7 @@
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0,
"eb7628cd576a195f43c703d7589c17c5"
"bb343756f2a75b6085ab51e181c1b075"
],
[
"C.Nullity.null_always_zero",
Expand All @@ -17,7 +17,7 @@
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0,
"0e01255ef4276349555e0991c61d7d11"
"6fa1327f1f2bef07706e34c5b1152e0c"
],
[
"C.Nullity.pointer",
Expand All @@ -26,7 +26,7 @@
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0,
"5416644033726d09b00af096e7d34c20"
"7a4999ff3a601c9b7ce39f5db5203367"
],
[
"C.Nullity.pointer_or_null",
Expand All @@ -35,7 +35,7 @@
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0,
"98da0edfc84e578793fdd66f052d1df0"
"85491f6530e8ec63be8e858b43f27d2c"
],
[
"C.Nullity.op_Bang_Star",
Expand All @@ -50,7 +50,7 @@
"refinement_interpretation_C.Nullity_Tm_refine_0d4da60cb6187749d65a25df63d2ab15"
],
0,
"f4391740eedf35b6bd067a98a145fbff"
"33571a4046549fb381885843050192e2"
],
[
"C.Nullity.pointer_distinct_sel_disjoint",
Expand Down Expand Up @@ -81,14 +81,13 @@
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.n_minus_one", "equation_Prims.eqtype",
"equation_Prims.nat", "fuel_guarded_inversion_FStar.Buffer._buffer",
"equation_FStar.UInt32.n_minus_one", "equation_Prims.pos",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Monotonic.HyperHeap.rid",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt32.n_minus_one",
"haseqFStar.Monotonic.Heap_Tm_refine_d6fbc9a334c0ab368ba5e3a78919f4aa",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"haseqPrims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"int_inversion", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Monotonic.Heap.lemma_distinct_addrs_distinct_types",
"lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
Expand Down Expand Up @@ -122,7 +121,7 @@
"typing_FStar.UInt32.v"
],
0,
"dcc6b69e1363ee2a8b0b2cf6b2a8e46a"
"8ad23e5315fddb25ca1eb84a5b908032"
]
]
]
16 changes: 8 additions & 8 deletions kremlib/compat/C.String.fst.hints
Expand Up @@ -11,7 +11,7 @@
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0"
],
0,
"7eedd41ad44f56825d65cefa86393f4f"
"65f12f6cdaf9bb8e4393e725696132fb"
],
[
"C.String.well_formed",
Expand All @@ -27,7 +27,7 @@
"typing_FStar.Seq.Base.length"
],
0,
"93b99fda79833ac2c0b7906a0af1aa0d"
"f1162b3ffaf0ab2865a75c4c3a28e2ee"
],
[
"C.String.t",
Expand All @@ -41,7 +41,7 @@
"haseqC.String_Tm_refine_72f6d6556b75c266fe5293885ad412ce"
],
0,
"8678acef46a224d8110a3c52858c8abb"
"0b96954162254ee159ac136a5c2a1a48"
],
[
"C.String.length",
Expand All @@ -55,7 +55,7 @@
"typing_C.String.__proj__S__item__s"
],
0,
"49b7f0547a3a855fd18ec3eea5d09833"
"6762c551354ee4c792c66249299fa3a9"
],
[
"C.String.get",
Expand All @@ -75,7 +75,7 @@
"typing_FStar.UInt32.v"
],
0,
"0d61f65b1655b45485c9327afec9841b"
"c2e1207b08a5dc54cb4751eed44c7bb1"
],
[
"C.String.nonzero_is_lt",
Expand All @@ -102,7 +102,7 @@
"typing_FStar.UInt32.v"
],
0,
"0f609c208fb4172ea29c7c372c49649f"
"10a385a14024325a845689a89437b559"
],
[
"C.String.strlen",
Expand All @@ -111,7 +111,7 @@
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0,
"1eb14940c10818f0bc335e31792d2e61"
"8ca9ed87aa79b54cafbfa19f74a3b2e4"
],
[
"C.String.memcpy",
Expand All @@ -129,7 +129,7 @@
"haseqC.String_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d"
],
0,
"f40225d1d24dd64ea11e45b85408d290"
"eb6885010ef6de278e51b26e8f11adb4"
]
]
]
4 changes: 2 additions & 2 deletions kremlib/compat/C.fst.hints
Expand Up @@ -8,7 +8,7 @@
1,
[ "@query", "assumption_C.HasEq_char" ],
0,
"052bcfc5de295b37f16227ea6dc01ea3"
"c1b65d2759c18e1fee301d820350544c"
],
[
"C.uint8_char",
Expand All @@ -17,7 +17,7 @@
1,
[ "@query", "assumption_FStar.UInt8.t__uu___haseq" ],
0,
"2c5677f5c76d57aa2c2a772238bab791"
"0baafc8bd0b5a4980c9eb80ba9e25b0f"
]
]
]

0 comments on commit b8f09bf

Please sign in to comment.