Merge pull request #3337 from mtzguido/lax_vs_admit

Tidying lax vs admit, options vs environment
FStarLang · Aug 5, 2024 · 401f413 · 401f413
2 parents e5cef6f + 24dde55
commit 401f413
Show file tree

Hide file tree

Showing 109 changed files with 1,044 additions and 909 deletions.
diff --git a/examples/Makefile b/examples/Makefile
@@ -18,7 +18,7 @@ all: prep verify special_cases
 # * miniparse: Needs Krml to build
 
 
-EXCLUDE_DIRS=old/ hello/ native_tactics/ kv_parsing/ miniparse/ 
+EXCLUDE_DIRS=old/ hello/ native_tactics/ kv_parsing/ miniparse/ sample_project/
 
 # F* contrib directory needed by crypto/ . Since this Makefile
 # supersedes crypto/Makefile, we need to determine the location of the
@@ -45,6 +45,7 @@ verify: prep $(filter-out $(CACHE_DIR)/Launch.fst.checked, $(ALL_CHECKED_FILES))
 
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
+SPECIAL_CASES += sample_project
 ifneq (,$(HAS_OCAML))
 SPECIAL_CASES += hello
 SPECIAL_CASES += native_tactics

diff --git a/examples/dm4free/FStar.DM4F.Id.fst b/examples/dm4free/FStar.DM4F.Id.fst
@@ -35,7 +35,7 @@ total reifiable reflectable new_effect {
 
 // Paranoid check that dm4f didn't mess up something
 // GM: This is actually not very useful: if we mistakenly set
-// --lax, then this check will be skipped since it's not an
+// --admit_smt_queries true, then this check will be skipped since it's not an
 // expect_lax_failure, but we also cannot use expect_lax_failure.
 [@@expect_failure]
 let _ = assert False

diff --git a/examples/kv_parsing/EnumParsing.fst b/examples/kv_parsing/EnumParsing.fst
@@ -336,15 +336,15 @@ let ser_TwoNums' (n m:U32.t) : serializer_ty =
 let unfold_only (ns:list (list string)) : Tot (list norm_step) =
   FStar.List.Tot.map delta_only ns
 
-#reset-options "--lax"
+#push-options "--admit_smt_queries true"
 
 let ser_TwoNums'' (n m:U32.t) : serializer_ty =
   synth_by_tactic (fun () ->
                       normalize [delta_only
                       ["EnumParsing.ser_TwoNums";
                       "Serializing.ser_append"]] (ser_TwoNums n m <: serializer_ty))
 
-#reset-options
+#pop-options
 
 // this works, but perhaps it should be eta expanded for extraction purposes
 val ser_numbers_data: ns:numbers -> serializer (hide (encode_numbers_data ns))
@@ -370,23 +370,25 @@ let ser_numbers_data2 ns =
   | OneNum n -> ser_OneNum n
   | TwoNums n m -> ser_TwoNums n m
 
-//but doing it via tactic normalization does not; NS/JR/JP: We added the --lax on 09/14
+//but doing it via tactic normalization does not; NS/JR/JP: We added the --admit_smt_queries true on 09/14
 // this is the same as ser_numbers_data; haven't synthesized the eta expansion
-#set-options "--lax"
+#push-options "--admit_smt_queries true"
 let ser_numbers_data'' ns : serializer_ty =
     synth_by_tactic (fun () ->
                         normalize' [delta_only
                                    ["EnumParsing.ser_numbers_data2"]] (ser_numbers_data2 ns))
 
-#reset-options
+#pop-options
+
 val ser_numbers: ns:numbers -> serializer (hide (encode_numbers ns))
 let ser_numbers ns = fun buf ->
   (ser_numbers_tag (numbers_tag_val ns) `ser_append`
    ser_numbers_data ns) buf
 
 //same problem as ser_numbers_data''
-#set-options "--lax"
+#push-options "--admit_smt_queries true"
 let ser_numbers' ns : serializer_ty =
   synth_by_tactic (fun () -> normalize' [delta_only
                              ["EnumParsing.ser_numbers";
                               "Serializing.ser_append"]] (ser_numbers ns <: serializer_ty))
+#pop-options
diff --git a/examples/miniparse/MiniParse.Impl.List.fst b/examples/miniparse/MiniParse.Impl.List.fst
@@ -76,7 +76,7 @@ let list_assoc_append (#t: Type) (x: t) (l1 l2: list t) : Lemma
 = L.append_assoc (L.rev l1) [x] l2;
   L.rev_append [x] l1
 
-#set-options "--z3rlimit 64 --max_ifuel 8"
+#set-options "--z3rlimit 96 --max_ifuel 8"
 
 let parse_nlist_impl_inv_false_intro
   (#t: Type0)

diff --git a/examples/old/tls-record-layer/crypto/Buffer.Utils.fst b/examples/old/tls-record-layer/crypto/Buffer.Utils.fst
@@ -38,7 +38,7 @@ let bytes = buffer u8
 // JP: 20180402 this file dropped off CI a long while ago. Retained here,
 // currently used as a testcase for KaRaMeL extraction, but I would love to see
 // this re-enabled as a sanity check for F*'s long CI.
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 (** Rotate operators on UInt32.t *)
 let op_Greater_Greater_Greater (a:u32) (s:u32{v s <= 32}) =

diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encoding.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encoding.fst
@@ -421,7 +421,7 @@ val accumulate:
 
 // 20170313 JP: this verifies on my OSX laptop but not on the CI machine. See
 // #893
-#reset-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0 --z3rlimit 2048 --lax"
+#reset-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0 --z3rlimit 2048 --admit_smt_queries true"
 let accumulate #i st aadlen aad txtlen cipher  = 
   let h = ST.get() in 
   let acc = CMA.start st in

diff --git a/examples/old/tls-record-layer/crypto/Crypto.KrmlTest.fst b/examples/old/tls-record-layer/crypto/Crypto.KrmlTest.fst
@@ -56,7 +56,7 @@ module E = Crypto.AEAD.Encrypt
 
 module L = FStar.List.Tot
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 
 let mk_buf_t (len:nat) =
@@ -85,7 +85,7 @@ let mk_ivBuffer : mk_buf_t 12
   = fun () ->
     Buffer.createL [0x07uy; 0x00uy; 0x00uy; 0x00uy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy ]
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 let mk_expected_cipher : mk_buf_t 130
   = fun () ->
     Buffer.createL [0xd3uy; 0x1auy; 0x8duy; 0x34uy; 0x64uy; 0x8euy; 0x60uy; 0xdbuy; 0x7buy; 0x86uy; 0xafuy; 0xbcuy; 0x53uy; 0xefuy; 0x7euy; 0xc2uy;

diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES.fst
@@ -76,7 +76,7 @@ let multiply a b =
   ^^ (xtime (xtime (xtime (xtime (xtime (xtime a))))) *%^ ((b >>^ 6ul) &^ 1uy))
   ^^ (xtime (xtime (xtime (xtime (xtime (xtime (xtime a)))))) *%^ ((b >>^ 7ul) &^ 1uy)))
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 // tables for S-box and inv-S-box, derived from GF256 specification.
 
 type sbox  = lbytes 256

diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES128.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES128.fst
@@ -72,7 +72,7 @@ let multiply a b =
   ^^ (xtime (xtime (xtime (xtime (xtime (xtime a))))) *%^ ((b >>^ 6ul) &^ 1uy))
   ^^ (xtime (xtime (xtime (xtime (xtime (xtime (xtime a)))))) *%^ ((b >>^ 7ul) &^ 1uy)))
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 // tables for S-box and inv-S-box, derived from GF256 specification.
 
 type sbox  = lbytes 256

diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Chacha20.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Chacha20.fst
@@ -37,7 +37,7 @@ module ST = FStar.HyperStack.ST
 type u64 = FStar.UInt64.t
 
 // JP: see comment in Buffer.Utils.fst
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 (*** Chacha 20 ***)
 

diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.MAC.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.MAC.fst
@@ -398,7 +398,7 @@ let mac #i st l acc tag =
     end
 //16-09-24 why?
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 val verify: #i:id -> st:state i -> l:itext -> computed:accB i -> tag:tagB ->
   Stack bool

diff --git a/examples/old/tls-record-layer/crypto/Crypto.Test.fst b/examples/old/tls-record-layer/crypto/Crypto.Test.fst
@@ -88,7 +88,7 @@ let mk_ivBuffer : mk_buf_t 12
       0x07uy; 0x00uy; 0x00uy; 0x00uy; 0x40uy; 0x41uy; 0x42uy; 0x43uy; 
       0x44uy; 0x45uy; 0x46uy; 0x47uy ]
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 let mk_expected_cipher : mk_buf_t 130
   = fun () -> 
     createL 130 [

diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fdifference.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fdifference.fst
@@ -25,7 +25,7 @@ open Math.Lib
 open Curve.Parameters
 open Curve.Bigint
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 module U8  = FStar.UInt8
 module U32 = FStar.UInt32

diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fproduct.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fproduct.fst
@@ -25,7 +25,7 @@ open Math.Lib
 open Curve.Parameters
 open Curve.Bigint
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 module U8  = FStar.UInt8
 module U32 = FStar.UInt32

diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fscalar.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fscalar.fst
@@ -25,7 +25,7 @@ open Math.Lib
 open Curve.Parameters
 open Curve.Bigint
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 module U8  = FStar.UInt8
 module U32 = FStar.UInt32

diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fsum.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fsum.fst
@@ -25,7 +25,7 @@ open Math.Lib
 open Curve.Parameters
 open Curve.Bigint
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 module U8  = FStar.UInt8
 module U32 = FStar.UInt32

diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.FsumWide.fst b/examples/old/tls-record-layer/crypto/stale/Curve.FsumWide.fst
@@ -25,7 +25,7 @@ open Math.Lib
 open Curve.Parameters
 open Curve.Bigint
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 module U8  = FStar.UInt8
 module U32 = FStar.UInt32

diff --git a/examples/old/tls-record-layer/old/ulib/FStar.Buffer.fst b/examples/old/tls-record-layer/old/ulib/FStar.Buffer.fst
@@ -250,7 +250,7 @@ let lemma_modifies_one_trans_1 (#a:Type) (b:buffer a) (h0:t) (h1:t) (h2:t): Lemm
   = ()
 
 #reset-options "--z3timeout 100"
-#set-options "--lax" // TODO: remove 
+#set-options "--admit_smt_queries true" // TODO: remove
 
 (* TODO: simplify, add triggers ? *)
 private val blit_aux: #a:Type -> b:buffer a -> idx_b:uint32{v idx_b<=length b} -> 

diff --git a/examples/old/tls-record-layer/old/ulib/aes.fst b/examples/old/tls-record-layer/old/ulib/aes.fst
@@ -22,7 +22,7 @@ open SInt
 open SInt.UInt8
 open FStar.Buffer
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 (* JK: bug, it is necessary to add this type abbreviation to make things typecheck *)
 type suint8 = uint8   // 

diff --git a/examples/old/tls-record-layer/old/ulib/hyperstack/FStar.Buffer.fst b/examples/old/tls-record-layer/old/ulib/hyperstack/FStar.Buffer.fst
@@ -280,7 +280,7 @@ let lemma_modifies_one_trans_1 (#a:Type) (b:buffer a) (h0:mem) (h1:mem) (h2:mem)
 
 #reset-options "--z3timeout 100"
 // TODO: remove 
-(* #set-options "--lax" *)
+(* #set-options "--admit_smt_queries true" *)
 
 (* TODO: simplify, add triggers ? *)
 private val blit_aux: #a:Type -> b:buffer a -> idx_b:u32 -> 

diff --git a/examples/old/tls-record-layer/old/ulib/hyperstack/chacha.fst b/examples/old/tls-record-layer/old/ulib/hyperstack/chacha.fst
@@ -151,7 +151,7 @@ let rec bytes_of_uint32s output m len =
       bytes_of_uint32s output m l
     end
 
-#set-options "--lax" // TODO
+#set-options "--admit_smt_queries true" // TODO
 
 val xor_bytes: output:bytes -> in1:bytes -> in2:bytes{disjoint in1 in2 /\ disjoint in1 output /\ disjoint in2 output} -> len:u32{v len <= length output /\ v len <= length in1 /\ v len <= length in2} -> STL unit
   (requires (fun h -> live h output /\ live h in1 /\ live h in2))

diff --git a/examples/old/tls-record-layer/parsing/FStar.ImmBuffer.fst b/examples/old/tls-record-layer/parsing/FStar.ImmBuffer.fst
@@ -246,7 +246,7 @@ let cast (#t:sizeof_t) (ty:serializable t) (#t':sizeof_t) (#ty':serializable t')
 (**           Concrete parser and serializers for basetypes          **)
 (** **************************************************************** **)
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 assume val le_uint8_serializer: serializer byte
 (* let le_uint8_serializer = *)

diff --git a/examples/old/tls-record-layer/parsing/MessagesParsing.fst b/examples/old/tls-record-layer/parsing/MessagesParsing.fst
@@ -23,7 +23,7 @@ open FStar.Int.Cast
 open FStar.Buffer
 open Messages2
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 
 (* Returns the length as a UInt32 *)

diff --git a/examples/old/tls-record-layer/parsing/Parsing3.fst b/examples/old/tls-record-layer/parsing/Parsing3.fst
@@ -24,7 +24,7 @@ open FStar.Int.Cast
 open FStar.Buffer
 open Low.Bytes
 
-#set-options "--lax"
+#set-options "--admit_smt_queries true"
 
 val read_length: b:bytes -> n:UInt32.t{v n = 1 \/ v n = 2 \/ v n = 3} -> STL UInt32.t
   (requires (fun h -> Buffer.live h b /\ v n <= Buffer.length b))

diff --git a/examples/preorders/Indexed_effect.fst.wish b/examples/preorders/Indexed_effect.fst.wish
@@ -28,8 +28,8 @@ let ist_wp   (state:Type) (a:Type) = ist_post state a -> Tot (ist_pre state)
 
 (* A WP-style preorder-indexed state monad. *)
 
-new_effect  ISTATE (state:Type0) (rel:relation state{preorder rel}) = STATE_h state //typechecks with --lax flag on
-//new_effect  ISTATE (state:Type) (rel:relation state{preorder rel}) = STATE_h state //does not typecheck with --lax flag on
+new_effect  ISTATE (state:Type0) (rel:relation state{preorder rel}) = STATE_h state //typechecks with --admit_smt_queries true flag on
+//new_effect  ISTATE (state:Type) (rel:relation state{preorder rel}) = STATE_h state //does not typecheck with --admit_smt_queries true flag on
 
 
 (* Currently not possible, but at this point one would like to show that 

diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Interactive_Ide.ml b/ocaml/fstar-lib/generated/FStar_Interactive_Ide.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Interactive_Legacy.ml b/ocaml/fstar-lib/generated/FStar_Interactive_Legacy.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Interactive_PushHelper.ml b/ocaml/fstar-lib/generated/FStar_Interactive_PushHelper.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml