fix stdlib (manual clones)

examples/ChaChaPoly/chacha_poly.ec

@@ -80,14 +80,17 @@ theory C.
 
   axiom gt0_max_counter : 0 < max_counter.
 
+  type counter.
+
   clone include Subtype with 
-    type T <- int,
-    op P <- fun (i:int) => 0 <= i < max_counter + 1
-    rename (* [type] "sT" as "counter" *) (* Gives error. *)
-           [op] "insubd" as "ofint"
-  proof *.
-  realize inhabited. exists 0. smt(gt0_max_counter). qed.
-  type counter = sT.
+    type sT <- counter,
+    type T  <- int,
+    pred P  <- fun (i:int) => 0 <= i < max_counter + 1
+    rename [op] "insubd" as "ofint"
+    proof *.
+
+  realize inhabited.
+  proof. by exists 0; smt(gt0_max_counter). qed.
 
   clone FinType with 
     type t  = counter,
@@ -116,16 +119,20 @@ abstract theory GenBlock.
   op block_size : int.
   axiom ge0_block_size : 0 <= block_size.
 
+  type block.
+
   clone include Subtype with
-    type T <- bytes, 
-    op P <- fun (l:bytes) => size l = block_size
+    type sT <- block,
+    type  T <- bytes, 
+    pred  P <- fun (l:bytes) => size l = block_size
     rename [op] "val" as "bytes_of_block"
   proof *.
+
   realize inhabited.
+  proof.
     exists (nseq block_size witness).
     smt(size_nseq ge0_block_size).
   qed.
-  type block = sT.
 
   op dblock =  dmap (dlist dbyte block_size) insubd.
 

examples/MEE-CBC/FunctionalSpec.ec

@@ -492,7 +492,6 @@ proof.
                       (size (pad _p (hmac_sha256 _mk _p)))
                       (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
                                    (size (pad _p (hmac_sha256 _mk _p)))).
-        smt().
       split=> //=.
       split; 1:by rewrite /mee_enc /= size_cbc_enc addzC.
       by rewrite take_size.

src/ecTheoryReplay.ml

@@ -246,22 +246,33 @@ let operator_compatible env oper1 oper2 =
   | _                 , _                  -> raise exn
 
 (* -------------------------------------------------------------------- *)
-let check_evtags (tags : evtags) (src : symbol list) =
-  let module E = struct exception Reject end in
+let check_evtags ?(tags : evtags option) (src : symbol list) =
+  let exception Reject in
+
+  let explicit = "explicit" in
 
   try
-    let dfl = not (List.exists (fun (mode, _) -> mode = `Include) tags) in
-    let stt =
-      List.map (fun src ->
-        let do1 status (mode, dst) =
-          match mode with
-          | `Exclude -> if sym_equal src dst then raise E.Reject; status
-          | `Include -> status || (sym_equal src dst)
-        in List.fold_left do1 dfl tags)
-        src
-    in List.mem true stt
-
-  with E.Reject -> false
+    match tags with
+    | None ->
+      if List.mem explicit src then
+        raise Reject;
+      true
+
+    | Some tags ->
+      let dfl =
+        not (List.mem explicit src) &&
+        not (List.exists (fun (mode, _) -> mode = `Include) tags) in
+      let stt =
+        List.map (fun src ->
+          let do1 status (mode, dst) =
+            match mode with
+            | `Exclude -> if sym_equal src dst then raise Reject; status
+            | `Include -> status || (sym_equal src dst)
+          in List.fold_left do1 dfl tags)
+          src
+      in List.mem true stt
+
+  with Reject -> false
 
 (* -------------------------------------------------------------------- *)
 let xpath ove x =
@@ -691,9 +702,13 @@ and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) =
       match Msym.find_opt x (ove.ovre_ovrd.evc_lemmas.ev_bynames) with
       | Some (pt, hide, explicit) -> Some (pt, hide, explicit)
       | None when is_axiom ax.ax_kind ->
-          List.Exceptionless.find_map
-            (function (pt, None) -> Some (pt, `Alias, false) | (pt, Some pttags) ->
-               if check_evtags pttags (Ssym.elements tags) then
+          List.Exceptionless.find_map (function
+            | (pt, None) ->
+              if check_evtags (Ssym.elements tags) then
+                Some (pt, `Alias, false)
+              else None
+            | (pt, Some pttags) ->
+               if check_evtags ~tags:pttags (Ssym.elements tags) then
                  Some (pt, `Alias, false)
                else None)
             ove.ovre_glproof

theories/algebra/Poly.ec

@@ -23,18 +23,18 @@ op ispoly (p : prepoly) =
       (forall c, c < 0 => p c = zeror)
     /\ (exists d, forall c, (d < c)%Int => p c = zeror).
 
+type poly.
+
 clone include Subtype
-  with type T   <- prepoly,
-       op P   <- ispoly
+  with type sT <- poly,
+       type T <- prepoly,
+       pred P <- ispoly
   rename "insub" as "to_poly"
   rename "val"   as "of_poly"
 proof *.
+
 realize inhabited.
-  exists (fun _, zeror).
-  rewrite /ispoly.
-  auto.
-qed.
-type poly = sT.
+proof. by exists (fun _ => zeror). qed.
 
 op "_.[_]" (p : poly) (i : int) = (of_poly p) i.
 

theories/algebra/ZModP.ec

@@ -11,15 +11,16 @@ abstract theory ZModRing.
 const p : { int | 2 <= p } as ge2_p.
 
 (* -------------------------------------------------------------------- *)
+type zmod.
+
 clone Subtype as Sub with
-  type T <- int,
-  op P (x : int) <- 0 <= x < p
+  type sT <- zmod,
+  type  T <- int,
+  pred  P <- fun (x : int) => 0 <= x < p
 proof *.
-realize inhabited.
-exists 0. smt(ge2_p).
-qed.
 
-type zmod = Sub.sT.
+realize inhabited.
+proof. by exists 0; smt(ge2_p). qed.
 
 (* -------------------------------------------------------------------- *)
 op inzmod (z : int)  = Sub.insubd (z %% p).

theories/datatypes/Word.eca

@@ -14,13 +14,17 @@ op wordw : t list = mkseq (fun _ => dchar) n.
 lemma size_wordw: size wordw = n.
 proof. by rewrite size_mkseq ler_maxr ?ge0_n. qed.
 
-clone include Subtype
-  with type T   <- t list,
-       op P   <- fun w => size w = n
-proof *.
-realize inhabited by exists wordw; exact size_wordw.
+type word.
+
+clone include Subtype with
+  type sT <- word,
+  type T  <- t list,
+  pred P  <- fun w => size w = n
+  proof *.
+
+realize inhabited.
+proof. by exists wordw; exact size_wordw. qed.
 
-type word = sT.
 (* default value chosen for backward compatibility *)
 op mkword x = odflt (insubd wordw) (insub x).
 op ofword = val.

theories/datatypes/Xreal.ec

@@ -62,15 +62,17 @@ end MonoidDI.
 
 theory Rp.
 
-clone include Subtype
-  with type T <- real,
-       op P <- fun x => 0.0 <= x
+type realp.
+
+clone include Subtype with
+   type sT <- realp,
+   type T  <- real,
+   pred P  <- fun x => 0.0 <= x
    rename "insubd" as "of_real"
    rename "val" as "to_real"
-proof*.
-realize inhabited by exists 0%r.
+proof *.
 
-type realp = sT.
+realize inhabited by exists 0%r.
 
 abbrev (%r) = to_real.
 abbrev (%rp) = of_real.

theories/structure/Quotient.ec

@@ -87,16 +87,17 @@ apply/(eqv_trans (canon x)); first by apply/eqv_canon.
 by rewrite eq &(eqv_refl).
 qed.
 
+type qT.
+
 clone import Subtype with
+  type sT <- qT,
   type T  <- T,
-  op P  <- iscanon
+  pred P  <- iscanon
 proof *.
+
 realize inhabited.
-smt(canonK).
-qed.
+proof. smt(canonK). qed.
 
-type qT = sT.
-
 clone include CoreQuotient with
   type T     <- T,
   type qT    <- qT,

theories/structure/Subtype.eca

@@ -27,11 +27,11 @@ op val   : sT -> T.
 
 axiom [prove] inhabited : exists x, P x.
 
-axiom insubN (x : T): !P x => insub x = None.
-axiom insubT (x : T):  P x => omap val (insub x) = Some x.
+axiom [explicit] insubN (x : T): !P x => insub x = None.
+axiom [explicit] insubT (x : T):  P x => omap val (insub x) = Some x.
 
-axiom valP (x : sT): P (val x).
-axiom valK: pcancel val insub.
+axiom [explicit] valP (x : sT): P (val x).
+axiom [explicit] valK: pcancel val insub.
 
 (* -------------------------------------------------------------------- *)
 op insubd (x : T) = odflt witness (insub x).