[CI] regenerate hints

hacl-star · Apr 17, 2017 · c771955 · c771955
1 parent a8b403d
commit c771955
Show file tree

Hide file tree

Showing 24 changed files with 643 additions and 950 deletions.
diff --git a/code/api/Chacha20Poly1305.fst.hints b/code/api/Chacha20Poly1305.fst.hints
@@ -973,29 +973,29 @@
         "@MaxIFuel_assumption", "@query",
         "assumption_FStar.HyperHeap.HasEq_rid", "b2t_def", "bool_inversion",
         "bool_typing", "data_elim_FStar.Buffer.MkBuffer",
-        "data_elim_FStar.HyperStack.MkRef",
+        "data_elim_FStar.HyperStack.HS", "data_elim_FStar.HyperStack.MkRef",
         "data_elim_Spec.CTR.Mkblock_cipher_ctx",
         "equation_Chacha20Poly1305.keylen",
         "equation_Chacha20Poly1305.maclen",
-        "equation_Chacha20Poly1305.noncelen", "equation_FStar.Buffer.as_seq",
-        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
-        "equation_FStar.Buffer.content", "equation_FStar.Buffer.disjoint",
-        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf",
-        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes",
-        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
-        "equation_FStar.Buffer.sel", "equation_FStar.Buffer.sub",
-        "equation_FStar.Endianness.u32", "equation_FStar.HyperHeap.sel",
+        "equation_Chacha20Poly1305.noncelen", "equation_FStar.Buffer.buffer",
+        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
+        "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal",
+        "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx",
+        "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length",
+        "equation_FStar.Buffer.live", "equation_FStar.Buffer.sub",
+        "equation_FStar.Endianness.u32",
+        "equation_FStar.HyperHeap.map_invariant",
         "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
         "equation_FStar.HyperStack.equal_domains",
         "equation_FStar.HyperStack.frameOf",
         "equation_FStar.HyperStack.fresh_frame",
-        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
+        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
+        "equation_FStar.HyperStack.is_tip",
         "equation_FStar.HyperStack.live_region",
         "equation_FStar.HyperStack.pop",
         "equation_FStar.HyperStack.poppable",
         "equation_FStar.HyperStack.popped",
-        "equation_FStar.HyperStack.remove_elt",
-        "equation_FStar.HyperStack.sel", "equation_FStar.Mul.op_Star",
+        "equation_FStar.HyperStack.remove_elt", "equation_FStar.Mul.op_Star",
         "equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
         "equation_FStar.UInt.add", "equation_FStar.UInt.fits",
         "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
@@ -1018,8 +1018,10 @@
         "function_token_typing_FStar.Heap.emp",
         "function_token_typing_FStar.Heap.heap",
         "function_token_typing_FStar.HyperHeap.rid",
+        "function_token_typing_FStar.Set.singleton",
         "function_token_typing_FStar.UInt8.n",
         "function_token_typing_Spec.Chacha20.chacha20_ctx",
+        "interpretation_Tm_arrow_f285bd18d16ed788dea4e9c47fb2243d",
         "kinding_FStar.UInt8.t_@tok",
         "lemma_FStar.Buffer.lemma_disjoint_sub",
         "lemma_FStar.Buffer.lemma_disjoint_sub_",
@@ -1036,6 +1038,7 @@
         "lemma_FStar.Buffer.live_popped",
         "lemma_FStar.Buffer.modifies_popped_3_2",
         "lemma_FStar.Buffer.modifies_subbuffer_1",
+        "lemma_FStar.Buffer.modifies_subbuffer_2_",
         "lemma_FStar.Buffer.no_upd_fresh",
         "lemma_FStar.Buffer.no_upd_lemma_0",
         "lemma_FStar.Buffer.no_upd_lemma_1",
@@ -1044,7 +1047,6 @@
         "lemma_FStar.HyperStack.lemma_equal_domains_trans",
         "lemma_FStar.Map.lemma_ContainsDom",
         "lemma_FStar.Map.lemma_InDomUpd1",
-        "lemma_FStar.Map.lemma_SelRestrict",
         "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
         "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
         "lemma_FStar.UInt.pow2_values",
@@ -1059,6 +1061,7 @@
         "proj_equation_FStar.Buffer.MkBuffer_length",
         "proj_equation_FStar.Buffer.MkBuffer_max_length",
         "proj_equation_FStar.HyperStack.HS_h",
+        "proj_equation_FStar.HyperStack.HS_tip",
         "proj_equation_FStar.HyperStack.MkRef_id",
         "proj_equation_FStar.HyperStack.MkRef_ref",
         "proj_equation_FStar.UInt32.Mk_v",
@@ -1092,24 +1095,27 @@
         "refinement_interpretation_Tm_refine_953ae969eef645b5efb51ecb99722297",
         "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
         "refinement_interpretation_Tm_refine_aef6ec9d3290a1c96570fbfd09471f2e",
+        "refinement_interpretation_Tm_refine_b560551048d2e17324f021503ddc4232",
         "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
         "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
+        "refinement_interpretation_Tm_refine_d023b9461e4d4c2c1260f907a1d7e4a1",
         "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
         "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
         "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
+        "token_correspondence_FStar.Set.singleton",
         "typing_FStar.Buffer.__proj__MkBuffer__item__content",
         "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
         "typing_FStar.Buffer.__proj__MkBuffer__item__length",
         "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.content",
-        "typing_FStar.Buffer.length",
+        "typing_FStar.Buffer.length", "typing_FStar.HyperHeap.includes",
         "typing_FStar.HyperStack.__proj__HS__item__h",
         "typing_FStar.HyperStack.__proj__HS__item__tip",
         "typing_FStar.HyperStack.__proj__MkRef__item__id",
         "typing_FStar.HyperStack.poppable",
         "typing_FStar.HyperStack.remove_elt", "typing_FStar.Map.contains",
         "typing_FStar.Map.domain", "typing_FStar.Map.restrict",
-        "typing_FStar.Set.complement", "typing_FStar.Set.singleton",
-        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
+        "typing_FStar.Set.complement", "typing_FStar.UInt.fits",
+        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
         "typing_Prims.pow2"
       ],
       0
@@ -1523,7 +1529,6 @@
         "assumption_FStar.HyperHeap.HasEq_rid", "b2t_def", "bool_inversion",
         "bool_typing", "constructor_distinct_Prims.Some",
         "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.HyperStack.HS",
-        "data_elim_FStar.HyperStack.MkRef",
         "data_elim_Spec.CTR.Mkblock_cipher_ctx", "disc_equation_Prims.Some",
         "equation_Chacha20Poly1305.keylen",
         "equation_Chacha20Poly1305.maclen",
@@ -1572,12 +1577,9 @@
         "function_token_typing_FStar.Heap.emp",
         "function_token_typing_FStar.Heap.heap",
         "function_token_typing_FStar.HyperHeap.rid",
-        "function_token_typing_FStar.Set.singleton",
         "function_token_typing_FStar.UInt8.n",
         "function_token_typing_Spec.Chacha20.chacha20_ctx", "int_typing",
-        "interpretation_Tm_arrow_f285bd18d16ed788dea4e9c47fb2243d",
         "kinding_FStar.UInt8.t_@tok",
-        "lemma_FStar.Buffer.lemma_disjoint_sub",
         "lemma_FStar.Buffer.lemma_disjoint_symm",
         "lemma_FStar.Buffer.lemma_equal_domains_2",
         "lemma_FStar.Buffer.lemma_fresh_poppable",
@@ -1601,7 +1603,6 @@
         "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
         "lemma_FStar.UInt.pow2_values",
         "pretyping_6c86c071b92797cdf01eb016249a9465",
-        "pretyping_730e633374418435590e5214be2471d4",
         "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
         "primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
         "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
@@ -1613,8 +1614,6 @@
         "proj_equation_FStar.Buffer.MkBuffer_max_length",
         "proj_equation_FStar.HyperStack.HS_h",
         "proj_equation_FStar.HyperStack.HS_tip",
-        "proj_equation_FStar.HyperStack.MkRef_id",
-        "proj_equation_FStar.HyperStack.MkRef_ref",
         "proj_equation_FStar.UInt32.Mk_v", "proj_equation_Prims.Some_v",
         "projection_inverse_BoxBool_proj_0",
         "projection_inverse_BoxInt_proj_0",
@@ -1641,19 +1640,21 @@
         "refinement_interpretation_Tm_refine_d023b9461e4d4c2c1260f907a1d7e4a1",
         "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
         "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
-        "token_correspondence_FStar.Set.singleton",
+        "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
         "typing_FStar.Buffer.__proj__MkBuffer__item__content",
         "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
         "typing_FStar.Buffer.__proj__MkBuffer__item__length",
         "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.content",
         "typing_FStar.Buffer.length", "typing_FStar.HyperHeap.includes",
         "typing_FStar.HyperStack.__proj__HS__item__h",
         "typing_FStar.HyperStack.__proj__HS__item__tip",
+        "typing_FStar.HyperStack.__proj__MkRef__item__id",
         "typing_FStar.HyperStack.poppable",
         "typing_FStar.HyperStack.remove_elt", "typing_FStar.Map.contains",
         "typing_FStar.Map.domain", "typing_FStar.Map.restrict",
-        "typing_FStar.Set.complement", "typing_FStar.UInt.fits",
-        "typing_FStar.UInt32.v", "typing_Prims.pow2"
+        "typing_FStar.Set.complement", "typing_FStar.Set.singleton",
+        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
+        "typing_Prims.pow2"
       ],
       0
     ]

diff --git a/code/api/Hacl.Box.ZeroPad.fst.hints b/code/api/Hacl.Box.ZeroPad.fst.hints
@@ -368,7 +368,6 @@
         "lemma_FStar.Buffer.lemma_equal_domains_2",
         "lemma_FStar.Buffer.lemma_fresh_poppable",
         "lemma_FStar.Buffer.lemma_modifies_0_1_",
-        "lemma_FStar.Buffer.lemma_modifies_1_trans",
         "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
         "lemma_FStar.Buffer.modifies_poppable_0",
         "lemma_FStar.Buffer.modifies_poppable_1",

diff --git a/code/api/Hacl.SecretBox.ZeroPad.fst.hints b/code/api/Hacl.SecretBox.ZeroPad.fst.hints
@@ -280,7 +280,6 @@
         "lemma_FStar.Map.lemma_ContainsDom",
         "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
         "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
-        "lemma_FStar.UInt.pow2_values",
         "pretyping_6c86c071b92797cdf01eb016249a9465",
         "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
         "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
@@ -547,12 +546,14 @@
       0,
       [
         "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
-        "bool_typing", "equation_FStar.Buffer.buffer",
-        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
-        "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.frameOf",
+        "bool_typing", "equation_FStar.Buffer.as_seq",
+        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
+        "equation_FStar.Buffer.content", "equation_FStar.Buffer.disjoint",
+        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf",
         "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes",
         "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
-        "equation_FStar.Buffer.sub", "equation_FStar.HyperStack.contains",
+        "equation_FStar.Buffer.sel", "equation_FStar.Buffer.sub",
+        "equation_FStar.HyperStack.contains",
         "equation_FStar.HyperStack.equal_domains",
         "equation_FStar.HyperStack.frameOf",
         "equation_FStar.HyperStack.fresh_frame",
@@ -582,6 +583,7 @@
         "fuel_guarded_inversion_FStar.HyperStack.reference",
         "fuel_guarded_inversion_FStar.UInt32.t_",
         "fuel_guarded_inversion_FStar.UInt64.t_",
+        "function_token_typing_FStar.UInt64.n",
         "function_token_typing_FStar.UInt8.n", "int_inversion", "int_typing",
         "kinding_FStar.UInt8.t_@tok",
         "lemma_FStar.Buffer.lemma_disjoint_sub",
@@ -594,15 +596,18 @@
         "lemma_FStar.Buffer.lemma_modifies_0_2",
         "lemma_FStar.Buffer.lemma_modifies_1_trans",
         "lemma_FStar.Buffer.lemma_modifies_2_comm",
-        "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
+        "lemma_FStar.Buffer.lemma_sub_spec", "lemma_FStar.Buffer.live_fresh",
+        "lemma_FStar.Buffer.live_popped",
         "lemma_FStar.Buffer.modifies_poppable_1",
         "lemma_FStar.Buffer.modifies_poppable_2",
         "lemma_FStar.Buffer.modifies_popped_1",
         "lemma_FStar.Buffer.modifies_subbuffer_1",
         "lemma_FStar.Buffer.modifies_subbuffer_2",
+        "lemma_FStar.Buffer.no_upd_fresh",
         "lemma_FStar.Buffer.no_upd_lemma_0",
         "lemma_FStar.Buffer.no_upd_lemma_1",
         "lemma_FStar.HyperStack.lemma_equal_domains_trans",
+        "lemma_FStar.Seq.Base.lemma_len_slice",
         "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
         "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
         "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
@@ -615,28 +620,36 @@
         "projection_inverse_BoxBool_proj_0",
         "projection_inverse_BoxInt_proj_0",
         "projection_inverse_FStar.Buffer.MkBuffer_idx",
+        "projection_inverse_FStar.UInt32.Mk_v",
         "refinement_interpretation_Tm_refine_0113051b6b032ff9750105d7dd440c6b",
         "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
+        "refinement_interpretation_Tm_refine_0c39788a35c67ccb2b6c008a42650895",
         "refinement_interpretation_Tm_refine_1b5d9020cc8f44163e9c491b867a8c24",
         "refinement_interpretation_Tm_refine_4a3ba02ac5fb73cf633500f982181cea",
+        "refinement_interpretation_Tm_refine_7874c81428902f5ef0683ead2eab5830",
         "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
+        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
         "refinement_interpretation_Tm_refine_87921bbb84409a2ed981c6d200ceccc7",
         "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
         "refinement_interpretation_Tm_refine_90c17150abf5cdb4d91f504ab07d9689",
+        "refinement_interpretation_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
         "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
         "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
+        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
         "refinement_interpretation_Tm_refine_ce87d07f624eb77b8cd8e5f5bfb9f378",
         "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
         "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
         "refinement_interpretation_Tm_refine_f59487b7e8b45c2a070787f5739c33a0",
+        "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
         "typing_FStar.Buffer.__proj__MkBuffer__item__content",
         "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
         "typing_FStar.Buffer.__proj__MkBuffer__item__length",
         "typing_FStar.Buffer.__proj__MkBuffer__item__max_length",
-        "typing_FStar.Buffer.content", "typing_FStar.Buffer.length",
+        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.content",
+        "typing_FStar.Buffer.idx", "typing_FStar.Buffer.length",
         "typing_FStar.HyperStack.__proj__HS__item__tip",
-        "typing_FStar.HyperStack.poppable", "typing_FStar.UInt32.v",
-        "typing_FStar.UInt64.v", "typing_Prims.pow2"
+        "typing_FStar.HyperStack.poppable", "typing_FStar.HyperStack.sel",
+        "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Prims.pow2"
       ],
       0
     ],

diff --git a/code/curve25519/Hacl.EC.Format.fst.hints b/code/curve25519/Hacl.EC.Format.fst.hints
@@ -2277,8 +2277,8 @@
         "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
         "typing_FStar.Buffer.__proj__MkBuffer__item__length",
         "typing_FStar.Buffer.as_aref", "typing_FStar.Buffer.as_seq",
-        "typing_FStar.Buffer.content", "typing_FStar.Buffer.idx",
-        "typing_FStar.Buffer.length", "typing_FStar.Heap.domain",
+        "typing_FStar.Buffer.content", "typing_FStar.Buffer.length",
+        "typing_FStar.Heap.domain",
         "typing_FStar.HyperStack.__proj__HS__item__h",
         "typing_FStar.HyperStack.sel", "typing_FStar.Map.contains",
         "typing_FStar.Map.domain", "typing_FStar.Map.sel",

diff --git a/code/curve25519/Hacl.EC.Point.fst.hints b/code/curve25519/Hacl.EC.Point.fst.hints
@@ -504,9 +504,8 @@
         "equation_FStar.Set.eqtype", "equation_FStar.UInt.eq",
         "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
         "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
-        "equation_FStar.UInt.sub", "equation_FStar.UInt.uint_t",
-        "equation_FStar.UInt32.eq", "equation_FStar.UInt32.n",
-        "equation_FStar.UInt32.sub", "equation_FStar.UInt32.t",
+        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.eq",
+        "equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
         "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
         "equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
         "equation_FStar.UInt64.uint_to_t",
@@ -562,7 +561,6 @@
         "proj_equation_FStar.UInt32.Mk_v",
         "projection_inverse_BoxBool_proj_0",
         "projection_inverse_BoxInt_proj_0",
-        "projection_inverse_FStar.UInt32.Mk_v",
         "projection_inverse_Prims.Mktuple2__1",
         "projection_inverse_Prims.Mktuple2__2",
         "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",

diff --git a/code/curve25519/bignum_hints/Hacl.Bignum.fst.hints b/code/curve25519/bignum_hints/Hacl.Bignum.fst.hints
@@ -168,6 +168,7 @@
         "equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
         "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf",
         "equation_FStar.Buffer.idx", "equation_FStar.Buffer.live",
+        "equation_FStar.Buffer.sel", "equation_FStar.HyperHeap.sel",
         "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
         "equation_FStar.HyperStack.equal_domains",
         "equation_FStar.HyperStack.frameOf",
@@ -178,6 +179,7 @@
         "equation_FStar.HyperStack.poppable",
         "equation_FStar.HyperStack.popped",
         "equation_FStar.HyperStack.remove_elt",
+        "equation_FStar.HyperStack.sel",
         "equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
         "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
         "equation_FStar.UInt32.t", "equation_FStar.UInt64.t",
@@ -218,6 +220,7 @@
         "lemma_FStar.HyperStack.lemma_equal_domains_trans",
         "lemma_FStar.Map.lemma_ContainsDom",
         "lemma_FStar.Map.lemma_InDomUpd1",
+        "lemma_FStar.Map.lemma_SelRestrict",
         "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
         "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
         "lemma_Hacl.Spec.Bignum.Bigint.lemma_eval",
@@ -231,6 +234,7 @@
         "proj_equation_FStar.HyperStack.HS_h",
         "proj_equation_FStar.HyperStack.HS_tip",
         "proj_equation_FStar.HyperStack.MkRef_id",
+        "proj_equation_FStar.HyperStack.MkRef_ref",
         "projection_inverse_BoxBool_proj_0",
         "projection_inverse_BoxInt_proj_0",
         "projection_inverse_FStar.HyperStack.HS_h",
@@ -257,8 +261,8 @@
         "typing_FStar.HyperStack.poppable",
         "typing_FStar.HyperStack.remove_elt", "typing_FStar.Map.contains",
         "typing_FStar.Map.domain", "typing_FStar.Map.restrict",
-        "typing_FStar.Set.complement", "typing_FStar.Set.singleton",
-        "typing_FStar.UInt32.v",
+        "typing_FStar.Set.complement", "typing_FStar.Set.intersect",
+        "typing_FStar.Set.singleton", "typing_FStar.UInt32.v",
         "typing_Hacl.Spec.Bignum.Modulo.add_zero_spec"
       ],
       0

diff --git a/code/experimental/aesgcm/Crypto.Symmetric.GF128.fst.hints b/code/experimental/aesgcm/Crypto.Symmetric.GF128.fst.hints
@@ -1,5 +1,5 @@
 [
-  "��\u001b�m��J#���\\P��",
+  "�\u0016��34�.p-\"��71",
   [
     [
       "Crypto.Symmetric.GF128.elemB",