Merge pull request #3318 from mtzguido/use_ampersand

All: replace all uses of `*` for tuples by `&`

examples/algorithms/GC.fst

@@ -34,8 +34,8 @@ type mem_addr  = i:int{is_mem_addr i}
 type color_map = mem_addr -> Tot color
 type abs_map   = mem_addr -> Tot abs_node
 
-type field_map     = mem_addr * field -> Tot mem_addr
-type abs_field_map = abs_node * field -> Tot abs_node
+type field_map     = mem_addr & field -> Tot mem_addr
+type abs_field_map = abs_node & field -> Tot abs_node
 
 type trigger (i:int) = True
 
@@ -283,8 +283,8 @@ let rec alloc root abs =
           let gc = get () in
           if gc.color ptr = Unalloc
           then
-          begin let fields = upd_map #(mem_addr * field) #mem_addr gc.fields (ptr, F1) ptr in
-                let fields = upd_map #(mem_addr * field) #mem_addr fields (ptr, F2) ptr in
+          begin let fields = upd_map #(mem_addr & field) #mem_addr gc.fields (ptr, F1) ptr in
+                let fields = upd_map #(mem_addr & field) #mem_addr fields (ptr, F2) ptr in
                 let gc' = { gc with
                               to_abs=upd_map gc.to_abs ptr abs;
                               color =upd_map gc.color ptr White;

examples/algorithms/Huffman.fst

@@ -96,7 +96,7 @@ let rec huffman_trie (ts:list trie) : Pure trie
       t
   | [t1] -> t1 (* this uses `existsb Node? [t] ==> Node? t` fact *)
 
-let huffman (sws:list (symbol*pos)) : Pure trie
+let huffman (sws:list (symbol&pos)) : Pure trie
     (requires (b2t (List.Tot.length sws > 0)))
     (ensures (fun t -> List.Tot.length sws > 1 ==> Node? t)) =
   huffman_trie (insertion_sort (List.Tot.map (fun (s,w) -> Leaf w s) sws))
@@ -125,7 +125,7 @@ let rec encode (t:trie) (ss:list symbol) : Pure (option (list bool))
 
 // A more complex decode I originally wrote
 
-let rec decode_one (t:trie) (bs:list bool) : Pure (option (symbol * list bool))
+let rec decode_one (t:trie) (bs:list bool) : Pure (option (symbol & list bool))
     (requires (True))
     (ensures (fun r -> Some? r ==>
                    (List.Tot.length (snd (Some?.v r)) <= List.Tot.length bs /\
@@ -222,7 +222,7 @@ let rec cancelation_aux (t:trie{Node? t}) (ss:list symbol) : Lemma
     | Some bs, Some bs' -> decode_prefix t bs bs' s
     | _, _ -> ())
 
-let rec cancelation (sws:list (symbol*pos)) (ss:list symbol) : Lemma
+let rec cancelation (sws:list (symbol&pos)) (ss:list symbol) : Lemma
   (requires (b2t (List.Tot.length sws > 1)))
   (ensures (List.Tot.length sws > 1 ==>
             (let t = huffman sws in

examples/algorithms/MergeSort.fst

@@ -22,7 +22,7 @@ type split_inv (l:list int) (l1:list int) (l2:list int) =
     (* needed for decreases clause in mergesort function *)
     length l > length l1 /\ length l > length l2
 
-val split: l:list int -> Pure (list int * list int)
+val split: l:list int -> Pure (list int & list int)
              (requires (Cons? l /\ Cons? (Cons?.tl l)))
 	     (ensures (fun r -> split_inv l (fst r) (snd r)))
 let rec split (x::y::l) =

examples/algorithms/MergeSort2.fst

@@ -95,7 +95,7 @@ let merge'_stable #a l r k = merge'_filter_eq_inv l r k
 
 (** split_n splits a list at index n **)
 val split_n: #a:eqtype -> (l:list a) -> n:nat{0 < n /\ n < length l} ->
-  Tot (l_tup:(list a * list a){(fst l_tup)@(snd l_tup) = l
+  Tot (l_tup:(list a & list a){(fst l_tup)@(snd l_tup) = l
     /\ length (fst l_tup) < length l
     /\ length (snd l_tup) < length l
     /\ permutation_2 l (fst l_tup) (snd l_tup)})
@@ -106,7 +106,7 @@ let rec split_n #a l n =
 
 (** split_half splits a list halfway **)
 val split_half: #a:eqtype -> (l:list a{length l >= 2}) ->
-  Tot (l_tup:(list a * list a))
+  Tot (l_tup:(list a & list a))
 let split_half #a l = split_n l ((length l) / 2)
 
 (** Define mergesort **)

examples/algorithms/QuickSort.List.fst

@@ -48,7 +48,7 @@ let rec mem_count #a x = function
   | [] -> ()
   | _::tl -> mem_count x tl
 
-val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
+val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a & list 'a)
 let rec partition f = function
   | [] -> [], []
   | hd::tl ->

examples/algorithms/QuickSort.Seq.fst

@@ -25,7 +25,7 @@ module Seq = FStar.Seq
 
 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} ->
-       Pure (seq a * seq a)
+       Pure (seq a & seq a)
          (requires (forall (i:nat{i < length s}).
                                  ((i <= pivot ==> f (index s i) (index s pivot))
                                   /\ (back < i  ==> f (index s pivot) (index s i)))))

examples/algorithms/Unification.fst

@@ -58,7 +58,7 @@ let rec vars = function
   | F t1 t2 -> OrdSet.union (vars t1) (vars t2)
 
 (* Equations among pairs of terms, to be solved *)
-type eqns  = list (term * term)
+type eqns  = list (term & term)
 
 (* All the variables in a set of equations *)
 val evars : eqns -> Tot varset
@@ -91,7 +91,7 @@ let rec n_flex_rhs = function
   | _::tl -> n_flex_rhs tl
 
 (* A point substitution *)
-type subst = (nat * term)
+type subst = (nat & term)
 
 (* Composition of point substitutions *)
 type lsubst = list subst

examples/crypto/CntFormat.fst

@@ -102,7 +102,7 @@ let signal s c =
   let c_b = uint16_to_bytes c in
   (s_b @| c_b)
 
-val signal_split : m:msg signal_size -> Tot (x:(uint32 * uint16)
+val signal_split : m:msg signal_size -> Tot (x:(uint32 & uint16)
     { m = signal (fst x) (snd x)})
 let signal_split sc =
     let (s_b, c_b) = Platform.Bytes.split_eq sc 4 in

examples/crypto/EtM.AE.fst

@@ -33,10 +33,10 @@ module Plain = EtM.Plain
 type rid = erid
 
 /// An AE cipher includes a mac tag
-type cipher = (CPA.cipher * MAC.tag)
+type cipher = (CPA.cipher & MAC.tag)
 
 /// An AE log pairs plain texts with MAC'd ciphers
-let log_entry = Plain.plain * cipher
+let log_entry = Plain.plain & cipher
 type log_t (r:rid) = m_rref r (seq log_entry) grows
 
 /// An AE key pairs an encryption key, ke, with a MAC'ing key, km,

examples/crypto/EtM.MAC.fst

@@ -54,7 +54,7 @@ let hmac_sha1 k t =
 (* Type log_t defined as follows (in ulib/FStar.Monotonic.Seq.fst):
    type log_t (i:rid) (a:Type) = m_rref i (seq a) grows *)
 
-let log_entry = msg * tag
+let log_entry = msg & tag
 let entry_message (l:log_entry) = fst l
 let entry_tag (l:log_entry) = snd l
 type log_t (r:rid) = m_rref r (seq log_entry) grows

examples/crypto/HyE.AE.fsti

@@ -35,7 +35,7 @@ type msg = Plain.t
 type cipher = b:bytes{B.length b >= ivsize}
 (* MK: minimal cipher length twice blocksize? *)
 
-type mlog_t (r:erid) = m_rref r (seq (msg * cipher)) grows
+type mlog_t (r:erid) = m_rref r (seq (msg & cipher)) grows
 
 val key : Type0
 

examples/crypto/HyE.CCA2.fsti

@@ -42,7 +42,7 @@ val access_pk_raw (pk:pkey) : RSA.pkey
 
 val skey : Type0
 
-val keygen: parent:rid{HyperStack.ST.witnessed (region_contains_pred parent)} -> ML (pkey * skey)
+val keygen: parent:rid{HyperStack.ST.witnessed (region_contains_pred parent)} -> ML (pkey & skey)
 
 val encrypt (pk:pkey) (p:PlainPKE.t) : ML RSA.cipher
 

examples/crypto/HyE.HCCA2.fsti

@@ -39,8 +39,8 @@ val access_pkraw (pk:pkey) : RSA.pkey
 val skey : Type0
 
 type p = P.t
-type c = C.cipher * A.cipher //lbytes(C.ciphersize + A.ciphersize)
+type c = C.cipher & A.cipher //lbytes(C.ciphersize + A.ciphersize)
 
-val keygen: parent:C.rid{HyperStack.ST.witnessed (region_contains_pred parent)} -> ML (pkey * skey)
+val keygen: parent:C.rid{HyperStack.ST.witnessed (region_contains_pred parent)} -> ML (pkey & skey)
 val encrypt: pkey -> p -> ML c
 val decrypt: skey -> c -> ML (option p )

examples/crypto/HyE.RSA.fst

@@ -42,7 +42,7 @@ assume val ciphersize : nat
 type plain   = lbytes plainsize
 type cipher  = lbytes ciphersize
 
-type keypair = pkey * skey
+type keypair = pkey & skey
 assume val generated : keypair -> Tot bool
 
 assume val gen: unit -> x:keypair{generated x}

examples/crypto/OPLSS.AE.fst

@@ -44,7 +44,7 @@ type key =
            }
        -> key
 
-let ae_cipher = AES.iv_cipher * HMACSHA1.tag
+let ae_cipher = AES.iv_cipher & HMACSHA1.tag
 
 let footprint (k:key) =
   B.loc_union (Log.fp k.mac.MAC.log)

examples/data_structures/ArrayRealized.fst

@@ -58,7 +58,7 @@ let update (Seq c j k) i v = Seq (__update__ c (i + j) v) j k
 val slice: s:seq 'a -> i:nat -> j:nat{(i <= j /\ j <= length s)} -> Tot (seq 'a)
 let slice (Seq c start_i end_i) i j = Seq c (start_i + i) (start_i + j)
 
-val split: s:seq 'a -> i:nat{(0 <= i /\ i < length s)} -> Tot (seq 'a * seq 'a)
+val split: s:seq 'a -> i:nat{(0 <= i /\ i < length s)} -> Tot (seq 'a & seq 'a)
 let split s i = slice s 0 i, slice s i (length s)
 
 val append: seq 'a -> seq 'a -> Tot (seq 'a)

examples/data_structures/BinaryTreesEnumeration.fsti

@@ -32,7 +32,7 @@ let product #a #b (l1: list a) (l2: list b) =
 
 type bin_tree =
 | Leaf
-| Branch of bin_tree * bin_tree
+| Branch of bin_tree & bin_tree
 
 let rec size bt : nat =
   match bt with
@@ -53,7 +53,7 @@ let rec trees_of_size (s: nat) : list (bt_with_size s) =
   else
     List.Tot.concatMap #(prod_with_sum (s - 1))
       (fun (s1, s2) ->
-       List.Tot.map #((bt_with_size s1) * (bt_with_size s2))
+       List.Tot.map #((bt_with_size s1) & (bt_with_size s2))
                     #(bt_with_size s)
          (fun (t1, t2) -> Branch (t1, t2))
          (product (trees_of_size s1) (trees_of_size s2)))
@@ -106,7 +106,7 @@ let pure_as_squash (#a:Type)
 let rec memP_append_aux #a (x: a) (l: list a) :
   Lemma
     (requires (List.memP x l))
-    (ensures (exists (l12: (list a * list a)). l == fst l12 @ x :: snd l12))
+    (ensures (exists (l12: (list a & list a)). l == fst l12 @ x :: snd l12))
     =  let goal = exists l12. l == fst l12 @ x :: snd l12 in
        let x : squash goal =
          match l with
@@ -131,7 +131,7 @@ let rec memP_append_aux #a (x: a) (l: list a) :
 let memP_append #a (x: a) (l: list a) :
   Lemma
     (ensures (List.memP x l ==>
-              (exists (l12: (list a * list a)). l == (fst l12) @ (x :: (snd l12))))) =
+              (exists (l12: (list a & list a)). l == (fst l12) @ (x :: (snd l12))))) =
   FStar.Classical.move_requires (memP_append_aux x) l
 
 (*> * Should this be in the stdlib? *)
@@ -264,7 +264,7 @@ let unfold_tos (s: nat) :
           else
             List.Tot.concatMap #(prod_with_sum (s - 1))
               (fun (s1, s2) ->
-               List.Tot.map #(bt_with_size s1 * bt_with_size s2)
+               List.Tot.map #(bt_with_size s1 & bt_with_size s2)
                             #(bt_with_size s)
                  (fun (t1, t2) -> Branch (t1, t2))
                  (product (trees_of_size s1) (trees_of_size s2)))
@@ -275,7 +275,7 @@ let unfold_tos (s: nat) :
                 else
                   List.Tot.concatMap #(prod_with_sum (s - 1))
                     (fun (s1, s2) ->
-                     List.Tot.map #(bt_with_size s1 * bt_with_size s2)
+                     List.Tot.map #(bt_with_size s1 & bt_with_size s2)
                                   #(bt_with_size s)
                        (fun (t1, t2) -> Branch (t1, t2))
                        (product (trees_of_size s1) (trees_of_size s2)))
@@ -318,7 +318,7 @@ let rec tos_complete (bt0: bin_tree) :
       product_complete trees1 trees2 t1 t2;
       (* assert (List.memP (t1, t2) (product trees1 trees2)); *)
 
-      memP_map_intro #(bt_with_size s1 * bt_with_size s2)
+      memP_map_intro #(bt_with_size s1 & bt_with_size s2)
         (fun (t1, t2) -> Branch (t1, t2) <: (bt_with_size s))
         (t1, t2)
         (product trees1 trees2);
@@ -337,7 +337,7 @@ let rec tos_complete (bt0: bin_tree) :
         (s1, s2)
         (Branch (t1, t2))
         (fun (s1, s2) ->
-         List.Tot.map #(bt_with_size s1 * bt_with_size s2)
+         List.Tot.map #(bt_with_size s1 & bt_with_size s2)
                       #(bt_with_size s)
            (fun (t1, t2) -> Branch (t1, t2))
            (product (trees_of_size s1) (trees_of_size s2)))

examples/data_structures/Lens.fst

@@ -158,7 +158,7 @@ let moveUp' (c:colored circle) (offset_y: int) =
 
 /// You can also build other kinds of lens combinator
 /// For example, focusing on two different parts of an object at once
-let ( || ) (l1:lens 'a 'b) (l2:lens 'a 'c) : lens 'a ('b * 'c) = {
+let ( || ) (l1:lens 'a 'b) (l2:lens 'a 'c) : lens 'a ('b & 'c) = {
   get = (fun a -> l1.get a, l2.get a);
   put = (fun (b, c) a -> l2.put c (l1.put b a))
 }

examples/data_structures/StatefulLens.fst

@@ -35,8 +35,8 @@ assume val upd_ref (#a:Type) (r:ref a) (v:a) : ST unit
 ///  hlens as pure lenses, rather than ghost lenses
 noeq
 type hlens a b = {
-     get: (heap * a) -> GTot b;
-     put: b -> (heap * a) -> GTot (heap * a)
+     get: (heap & a) -> GTot b;
+     put: b -> (heap & a) -> GTot (heap & a)
 }
 
 /// `hlens a b` is just like `Lens.lens (heap * a) b`, except it uses the GTot effect.
@@ -185,8 +185,8 @@ let ( |^. ) #a #b #c (#l:hlens b c) (m:lens a b) (sl:stlens l) = (~. m) |.. sl
 let ( |.^ ) #a #b #c (#l:hlens a b) (sl:stlens l) (m:lens b c) = sl |.. (~. m)
 let ( |. ) #a #b #c (m:lens a b) (n:lens b c) = Lens.(m |.. n)
 
-let ( .() ) #a #b (#l:hlens a b) (x:a) ($hs:(heap * stlens l)) = l.get (fst hs, x)
-let ( .()<- ) #a #b (#l:hlens a b) (x:a) ($hs:(heap * stlens l)) (y:b)  = l.put y (fst hs, x)
+let ( .() ) #a #b (#l:hlens a b) (x:a) ($hs:(heap & stlens l)) = l.get (fst hs, x)
+let ( .()<- ) #a #b (#l:hlens a b) (x:a) ($hs:(heap & stlens l)) (y:b)  = l.put y (fst hs, x)
 
 let move_x (delta:int) (c:circle) : ST unit
   (requires (fun _ -> True))

examples/data_structures/Vector.fst

@@ -67,7 +67,7 @@ let rec find f #n v = match v with
     then Some hd
     else find f tl
 
-val zip': #a:Type -> #b:Type -> #n:nat -> vector a n -> vector b n -> Tot (vector (a * b) n)
+val zip': #a:Type -> #b:Type -> #n:nat -> vector a n -> vector b n -> Tot (vector (a & b) n)
 let rec zip' #a #b #n v1 v2 = match v1 with
   | VNil -> VNil
   | VCons a tl1 ->

examples/dm4free/Effects.Def.fst

@@ -81,7 +81,7 @@ let morphism_laws_via_eq m n eqn return_m bind_m return_n bind_n lift = ()
 (* ******************************************************************************)
 assume type s : Type //an abstract type of the state
 
-let st (a:Type) = restricted_t s (fun _ -> a * s)
+let st (a:Type) = restricted_t s (fun _ -> a & s)
 
 let eq_st (a:Type) (x:st a) (y:st a) = is_restricted s x /\ is_restricted s y /\ feq x y //extensional equality on st
 
@@ -132,7 +132,7 @@ let ex_laws = monad_laws_via_eq ex eq_ex return_ex bind_ex
 (* ******************************************************************************)
 (* Effect (stexn a) : A combined monad, exceptions over state                   *)
 (* ******************************************************************************)
-let stexn (a:Type) = restricted_t s (fun _ -> (option a * s))
+let stexn (a:Type) = restricted_t s (fun _ -> (option a & s))
 
 let eq_stexn (a:Type) (x:stexn a) (y:stexn a) = is_restricted s x /\ is_restricted s y /\ feq x y
 
@@ -151,7 +151,7 @@ let stexn_laws = monad_laws_via_eq stexn eq_stexn return_stexn bind_stexn
 (* ******************************************************************************)
 (* Effect (exnst a) : A combined monad, state over exceptions                   *)
 (* ******************************************************************************)
-let exnst (a:Type) = restricted_t s (fun _ -> (option (a * s)))
+let exnst (a:Type) = restricted_t s (fun _ -> (option (a & s)))
 
 let eq_exnst (a:Type) (x:exnst a) (y:exnst a) = is_restricted s x /\ is_restricted s y /\ feq x y
 

examples/dm4free/FStar.DM4F.ExnSt.fst

@@ -25,7 +25,7 @@ module FStar.DM4F.ExnSt
 module IntST = FStar.DM4F.IntST
 
 (* The underlying representation type *)
-let exnst a = int -> M (option (a * int))
+let exnst a = int -> M (option (a & int))
 
 (* Monad definition *)
 val return : (a:Type) -> (x:a) -> exnst a
@@ -59,7 +59,7 @@ sub_effect IntST.STINT ~> EXNST {
 }
 
 (* Pre-/postcondition variant *)
-effect ExnSt (a:Type) (req:EXNST?.pre) (ens:int -> option (a * int) -> GTot Type0) =
+effect ExnSt (a:Type) (req:EXNST?.pre) (ens:int -> option (a & int) -> GTot Type0) =
        EXNST a
          (fun (h0:int) (p:EXNST?.post a) -> req h0 /\ (forall r. (req h0 /\ ens h0 r) ==> p r))
 
@@ -73,7 +73,7 @@ effect S (a:Type) =
  * doesn't modify the state.
  *)
 
-let div_intrisic_spec (i :nat) (j:int) (h0:int) (x:option (int * int)) : Type0 =
+let div_intrisic_spec (i :nat) (j:int) (h0:int) (x:option (int & int)) : Type0 =
   match x with
   | None -> j=0
   | Some (z, h1) -> h0 = h1 /\ j<>0 /\ z = i / j

examples/dm4free/FStar.DM4F.Heap.ST.fsti

@@ -195,7 +195,7 @@ let refine_st (#a:Type)
                               reify (f x) h0 == (z, h1) /\
                               post x h0 z h1)
   = let g (h0:heap)
-      : Pure (b * heap)
+      : Pure (b & heap)
              (pre x h0)
              (fun (z,h1) -> pre x h0 /\
                        reify (f x) h0 == (z, h1) /\

examples/dm4free/FStar.DM4F.Heap.fsti

@@ -50,7 +50,7 @@ val upd: #a:Type -> h0:heap -> r:ref a -> x:a
                   -> GTot heap
 (* Generating a fresh reference for the given heap. *)
 
-val alloc: #a:Type -> h0:heap -> x:a -> Tot (t:(ref a * heap){snd t == upd h0 (fst t) x})
+val alloc: #a:Type -> h0:heap -> x:a -> Tot (t:(ref a & heap){snd t == upd h0 (fst t) x})
 
 val contains (#a:Type) (h:heap) (r:ref a): Tot Type0