FStar.Seq: towards enforcing some naming conventions

- lemma_ prefix discarded
- lemmas about (f1 ... (f2 ...)) named f1_f2

See GitHub issue #687 for more information:
#687

doc/tutorial/code/solutions/Ex12b.Format.fst

@@ -18,7 +18,7 @@ val append_inj_lemma: b1:message -> b2:message
                             (ensures (b2t (Seq.eq b1 c1) /\ b2t (Seq.eq b2 c2)))
                             [SMTPat (b1 @| b2); SMTPat (c1 @| c2)] (* given to the SMT solver *)
 let append_inj_lemma b1 b2 c1 c2 =
-  lemma_append_len_disj b1 b2 c1 c2;
+  lemma_append_length_disj b1 b2 c1 c2;
   Classical.forall_intro #_ #(fun (x:(i:nat{i < length b1})) -> index b1 x == index c1 x) (lemma_append_inj_l b1 b2 c1 c2); //sadly, the 2nd implicit argument has to be provided explicitly
   Classical.forall_intro #_ #(fun (x:(i:nat{i < length b2})) -> index b2 x == index c2 x) (lemma_append_inj_r b1 b2 c1 c2)  //should fix this soon (NS)
 

examples/algorithms/QuickSort.Array.fst

@@ -68,7 +68,7 @@ let rec partition #a f start len pivot back x =
   then
     begin
 (*ghost*)      (let s = sel h0 x in
-(*ghost*)       lemma_slice_cons s pivot len;
+(*ghost*)       lemma_mem_slice_cons s pivot len;
 (*ghost*)       splice_refl s start len);
       pivot
     end
@@ -134,7 +134,7 @@ let lemma_slice_cons_pv #a s i pivot j pv =
   cut (Seq.equal (slice s i j) (append lo (cons pv hi)))
 
 #reset-options
-#set-options "--initial_fuel 1 --initial_ifuel 0 --max_fuel 1 --max_ifuel 0 --z3timeout 15"
+#set-options "--initial_fuel 1 --initial_ifuel 0 --max_fuel 1 --max_ifuel 0 --z3timeout 60"
 val sort: #a:eqtype -> f:tot_ord a -> i:nat -> j:nat{i <= j} -> x:array a
           -> ST unit
   (requires (fun h -> contains h x /\ j <= length (sel h x)))
@@ -168,7 +168,7 @@ let rec sort #a f i j x =
 (* ghost *)    let lo = slice (sel h3 x) i pivot in
 (* ghost *)    let hi = slice (sel h3 x) (pivot + 1) j in
 (* ghost *)    let pv = index (sel h1 x) pivot in
-(* ghost *)    SeqProperties.sorted_concat_lemma f lo pv hi;
+(* ghost *)    SeqProperties.lemma_sorted_append_cons f lo pv hi;
 (* ghost *)    lemma_slice_cons_pv (sel h3 x) i pivot j pv;
 
 (* ghost *)    lemma_weaken_frame_right (sel h2 x) (sel h1 x) i pivot j;

examples/algorithms/QuickSort.Array.fst.hints

@@ -156,11 +156,11 @@
         "@query", "assumption_FStar.Seq.Extensionality",
         "equation_FStar.SeqProperties.cons", "equation_Prims.nat",
         "int_inversion", "int_typing", "lemma_FStar.Seq.lemma_create_len",
-        "lemma_FStar.Seq.lemma_eq_elim", "lemma_FStar.Seq.lemma_eq_intro",
+        "lemma_FStar.Seq.eq_elim", "lemma_FStar.Seq.eq_intro",
         "lemma_FStar.Seq.lemma_index_app1",
         "lemma_FStar.Seq.lemma_index_app2",
-        "lemma_FStar.Seq.lemma_index_create",
-        "lemma_FStar.Seq.lemma_index_slice",
+        "lemma_FStar.Seq.index_create",
+        "lemma_FStar.Seq.index_slice",
         "lemma_FStar.Seq.lemma_len_append",
         "lemma_FStar.Seq.lemma_len_slice",
         "pretyping_ae567c2fb75be05905677af440075565",
@@ -280,9 +280,9 @@
         "equation_Prims.nat",
         "fuel_correspondence_FStar.SeqProperties.sorted.fuel_instrumented",
         "fuel_irrelevance_FStar.SeqProperties.sorted.fuel_instrumented",
-        "int_inversion", "lemma_FStar.Seq.lemma_eq_elim",
-        "lemma_FStar.Seq.lemma_eq_intro",
-        "lemma_FStar.Seq.lemma_index_slice",
+        "int_inversion", "lemma_FStar.Seq.eq_elim",
+        "lemma_FStar.Seq.eq_intro",
+        "lemma_FStar.Seq.index_slice",
         "lemma_FStar.Seq.lemma_len_slice",
         "pretyping_ae567c2fb75be05905677af440075565",
         "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",

examples/algorithms/QuickSort.Seq.fst

@@ -7,7 +7,7 @@ open FStar.SeqProperties
 #set-options "--max_fuel 0 --initial_fuel 0 --initial_ifuel 0 --max_ifuel 0" *)
 
 (* CH: this is needed on my machine, intermittent failures otherwise *)
-#reset-options "--z3timeout 20"
+#reset-options "--z3timeout 60"
 
 val partition: #a:eqtype -> f:(a -> a -> Tot bool){total_order a f}
     -> s:seq a -> pivot:nat{pivot < length s} -> back:nat{pivot <= back /\ back < length s} ->
@@ -64,8 +64,8 @@ let rec sort #a f s =
 
        let result = Seq.append l (cons pivot h) in
 
-       sorted_concat_lemma f l pivot h;
-       lemma_append_count l (cons pivot h);
+       lemma_sorted_append_cons f l pivot h;
+       lemma_count_append l (cons pivot h);
        cons_perm h hi;
 
        result

examples/algorithms/QuickSort.Seq.fst.hints

@@ -51,7 +51,7 @@
         "fuel_irrelevance_FStar.SeqProperties.count.fuel_instrumented",
         "int_inversion", "int_typing",
         "interpretation_Tm_arrow_4c138685807de122ddf5307392e2b2e9",
-        "lemma_FStar.Seq.lemma_index_slice",
+        "lemma_FStar.Seq.index_slice",
         "lemma_FStar.Seq.lemma_index_upd1",
         "lemma_FStar.Seq.lemma_index_upd2",
         "lemma_FStar.Seq.lemma_len_slice", "lemma_FStar.Seq.lemma_len_upd",

examples/crypto/CntFormat.fst

@@ -34,7 +34,7 @@ val append_inj_lemma: b1:message -> b2:message
                             (ensures (b2t (Seq.eq b1 c1) /\ b2t (Seq.eq b2 c2)))
                             [SMTPat (b1 @| b2); SMTPat (c1 @| c2)] (* given to the SMT solver *)
 let append_inj_lemma b1 b2 c1 c2 =
-  lemma_append_len_disj b1 b2 c1 c2;
+  lemma_append_length_disj b1 b2 c1 c2;
   Classical.forall_intro #_ #(fun (x:(i:nat{i < length b1})) -> index b1 x == index c1 x) (lemma_append_inj_l b1 b2 c1 c2); //sadly, the 2nd implicit argument has to be provided explicitly
   Classical.forall_intro #_ #(fun (x:(i:nat{i < length b2})) -> index b2 x == index c2 x) (lemma_append_inj_r b1 b2 c1 c2)  //should fix this soon (NS)
 

examples/crypto/CntFormat.fst.hints

@@ -45,7 +45,7 @@
         "equation_CntFormat.message", "equation_FStar.Char.char",
         "equation_FStar.Seq.op_At_Bar", "equation_Platform.Bytes.byte",
         "equation_Platform.Bytes.bytes", "equation_Prims.eqtype",
-        "kinding_FStar.Char.char_@tok", "lemma_FStar.Seq.lemma_eq_intro",
+        "kinding_FStar.Char.char_@tok", "lemma_FStar.Seq.eq_intro",
         "pretyping_f537159ed795b314b4e58c260361ae86",
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
         "refinement_interpretation_Tm_refine_d4aaeb44afd9014ffa1175af1903c82d",

examples/crypto/EtM.AE.fst

@@ -54,7 +54,7 @@ let genPost parent h0 (k:key) h1 =
   /\ fresh_region k.region h0 h1
   /\ Map.contains h1 k.region
   /\ m_contains k.log h1
-  /\ m_sel h1 k.log == createEmpty
+  /\ m_sel h1 k.log == empty
   /\ invariant h1 k
 
 val keygen: parent:rid -> ST key
@@ -65,7 +65,7 @@ let keygen parent =
   let region = new_region parent in
   let ke = CPA.keygen region in
   let ka = MAC.keygen region in
-  let log = alloc_mref_seq region createEmpty in
+  let log = alloc_mref_seq region empty in
   Key #region ke ka log
 
 val encrypt: k:key -> m:Plain.plain -> ST cipher

examples/crypto/EtM.AE.fst.hints

@@ -323,7 +323,7 @@
         "lemma_FStar.Seq.lemma_create_len",
         "lemma_FStar.Seq.lemma_index_app1",
         "lemma_FStar.Seq.lemma_index_app2",
-        "lemma_FStar.Seq.lemma_index_create",
+        "lemma_FStar.Seq.index_create",
         "lemma_FStar.Seq.lemma_len_append", "lemma_FStar.Set.mem_complement",
         "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
         "lemma_FStar.TSet.mem_complement", "lemma_FStar.TSet.mem_intersect",

examples/crypto/EtM.CPA.fst

@@ -39,7 +39,7 @@ let genPost parent m0 (k:key) m1 =
   /\ extends k.region parent
   /\ fresh_region k.region m0 m1
   /\ m_contains k.log m1
-  /\ m_sel m1 k.log == createEmpty
+  /\ m_sel m1 k.log == empty
 
 val keygen: parent:rid -> ST key
   (requires (fun _ -> True))
@@ -48,7 +48,7 @@ val keygen: parent:rid -> ST key
 let keygen parent =
   let raw = random keysize in
   let region = new_region parent in
-  let log = alloc_mref_seq region createEmpty in
+  let log = alloc_mref_seq region empty in
   Key #region raw log
 
 val encrypt: k:key -> m:msg -> ST cipher

examples/crypto/EtM.MAC.fst

@@ -48,11 +48,11 @@ let genPost parent h0 (k:key) h1 =
   /\ extends k.region parent
   /\ fresh_region k.region h0 h1
   /\ m_contains k.log h1
-  /\ m_sel h1 k.log == createEmpty
+  /\ m_sel h1 k.log == empty
   (* CH: equivalent definition makes gen fail:
          /\ (m_sel h1 k.log).length == 0
          can't even prove:
-           assert((createEmpty #key).length == 0); *)
+           assert((empty #key).length == 0); *)
 
 val keygen: parent:rid -> ST key
   (requires (fun _ -> True))
@@ -61,7 +61,7 @@ val keygen: parent:rid -> ST key
 let keygen parent =
   let raw = random keysize in
   let region = new_region parent in
-  let log = alloc_mref_seq region createEmpty in
+  let log = alloc_mref_seq region empty in
   Key #region raw log
 
 val mac: k:key -> m:msg -> ST tag

examples/crypto/Formatting.fst

@@ -34,7 +34,7 @@ val append_inj_lemma: b1:message -> b2:message
                             (ensures (b2t (Seq.eq b1 c1) /\ b2t (Seq.eq b2 c2)))
                             [SMTPat (b1 @| b2); SMTPat (c1 @| c2)] (* given to the SMT solver *)
 let append_inj_lemma b1 b2 c1 c2 =
-  lemma_append_len_disj b1 b2 c1 c2;
+  lemma_append_length_disj b1 b2 c1 c2;
   Classical.forall_intro #_ #(fun (x:(i:nat{i < length b1})) -> index b1 x == index c1 x) (lemma_append_inj_l b1 b2 c1 c2); //sadly, the 2nd implicit argument has to be provided explicitly
   Classical.forall_intro #_ #(fun (x:(i:nat{i < length b2})) -> index b2 x == index c2 x) (lemma_append_inj_r b1 b2 c1 c2)  //should fix this soon (NS)
 

examples/low-level/Utils.fst

@@ -36,8 +36,8 @@ let lemma_slice_sub_2 s (a:nat) (b:nat) (a':nat) (b':nat{b - a >= b' /\ a <= b /
     lemma_slice_0 s1 a' b';
     lemma_slice_0 s (a+a') (a+b');
     assert(forall (i:nat). i < b' - a' ==> Seq.index s2 i == Seq.index s (i+a+a'));
-    Seq.lemma_eq_intro s2 s3;
-    Seq.lemma_eq_elim s2 s3
+    Seq.eq_intro s2 s3;
+    Seq.eq_elim s2 s3
 
 let lemma_equal s s' (i:nat) : Lemma
   (requires (s == s' /\ i < Seq.length s))
@@ -93,16 +93,16 @@ let rec f_seq_lemma_0 #a f s1 s2 s1' s2' len =
 val lemma_slice_append: #a:Type -> s:Seq.seq a -> i:nat{i < Seq.length s} -> Lemma
   (Seq.slice s 0 (i+1) == Seq.append (Seq.slice s 0 i) (Seq.create 1 (Seq.index s i)))
 let lemma_slice_append #a s i = 
-  Seq.lemma_eq_intro (Seq.slice s 0 (i+1)) (Seq.append (Seq.slice s 0 i) (Seq.create 1 (Seq.index s i)))
+  Seq.eq_intro (Seq.slice s 0 (i+1)) (Seq.append (Seq.slice s 0 i) (Seq.create 1 (Seq.index s i)))
 
 val lemma_seq_upd: #a:Type -> s:Seq.seq a -> s':Seq.seq a -> s'':Seq.seq a -> i:nat{i < Seq.length s} -> oi:a -> Lemma
   (requires (s' == Seq.upd s i oi /\ Seq.length s'' >= Seq.length s /\ Seq.slice s'' i (Seq.length s) == Seq.slice s' i (Seq.length s)))
   (ensures  (Seq.length s'' >= Seq.length s /\ Seq.slice s'' (i+1) (Seq.length s) == Seq.slice s (i+1) (Seq.length s)))
 let lemma_seq_upd #a s s' s'' i oi =
-  Seq.lemma_eq_intro (Seq.slice s' (i+1) (Seq.length s)) (Seq.slice s (i+1) (Seq.length s));
+  Seq.eq_intro (Seq.slice s' (i+1) (Seq.length s)) (Seq.slice s (i+1) (Seq.length s));
   assert(Seq.slice s'' (i+1) (Seq.length s) == Seq.slice (Seq.slice s'' i (Seq.length s)) 1 (Seq.length s - i));
   assert(Seq.slice s' (i+1) (Seq.length s) == Seq.slice (Seq.slice s' i (Seq.length s)) 1 (Seq.length s - i));
-  Seq.lemma_eq_intro (Seq.slice s'' (i+1) (Seq.length s)) (Seq.slice s' (i+1) (Seq.length s))
+  Seq.eq_intro (Seq.slice s'' (i+1) (Seq.length s)) (Seq.slice s' (i+1) (Seq.length s))
 
 #reset-options "--z3timeout 20"
 #set-options "--max_fuel 1 --initial_fuel 1"
@@ -179,7 +179,7 @@ val xor_bytes_inplace: output:bytes -> in1:bytes{disjoint in1 output} ->
 let rec xor_bytes_inplace output in1 len =
   if UInt32.eq len 0ul then
     let h = HST.get() in
-    Seq.lemma_eq_intro (Seq.slice (to_seq8 h output) 0 0) (Seq.createEmpty #UInt8.t)
+    Seq.eq_intro (Seq.slice (to_seq8 h output) 0 0) (Seq.createEmpty #UInt8.t)
   else
     begin
       let h0 = HST.get() in
@@ -211,7 +211,7 @@ val xor_u16s_inplace: output:u16s -> in1:u16s{disjoint in1 output} ->
 let rec xor_u16s_inplace output in1 len =
   if UInt32.eq len 0ul then
     let h = HST.get() in
-    Seq.lemma_eq_intro (Seq.slice (to_seq16 h output) 0 0) (Seq.createEmpty #UInt16.t)
+    Seq.eq_intro (Seq.slice (to_seq16 h output) 0 0) (Seq.createEmpty #UInt16.t)
   else
     begin
       let h0 = HST.get() in

examples/low-level/crypto/Crypto.Symmetric.Poly1305.MAC.fst

@@ -106,7 +106,7 @@ let log_ref (r:rid) = if ideal then ideal_log r else unit
 
 let ilog (#r:rid) (l:log_ref r{ideal}) : Tot (ideal_log r) = l
 
-let text_0: itext = if ideal then Seq.createEmpty #elem else ()
+let text_0: itext = if ideal then Seq.empty #elem else ()
 
 noeq type state (i:id) =
   | State:
@@ -223,8 +223,8 @@ val seq_head_snoc: #a:Type -> xs:Seq.seq a -> x:a ->
         (ensures Seq.length (SeqProperties.snoc xs x) > 0 /\
                  seq_head (SeqProperties.snoc xs x) == xs)
 let seq_head_snoc #a xs x =
-  Seq.lemma_len_append xs (Seq.create 1 x);
-  Seq.lemma_eq_intro (seq_head (SeqProperties.snoc xs x)) xs
+  Seq.length_append xs (Seq.create 1 x);
+  Seq.eq_intro (seq_head (SeqProperties.snoc xs x)) xs
 
 #set-options "--print_fuels --initial_fuel 1 --initial_ifuel 1"
 
@@ -245,7 +245,7 @@ let update #i st l a v =
   if ideal then
     let v = sel_elemT v in
     let vs = SeqProperties.snoc l v in
-    Seq.lemma_index_app2 l (Seq.create 1 v) (Seq.length vs - 1);
+    Seq.index_append_right l (Seq.create 1 v) (Seq.length vs - 1);
     seq_head_snoc l v;
     //assert (Seq.index vs (Seq.length vs - 1) == v');
     //assert (seq_head vs == l);

examples/low-level/crypto/Crypto.Symmetric.Poly1305.Spec.fst

@@ -159,7 +159,7 @@ let lemma_little_endian_is_injective_2 b len =
   let s = Seq.slice b (Seq.length b - len) (Seq.length b) in
   let s' = Seq.slice s 1 (Seq.length s) in
   let s'' = Seq.slice b (Seq.length b - (len - 1)) (Seq.length b) in
-  Seq.lemma_eq_intro s' s''
+  Seq.eq_intro s' s''
 
 val lemma_little_endian_is_injective_3: b:word -> b':word -> len:pos{len <= Seq.length b /\ len <= Seq.length b'} -> Lemma
   (requires (Seq.slice b (Seq.length b - (len - 1)) (Seq.length b) ==
@@ -168,9 +168,9 @@ val lemma_little_endian_is_injective_3: b:word -> b':word -> len:pos{len <= Seq.
   (ensures  (Seq.slice b (Seq.length b - len) (Seq.length b) ==
              Seq.slice b' (Seq.length b' - len) (Seq.length b')))
 let lemma_little_endian_is_injective_3 b b' len =
-  Seq.lemma_eq_intro (Seq.slice b' (Seq.length b' - len) (Seq.length b'))
+  Seq.eq_intro (Seq.slice b' (Seq.length b' - len) (Seq.length b'))
 		     (Seq.append (Seq.create 1 (Seq.index b' (Seq.length b' - len))) (Seq.slice b' (Seq.length b' - (len-1)) (Seq.length b')));
-  Seq.lemma_eq_intro (Seq.slice b (Seq.length b - len) (Seq.length b))
+  Seq.eq_intro (Seq.slice b (Seq.length b - len) (Seq.length b))
 		     (Seq.append (Seq.create 1 (Seq.index b (Seq.length b - len))) (Seq.slice b (Seq.length b - (len-1)) (Seq.length b)))
 
 val lemma_little_endian_is_injective: b:word -> b':word ->
@@ -181,7 +181,7 @@ val lemma_little_endian_is_injective: b:word -> b':word ->
              Seq.slice b' (Seq.length b' - len) (Seq.length b')))
 let rec lemma_little_endian_is_injective b b' len =
   if len = 0 then
-    Seq.lemma_eq_intro (Seq.slice b (Seq.length b - len) (Seq.length b))
+    Seq.eq_intro (Seq.slice b (Seq.length b - len) (Seq.length b))
 		       (Seq.slice b' (Seq.length b' - len) (Seq.length b'))
   else
     begin
@@ -205,7 +205,7 @@ val lemma_pad_0_injective: b0:Seq.seq UInt8.t -> b1:Seq.seq UInt8.t -> l:nat ->
   (ensures  (b0 == b1))
 let lemma_pad_0_injective b0 b1 l =
   SeqProperties.lemma_append_inj b0 (Seq.create l 0uy) b1 (Seq.create l 0uy);
-  Seq.lemma_eq_intro b0 b1
+  Seq.eq_intro b0 b1
 
 val lemma_encode_16_injective: w0:word_16 -> w1:word_16 -> Lemma
   (requires (encode_16 w0 == encode_16 w1))
@@ -215,8 +215,8 @@ let lemma_encode_16_injective w0 w1 =
   lemma_little_endian_lt_2_128 w1;
   lemma_mod_plus_injective p_1305 (pow2 128) (little_endian w0) (little_endian w1);
   assert (little_endian w0 == little_endian w1);
-  Seq.lemma_eq_intro (Seq.slice w0 0 16) w0;
-  Seq.lemma_eq_intro (Seq.slice w1 0 16) w1;
+  Seq.eq_intro (Seq.slice w0 0 16) w0;
+  Seq.eq_intro (Seq.slice w1 0 16) w1;
   lemma_little_endian_is_injective w0 w1 16
 
 #reset-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 0 --max_ifuel 0"
@@ -229,16 +229,16 @@ val lemma_encode_pad_injective: p0:Seq.seq elem -> t0:Seq.seq UInt8.t -> p1:Seq.
   (decreases (Seq.length t0))
 let rec lemma_encode_pad_injective p0 t0 p1 t1 =
   let l = Seq.length t0 in
-  if l = 0 then Seq.lemma_eq_intro t0 t1
+  if l = 0 then Seq.eq_intro t0 t1
   else if l < 16 then
     begin
     let w0 = pad_0 t0 (16 - l) in
     let w1 = pad_0 t1 (16 - l) in
     SeqProperties.lemma_append_inj
       p0 (Seq.create 1 (encode_16 w0))
       p1 (Seq.create 1 (encode_16 w1));
-    lemma_index_create 1 (encode_16 w0) 0;
-    lemma_index_create 1 (encode_16 w1) 0;
+    index_create 1 (encode_16 w0) 0;
+    index_create 1 (encode_16 w1) 0;
     lemma_encode_16_injective w0 w1;
     lemma_pad_0_injective t0 t1 (16 -l)
     end
@@ -252,8 +252,8 @@ let rec lemma_encode_pad_injective p0 t0 p1 t1 =
     SeqProperties.lemma_append_inj
       p0 (Seq.create 1 (encode_16 w0))
       p1 (Seq.create 1 (encode_16 w1));
-    lemma_index_create 1 (encode_16 w0) 0;
-    lemma_index_create 1 (encode_16 w1) 0;
+    index_create 1 (encode_16 w0) 0;
+    index_create 1 (encode_16 w1) 0;
     lemma_encode_16_injective w0 w1
 
 val encode_pad_empty: prefix:Seq.seq elem -> txt:Seq.seq UInt8.t -> Lemma
@@ -265,12 +265,12 @@ val encode_pad_snoc: prefix:Seq.seq elem -> txt:Seq.seq UInt8.t -> w:word_16 ->
   (encode_pad (SeqProperties.snoc prefix (encode_16 w)) txt ==
    encode_pad prefix (append w txt))
 let encode_pad_snoc prefix txt w =
-  Seq.lemma_len_append w txt;
+  Seq.length_append w txt;
   assert (16 <= Seq.length (append w txt));
   let w', txt' = SeqProperties.split (append w txt) 16 in
   let prefix' = SeqProperties.snoc prefix (encode_16 w') in
-  Seq.lemma_eq_intro w w';
-  Seq.lemma_eq_intro txt txt'
+  Seq.eq_intro w w';
+  Seq.eq_intro txt txt'
 
 (* * *********************************************)
 (* *        Poly1305 functional invariant        *)