get rid of axiomatized by in favor of [opaque] with trivial lemma

examples/MEE-CBC/FunctionalSpec.ec

@@ -12,10 +12,7 @@ clone import BitWord as Octet with
   op n <- 8
 rename "word" as "octet"
 rename "Word" as "Octet"
-proof *.
-realize gt0_n by trivial.
-realize getE by rewrite /"_.[_]".
-realize setE by rewrite /"_.[_<-_]".
+proof * by trivial.
 
 op o2int (o : octet) : int = bs2int (ofoctet o).
 op int2o (i : int) : octet = mkoctet (int2bs 8 i).
@@ -41,8 +38,6 @@ rename "Word" as "Block"
 proof *.
 realize Alphabet.enum_spec by exact/Octet.enum_spec.
 realize ge0_n by trivial.
-realize getE by rewrite /"_.[_]".
-realize setE by rewrite /"_.[_<-_]".
 
 abbrev dblock = DBlock.dunifin.
 
@@ -136,8 +131,6 @@ rename "Word" as "Tag"
 proof *.
 realize Alphabet.enum_spec by exact/Octet.enum_spec.
 realize ge0_n by trivial.
-realize getE by rewrite /"_.[_]".
-realize setE by rewrite /"_.[_<-_]".
 
 (** Messages are just octet lists **)
 type msg = octet list.

theories/algebra/Group.ec

@@ -456,11 +456,11 @@ type exp = ZModE.exp.
 import ZModE.
 
 (* -------------------------------------------------------------------- *)
-op (^)  (x : group) (k : exp) = x ^ (asint k)
-axiomatized by expE.
+op [opaque] (^)  (x : group) (k : exp) = x ^ (asint k).
+lemma expE x (k: exp): (^) x k = x ^ (asint k) by rewrite /(^).
 
-op loge (x : group) : exp = inzmod (log x)
-axiomatized by logE.
+op [opaque] loge (x : group) : exp = inzmod (log x).
+lemma logE (x: group) : loge x = inzmod (log x) by rewrite /loge.
 
 (* -------------------------------------------------------------------- *)
 abbrev root (k : exp) (x : group) = x ^ (inv k).

theories/algebra/IntDiv.ec

@@ -18,18 +18,26 @@ op euclidef (m d : int) (qr : int * int) =
      m = qr.`1 * d + qr.`2
   /\ (d <> 0 => 0 <= qr.`2 < `|d|).
 
-op edivn (m d : int) =
+op [opaque] edivn (m d : int) =
   if (d < 0 \/ m < 0) then (0, 0) else
-    if d = 0 then (0, m) else choiceb (euclidef m d) (0, 0)
-  axiomatized by edivn_def.
+    if d = 0 then (0, m) else choiceb (euclidef m d) (0, 0).
+lemma edivn_def (m d: int): edivn m d = 
+  if (d < 0 \/ m < 0) then (0, 0) else
+    if d = 0 then (0, m) else choiceb (euclidef m d) (0, 0).
+proof. by rewrite /edivn. qed.
 
-op edivz (m d : int) =
+op [opaque] edivz (m d : int) =
+  let (q, r) =
+    if 0 <= m then edivn m `|d| else
+      let (q, r) = edivn (-(m+1)) `|d| in
+      (- (q + 1), `|d| - 1 - r)
+    in (signz d * q, r).
+lemma edivz_def (m d: int): edivz m d =
   let (q, r) =
     if 0 <= m then edivn m `|d| else
       let (q, r) = edivn (-(m+1)) `|d| in
       (- (q + 1), `|d| - 1 - r)
-    in (signz d * q, r)
-  axiomatized by edivz_def.
+    in (signz d * q, r) by rewrite/edivz.
 
 abbrev (%/) (m d : int) = (edivz m d).`1.
 abbrev (%%) (m d : int) = (edivz m d).`2.

theories/crypto/assumptions/DHIES.ec

@@ -9,7 +9,9 @@ pragma -implicits.
 pragma +oldip.
 
 (* an "eval safe" version of [dlet] *)
-op dlet_locked ['a, 'b] = dlet<:'a, 'b> axiomatized by dlet_lockedE.
+op [opaque] dlet_locked ['a, 'b] = dlet<:'a, 'b>. 
+lemma dlet_lockedE: dlet_locked<:'a, 'b> = dlet<:'a, 'b>.
+proof. by rewrite/dlet_locked. qed.
 
 theory DHIES.
 

theories/datatypes/Array.ec

@@ -22,15 +22,19 @@ lemma ofarray_inj: injective ofarray<:'a>.
 proof. by apply/(can_inj _ _ mkarrayK). qed.
 
 (* -------------------------------------------------------------------- *)
-op size (arr : 'a array) = size (ofarray arr)
-axiomatized by sizeE.
-
-op "_.[_]" (arr : 'a array) (i : int) = nth witness (ofarray arr) i
-axiomatized by getE.
-
-op "_.[_<-_]" (arr : 'a array) (i : int) (x : 'a) =
-  mkarray (mkseq (fun k => if i = k then x else arr.[k]) (size arr))
-axiomatized by setE.
+op [opaque] size (arr : 'a array) = size (ofarray arr).
+lemma sizeE (arr: 'a array): size arr = size (ofarray arr).
+proof. by rewrite/size. qed.
+
+op [opaque] "_.[_]" (arr : 'a array) i = nth witness (ofarray arr) i.
+lemma getE (arr: 'a array) i: arr.[i] = nth witness (ofarray arr) i.
+proof. by rewrite/"_.[_]". qed.
+
+op [opaque] "_.[_<-_]" (arr : 'a array) (i : int) (x : 'a) =
+  mkarray (mkseq (fun k => if i = k then x else arr.[k]) (size arr)).
+lemma setE (arr : 'a array) (i : int) (x : 'a): arr.[i<-x] =
+  mkarray (mkseq (fun k => if i = k then x else arr.[k]) (size arr)).
+proof. by rewrite /"_.[_<-_]". qed.
 
 (* -------------------------------------------------------------------- *)
 lemma size_ge0 (arr : 'a array): 0 <= size arr.

theories/datatypes/FMap.ec

@@ -25,9 +25,9 @@ proof. by []. qed.
 abbrev (\in)    ['a 'b] x (m : ('a, 'b) fmap) = (dom m x).
 abbrev (\notin) ['a 'b] x (m : ('a, 'b) fmap) = ! (dom m x).
 
-op rng ['a 'b] (m : ('a, 'b) fmap) =
-  fun y => exists x, m.[x] = Some y
-axiomatized by rngE.
+op [opaque] rng ['a 'b] (m : ('a, 'b) fmap) = fun y => exists x, m.[x] = Some y.
+lemma rngE (m : ('a, 'b) fmap): 
+  rng m = fun y => exists x, m.[x] = Some y by rewrite /rng.
 
 lemma get_none (m : ('a, 'b) fmap, x : 'a) :
   x \notin m => m.[x] = None.
@@ -458,8 +458,9 @@ case: (y = x) => [->|] /=; case: (p x b) => /=.
 qed.
 
 (* ==================================================================== *)
-op fdom ['a 'b] (m : ('a, 'b) fmap) =
-  oflist (to_seq (dom m)) axiomatized by fdomE.
+op [opaque] fdom ['a 'b] (m : ('a, 'b) fmap) = oflist (to_seq (dom m)).
+lemma fdomE (m : ('a, 'b) fmap): fdom m = oflist (to_seq (dom m)).
+proof. by rewrite/fdom. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma mem_fdom ['a 'b] (m : ('a, 'b) fmap) (x : 'a) :
@@ -512,8 +513,9 @@ lemma mem_fdom_rem ['a 'b] (m : ('a, 'b) fmap) x y :
 proof. by rewrite fdom_rem in_fsetD1. qed.
 
 (* ==================================================================== *)
-op frng ['a 'b] (m : ('a, 'b) fmap) =
-  oflist (to_seq (rng m)) axiomatized by frngE.
+op [opaque] frng ['a 'b] (m : ('a, 'b) fmap) = oflist (to_seq (rng m)).
+lemma frngE (m : ('a, 'b) fmap): frng m = oflist (to_seq (rng m)).
+proof. by rewrite/frng. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma mem_frng ['a 'b] (m : ('a, 'b) fmap) (y : 'b) :
@@ -590,9 +592,10 @@ by apply/fsetP=> x; rewrite mem_fdom mem_join in_fsetU !mem_fdom.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op has (P : 'a -> 'b -> bool) (m : ('a, 'b) fmap) =
-  has (fun x=> P x (oget m.[x])) (elems (fdom m))
-axiomatized by hasE.
+op [opaque] has (P : 'a -> 'b -> bool) (m : ('a, 'b) fmap) =
+  has (fun x=> P x (oget m.[x])) (elems (fdom m)).
+lemma hasE (P : 'a -> 'b -> bool) m: 
+  has P m = has (fun x=>P x (oget m.[x])) (elems (fdom m)) by rewrite/has.
 
 (* -------------------------------------------------------------------- *)
 lemma hasP (P : 'a -> 'b -> bool) (m : ('a, 'b) fmap):
@@ -604,9 +607,11 @@ by split=> [Pxy|/>]; exists y.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op find (P : 'a -> 'b -> bool) (m : ('a, 'b) fmap) =
-  onth (elems (fdom m)) (find (fun x=> P x (oget m.[x])) (elems (fdom m)))
-axiomatized by findE.
+op [opaque] find (P : 'a -> 'b -> bool) (m : ('a, 'b) fmap) =
+  onth (elems (fdom m)) (find (fun x=> P x (oget m.[x])) (elems (fdom m))).
+lemma findE (P : 'a -> 'b -> bool) m: find P m =
+  onth (elems (fdom m)) (find (fun x=> P x (oget m.[x])) (elems (fdom m))).
+proof. by rewrite/find. qed.
 
 (* -------------------------------------------------------------------- *)
 

theories/datatypes/FSet.ec

@@ -60,11 +60,12 @@ lemma perm_eq_oflistP (s1 s2 : 'a list):
 proof. by split; [apply perm_eq_oflist | apply oflist_perm_eq_undup]. qed.
 
 (* -------------------------------------------------------------------- *)
-op card ['a] (s : 'a fset) = size (elems s) axiomatized by cardE.
+op [opaque] card ['a] (s : 'a fset) = size (elems s). 
+lemma cardE (s : 'a fset): card s = size (elems s) by rewrite/card.
 
 (* -------------------------------------------------------------------- *)
-op mem ['a] (s : 'a fset) (x : 'a) = mem (elems s) x
-  axiomatized by memE.
+op [opaque] mem ['a] (s : 'a fset) (x : 'a) = mem (elems s) x.
+lemma memE (s : 's fset) x: mem s x = mem (elems s) x by rewrite /mem.
 
 abbrev (\in)    (z : 'a) (s : 'a fset) =  mem s z.
 abbrev (\notin) (z : 'a) (s : 'a fset) = !mem s z.
@@ -84,17 +85,25 @@ by move=> x; rewrite -!memE h.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op fset0 ['a] = oflist [<:'a>] axiomatized by set0E.
-op fset1 ['a] (z : 'a) = oflist [z] axiomatized by set1E.
+op [opaque] fset0 ['a] = oflist [<:'a>]. 
+lemma set0E: fset0<:'a> = oflist [<:'a>] by rewrite/fset0.
 
-op (`|`) ['a] (s1 s2 : 'a fset) = oflist (elems s1 ++ elems s2)
-  axiomatized by setUE.
+op [opaque] fset1 ['a] (z : 'a) = oflist [z].
+lemma set1E (z : 'a): fset1 z = oflist [z] by rewrite/fset1.
 
-op (`&`) ['a] (s1 s2 : 'a fset) = oflist (filter (mem s2) (elems s1))
-  axiomatized by setIE.
+op [opaque] (`|`) ['a] (s1 s2 : 'a fset) = oflist (elems s1 ++ elems s2).
+lemma setUE (s1 s2 : 'a fset): s1 `|` s2 = oflist (elems s1 ++ elems s2).
+proof. by rewrite/(`|`). qed.
 
-op (`\`) ['a] (s1 s2 : 'a fset) = oflist (filter (predC (mem s2)) (elems s1))
-  axiomatized by setDE.
+op [opaque] (`&`) ['a] (s1 s2 : 'a fset) = 
+  oflist (filter (mem s2) (elems s1)).
+lemma setIE (s1 s2 : 'a fset): 
+  s1 `&` s2 = oflist (filter (mem s2) (elems s1)) by rewrite/(`&`).
+
+op [opaque] (`\`) ['a] (s1 s2 : 'a fset) = 
+  oflist (filter (predC (mem s2)) (elems s1)).
+lemma setDE (s1 s2 : 'a fset): 
+  s1 `\` s2 = oflist (filter (predC (mem s2)) (elems s1)) by rewrite/(`\`).
 
 (* -------------------------------------------------------------------- *)
 lemma in_fset0: forall x, mem fset0<:'a> x <=> false.
@@ -201,8 +210,8 @@ right; by rewrite all_xs_not_in_ys.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op pick ['a] (A : 'a fset) = head witness (elems A)
-axiomatized by pickE.
+op [opaque] pick ['a] (A : 'a fset) = head witness (elems A).
+lemma pickE (A : 'a fset): pick A = head witness (elems A) by rewrite/pick.
 
 lemma pick0: pick<:'a> fset0 = witness.
 proof. by rewrite pickE elems_fset0. qed.
@@ -214,9 +223,10 @@ by move=> /(mem_head_behead witness) <-.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op filter ['a] (p : 'a -> bool) (s : 'a fset) =
-  oflist (filter p (elems s))
-axiomatized by filterE.
+op [opaque] filter ['a] (p : 'a -> bool) (s : 'a fset) =
+  oflist (filter p (elems s)).
+lemma filterE (p: 'a -> bool) s: filter p s = oflist (filter p (elems s)).
+proof. by rewrite/filter. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma in_filter (p : 'a -> bool) (s : 'a fset):
@@ -612,8 +622,10 @@ by apply: contraL o_cA => ->; rewrite fcards0.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op image (f: 'a -> 'b) (A : 'a fset): 'b fset = oflist (map f (elems A))
-  axiomatized by imageE.
+op [opaque] image (f: 'a -> 'b) (A : 'a fset): 'b fset = 
+  oflist (map f (elems A)).
+lemma imageE (f: 'a -> 'b) A: image f A = oflist (map f (elems A)).
+proof. by rewrite/image. qed.
 
 lemma imageP (f : 'a -> 'b) (A : 'a fset) (b : 'b):
   mem (image f A) b <=> (exists a, mem A a /\ f a = b).
@@ -686,9 +698,11 @@ by rewrite /image /card -(perm_eq_size _ _ uniq_f) size_map.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op product (A : 'a fset) (B : 'b fset): ('a * 'b) fset =
-  oflist (allpairs (fun x y => (x,y)) (elems A) (elems B))
-axiomatized by productE.
+op [opaque] product (A : 'a fset) (B : 'b fset): ('a * 'b) fset =
+  oflist (allpairs (fun x y => (x,y)) (elems A) (elems B)).
+lemma productE (A : 'a fset) (B : 'b fset):
+  product A B = oflist (allpairs (fun x y => (x,y)) (elems A) (elems B)).
+proof. by rewrite/product. qed.
 
 lemma productP (A : 'a fset) (B : 'b fset) (a : 'a) (b : 'b):
   (a, b) \in product A B <=> (a \in A) /\ (b \in B).
@@ -704,9 +718,10 @@ apply allpairs_uniq; smt(uniq_elems).
 qed.
 
 (* -------------------------------------------------------------------- *)
-op fold (f : 'a -> 'b -> 'b) (z : 'b) (A : 'a fset) : 'b =
-  foldr f z (elems A)
-  axiomatized by foldE.
+op [opaque] fold (f : 'a -> 'b -> 'b) (z : 'b) (A : 'a fset) : 'b =
+  foldr f z (elems A).
+lemma foldE (f : 'a -> 'b -> 'b) z A: fold f z A = foldr f z (elems A).
+proof. by rewrite/fold. qed.
 
 lemma fold0 (f : 'a -> 'b -> 'b) (z : 'b): fold f z fset0 = z.
 proof. by rewrite foldE elems_fset0. qed.

theories/datatypes/Word.eca

@@ -64,13 +64,17 @@ by rewrite -(@ofwordK s1) // -(@ofwordK s2) // eq_mkword.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op "_.[_]" (w : word) (i : int): t =
-  if 0 <= i < n then nth witness (ofword w) i else dchar
-axiomatized by getE.
-
-op "_.[_<-_]" (w : word) (i : int) (x : t) : word =
-  mkword (mkseq (fun k => if i = k then x else w.[k]) n)
-axiomatized by setE.
+op [opaque] "_.[_]" (w : word) (i : int): t =
+  if 0 <= i < n then nth witness (ofword w) i else dchar.
+lemma getE w i: 
+  w.[i] = if 0 <= i < n then nth witness (ofword w) i else dchar.
+proof. by rewrite/"_.[_]". qed.
+
+op [opaque] "_.[_<-_]" (w : word) (i : int) (x : t) : word =
+  mkword (mkseq (fun k => if i = k then x else w.[k]) n).
+lemma setE w i x: 
+  w.[i<-x] = mkword (mkseq (fun k => if i = k then x else w.[k]) n).
+proof. by rewrite/"_.[_<-_]". qed.
 
 (* -------------------------------------------------------------------- *)
 lemma wordP (w1 w2 : word):

theories/distributions/DList.ec

@@ -2,9 +2,11 @@
 require import AllCore List FSet Distr DProd StdOrder StdBigop.
 (*---*) import Bigreal Bigreal.BRM MUnit.
 
-op dlist (d : 'a distr) (n : int): 'a list distr =
-  fold (fun d' => dapply (fun (xy : 'a * 'a list) => xy.`1 :: xy.`2) (d `*` d')) (dunit []) n
-  axiomatized by dlist_def.
+op [opaque] dlist (d : 'a distr) (n : int): 'a list distr =
+  fold (fun d' => dapply (fun (xy : 'a * 'a list) => xy.`1 :: xy.`2) (d `*` d')) (dunit []) n.
+lemma dlist_def (d : 'a distr) n: dlist d n = fold 
+  (fun d' => dapply (fun (xy : 'a * 'a list) => xy.`1 :: xy.`2) (d `*` d')) 
+  (dunit []) n by rewrite/dlist.
 
 lemma dlist0 (d : 'a distr) n: n <= 0 => dlist d n = dunit [].
 proof. by move=> ge0_n; rewrite dlist_def foldle0. qed.

theories/distributions/Distr.ec

@@ -1738,9 +1738,10 @@ pose s' := undup _; apply/(@ler_trans (big predT (fun x => ma x) s')).
 by apply/le1_sum_isdistr/undup_uniq.
 qed.
 
-op (`*`) (da : 'a distr) (db : 'b distr) =
-  mk (mprod (mu1 da) (mu1 db))
-axiomatized by dprod_def.
+op [opaque] (`*`) (da : 'a distr) (db : 'b distr) = 
+  mk (mprod (mu1 da) (mu1 db)).
+lemma dprod_def (da : 'a distr) (db : 'b distr):
+  da `*` db = mk (mprod (mu1 da) (mu1 db)) by rewrite/(`*`).
 
 lemma dprod1E (da : 'a distr) (db : 'b distr) a b:
   mu1 (da `*` db) (a,b) = mu1 da a * mu1 db b.
@@ -2019,11 +2020,13 @@ have := dprod_dmap_cross da db dc dd idfun idfun F1 idfun idfun F2 _.
 qed.
 
 (* -------------------------------------------------------------------- *)
-op djoin (ds : 'a distr list) : 'a list distr =
+op [opaque] djoin (ds : 'a distr list) : 'a list distr =
  foldr
    (fun d1 dl => dapply (fun xy : _ * _ => xy.`1 :: xy.`2) (d1 `*` dl))
-   (dunit []) ds
- axiomatized by djoin_axE.
+   (dunit []) ds.
+lemma djoin_axE (ds : 'a distr list): djoin ds = foldr
+   (fun d1 dl => dapply (fun xy : _ * _ => xy.`1 :: xy.`2) (d1 `*` dl))
+   (dunit []) ds by rewrite/djoin.
 
 abbrev djoinmap ['a 'b] (d : 'a -> 'b distr) xs = djoin (map d xs).
 

theories/prelude/Logic.ec

@@ -1,3 +1,6 @@
+(* This theory is in the prelude, so it cannot be checked directly      *)
+(* Run easycrypt via the commandline with a `-boot` flag instead        *)
+
 (* -------------------------------------------------------------------- *)
 require import Tactics.
 
@@ -91,8 +94,8 @@ abbrev [-printing] transpose ['a 'b 'c] (f : 'a -> 'b -> 'c) (y : 'b) =
 lemma transposeP ['a, 'b, 'c] (f : 'a -> 'b -> 'c) (x : 'a) (y : 'b) : f x y = transpose f y x by done.
 
 (* -------------------------------------------------------------------- *)
-op eta_ (f : 'a -> 'b) = fun x => f x
-  axiomatized by etaE.
+op [opaque] eta_ (f : 'a -> 'b) = fun x => f x.
+lemma etaE (f : 'a -> 'b): eta_ f = fun x => f x by rewrite/eta_.
 
 (* -------------------------------------------------------------------- *)
 op (\o) ['a 'b 'c] (g : 'b -> 'c) (f : 'a -> 'b) =
@@ -690,5 +693,6 @@ lemma semptyNP ['a] (E : 'a -> bool) :
 proof. by rewrite /sempty -negb_exists. qed.
 
 (* Locking (use with `rewrite [...]lock /= unlock`) *)
-op locked (x : 'a) = x axiomatized by unlock.
+op [opaque] locked (x : 'a) = x. 
+lemma unlock (x : 'a) : locked x = x by rewrite/locked.
 lemma lock (x : 'a) : x = locked x by rewrite unlock.