feat: new source-documented lazy/eager logic.

This logic is deliberately slightly less expressive than the one it
replaces, which does not hinder usability in any cryptographic context,
with the hope that it is simpler to maintain and verify.

Author: loutr

examples/PRG.ec

@@ -340,11 +340,8 @@ section.
     by wp; rnd; wp; rnd{2}; auto; rewrite dseed_ll.
   (* presampling ~ postsampling *)
   seq 2 2: (={glob A, glob F, glob Plog}); first by sim.
-  eager (H: Resample.resample(); ~ Resample.resample();
-    : ={glob Plog} ==> ={glob Plog})
-    : (={glob A, glob Plog, glob F})=> //;
-    first by sim.
-  eager proc H (={glob Plog, glob F})=> //.
+  eager call (: ={glob Plog, glob A, glob F}).
+  eager proc (={glob Plog, glob F}) => //; try sim.
   + eager proc; inline Resample.resample.
     swap{1} 3 3. swap{2} [4..5] 2. swap{2} [6..8] 1.
     swap{1} 4 3. swap{1} 4 2. swap{2} 2 4.
@@ -357,10 +354,9 @@ section.
       by wp; rnd{2}; auto=> />; smt (size_ge0).
     rcondt{2} 1; first by move=> &hr; auto=> /#.
     rcondf{2} 3; first by move=> &hr; auto=> /#.
-  + by sim.
-  + by sim.
+    by sim.
   + by eager proc; swap{1} 1 4; sim.
-  by sim.
+  by auto.
   qed.
 
   lemma P_PrgI &m:

examples/UC/RndO.ec

@@ -681,8 +681,7 @@ lemma eager_D :
          D(RRO).distinguish, RRO.resample(); :
          ={glob D, FRO.m} ==> ={FRO.m, glob D} /\ ={res}].
 proof.
-  eager proc (H_: RRO.resample(); ~ RRO.resample();: ={FRO.m} ==> ={FRO.m})
-             (={FRO.m}) =>//; try by sim.
+  eager proc (={FRO.m}) => //; try by sim.
   + by apply eager_init. + by apply eager_get. + by apply eager_set. 
   + by apply eager_rem. + by apply eager_sample. 
   + by apply eager_in_dom. + by apply eager_restrK. 

src/ecEnv.ml

@@ -2360,7 +2360,7 @@ module NormMp = struct
     match item with
     | MI_Module me -> mod_use env rm fdone us (EcPath.mqname mp me.me_name)
     | MI_Variable v -> add_var env (xpath mp v.v_name) us
-    | MI_Function f -> fun_use_aux env rm fdone us (xpath mp f.f_name)
+    | MI_Function f -> gen_fun_use env fdone rm us (xpath mp f.f_name)
 
   and body_use env rm fdone mp us comps body =
     match body with
@@ -2372,9 +2372,6 @@ module NormMp = struct
     | ME_Structure ms ->
       List.fold_left (item_use env rm fdone mp) us ms.ms_body
 
-  and fun_use_aux env rm fdone us f =
-    gen_fun_use env fdone rm us f
-
   let mod_use_top env mp =
     let mp = norm_mpath env mp in
     let me, _ = Mod.by_mpath mp env in

src/ecHiTacticals.ml

@@ -223,9 +223,8 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Peager_if                 -> EcPhlEager.process_if
     | Peager_while info         -> EcPhlEager.process_while info
     | Peager_fun_def            -> EcPhlEager.process_fun_def
-    | Peager_fun_abs infos      -> curry EcPhlEager.process_fun_abs infos
+    | Peager_fun_abs infos      -> EcPhlEager.process_fun_abs infos
     | Peager_call info          -> EcPhlEager.process_call info
-    | Peager infos              -> curry EcPhlEager.process_eager infos
     | Pbd_equiv (nm, f1, f2)    -> EcPhlConseq.process_bd_equiv nm (f1, f2)
     | Pauto                     -> EcPhlAuto.t_auto ~conv:`Conv
     | Plossless                 -> EcPhlHiAuto.t_lossless

src/ecParser.mly

@@ -2847,35 +2847,25 @@ logtactic:
 | WLOG b=boption(SUFF) COLON ids=loc(ipcore_name)* SLASH f=form
    { Pwlog (ids, b, f) }
 
-eager_info:
-| h=ident
-    { LE_done h }
-
-| LPAREN h=ident COLON s1=stmt TILD s2=stmt COLON pr=form LONGARROW po=form RPAREN
-    { LE_todo (h, s1, s2, pr, po) }
-
 eager_tac:
-| SEQ n1=codepos1 n2=codepos1 i=eager_info COLON p=sform
-    { Peager_seq (i, (n1, n2), p) }
+| SEQ n1=codepos1 n2=codepos1 COLON s=stmt COLON p=form_or_double_form
+    { Peager_seq ((n1, n2), s, p) }
 
 | IF
     { Peager_if }
 
-| WHILE i=eager_info
+| WHILE i=sform
     { Peager_while i }
 
 | PROC
     { Peager_fun_def }
 
-| PROC i=eager_info f=sform
-    { Peager_fun_abs (i, f) }
+| PROC f=sform
+    { Peager_fun_abs f }
 
 | CALL info=gpterm(call_info)
     { Peager_call info }
 
-| info=eager_info COLON p=sform
-    { Peager (info, p) }
-
 form_or_double_form:
 | f=sform
     { Single f }

src/ecParsetree.ml

@@ -602,11 +602,6 @@ type trans_formula =
 type trans_info =
   trans_kind * trans_formula
 
-(* -------------------------------------------------------------------- *)
-type eager_info =
-  | LE_done of psymbol
-  | LE_todo of psymbol * pstmt * pstmt * pformula * pformula
-
 (* -------------------------------------------------------------------- *)
 type bdh_split =
   | BDH_split_bop     of pformula * pformula * pformula option
@@ -782,13 +777,12 @@ type phltactic =
 
 
     (* Eager *)
-  | Peager_seq       of (eager_info * pcodepos1 pair * pformula)
+  | Peager_seq       of (pcodepos1 pair * pstmt * pformula doption)
   | Peager_if
-  | Peager_while     of (eager_info)
+  | Peager_while     of pformula
   | Peager_fun_def
-  | Peager_fun_abs   of (eager_info * pformula)
-  | Peager_call      of (call_info gppterm)
-  | Peager           of (eager_info * pformula)
+  | Peager_fun_abs   of pformula
+  | Peager_call      of call_info gppterm
 
     (* Relation between logic *)
   | Pbd_equiv of (side * pformula * pformula)