Merge pull request #3406 from mtzguido/unrefine

Introduce an attribute to unrefine type arguments
FStarLang · Aug 29, 2024 · 4734765 · 4734765
2 parents d934177 + b6a049d
commit 4734765
Show file tree

Hide file tree

Showing 81 changed files with 1,772 additions and 1,469 deletions.
diff --git a/doc/old/tutorial/code/solutions/EtM.CPA.fst b/doc/old/tutorial/code/solutions/EtM.CPA.fst
@@ -37,6 +37,7 @@ let ivsize = blockSize AES_128_CBC
 let keysize = 16
 type aes_key = lbytes keysize (* = b:bytes{B.length b = keysize} *)
 type msg = plain
+[@@do_not_unrefine]
 type cipher = b:bytes{B.length b >= ivsize}
 (* MK: minimal cipher length twice blocksize? *)
 

diff --git a/examples/crypto/HyE.AE.fsti b/examples/crypto/HyE.AE.fsti
@@ -32,6 +32,7 @@ let ivsize = aeadRealIVSize AES_128_GCM
 let keysize = aeadKeySize AES_128_GCM
 type aes_key = lbytes keysize (* = b:bytes{B.length b = keysize} *)
 type msg = Plain.t
+[@@do_not_unrefine]
 type cipher = b:bytes{B.length b >= ivsize}
 (* MK: minimal cipher length twice blocksize? *)
 

diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml b/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Canon.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Canon.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoidSimple.ml b/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoidSimple.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_CtrlRewrite.ml b/ocaml/fstar-lib/generated/FStar_Tactics_CtrlRewrite.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml