New lazy/eager logic.

[loutr]

This PR implements a new lazy/eager logic which 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.

It also brings some documentation in the interface file. The corresponding source file has been formatted with ocamlformat (although it is not (yet) the case for other source files in the project).

This new implementation also fixes #771.

[loutr]

I have no idea how that one stuck goal (in the CI) in the examples is related to this PR. The fix is trivial however, and just requires providing the SMT more information.

[strub]

I have no idea how that one stuck goal (in the CI) in the examples is related to this PR. The fix is trivial however, and just requires providing the SMT more information.

This kind of SMT calls are very fragile. Restarting the CI without any change could have fixed it.

[alleystoughton]

The old eager proc had an option enabling the following proof. Is there a way to patch it with your simplification?

require import AllCore List.

module type OR = {
  proc init() : unit
  proc incr_x() : unit
  proc incr_y() : unit
}.

module Or1 : OR = {
  var x, y : int
  proc init() : unit = { x <- 0; y <- 0; }
  proc incr_x() : unit = { x <- x + 1; }
  proc incr_y() : unit = { y <- y + 1; }
}.

module Or2 : OR = {  (* same but with transcript *)
  var x, y : int
  var trace : bool list
  proc init() : unit = { x <- 0; y <- 0; trace <- []; }
  proc incr_x() : unit = { x <- x + 1; trace <- trace ++ [true]; }
  proc incr_y() : unit = { y <- y + 1; trace <- trace ++ [false]; }
}.

(* this works, even though the statement begin swapped goes
   from Or1.incr_x() to Or2.incr_x() *)

lemma eager_incr_x :
  eager[Or1.incr_x(); , Or1.incr_x ~ Or2.incr_x , Or2.incr_x(); :
        ={x, y}(Or1, Or2) ==> ={x, y}(Or1, Or2)].
proof.
eager proc.
inline*; auto.
qed.

(* this works, even though the statement begin swapped goes
   from Or1.incr_x() to Or2.incr_x() *)

lemma eager_incr_y :
  eager[Or1.incr_x(); , Or1.incr_y ~ Or2.incr_y, Or2.incr_x(); :
        ={x, y}(Or1, Or2) ==> ={x, y}(Or1, Or2)].
proof.
eager proc.
inline*; auto.
qed.

module type ADV(O : OR) = {
  proc main() : bool {O.incr_x, O.incr_y}
}.

module G (Adv : ADV) = {
  proc main1() : bool = {
    var b : bool;
    Or1.init();
    Or1.incr_x();
    b <@ Adv(Or1).main();
    return b;
  }

  proc main2() : bool = {
    var b : bool;
    Or2.init();
    b <@ Adv(Or2).main();
    Or2.incr_x();
    return b;
  }
}.

lemma eager_adv (Adv <: ADV{-Or1, -Or2}) :
  eager[Or1.incr_x(); , Adv(Or1).main ~
        Adv(Or2).main, Or2.incr_x(); :
        ={glob Adv} /\ ={x, y}(Or1, Or2) ==> ={res} /\ ={x, y}(Or1, Or2)].
proof.
(* this works with the existing logic

   is there a way to translate this eager proc into the new logic?

   given that the lemmas eager_incr_x and eager_incr_y can be
   proved using eager proc, it seems it should be possible to
   lift them to an abstract procedure *)
eager proc
      (incr :
         Or1.incr_x(); ~ Or2.incr_x(); :
         ={x, y}(Or1, Or2) ==> ={x, y}(Or1, Or2))
      (={x, y}(Or1, Or2)).
sim.
trivial.
trivial.
apply eager_incr_x.
sim.
apply eager_incr_y.
sim.
qed.

lemma G_Adv (Adv <: ADV{-Or1, -Or2}) :
  equiv[G(Adv).main1 ~ G(Adv).main2 :
        ={glob Adv} ==> ={res} /\ ={x, y}(Or1, Or2)].
proof.
proc.
seq 1 1 : (={glob Adv} /\ ={x, y}(Or1, Or2)); first inline*; auto.
eager call (eager_adv Adv); first auto.
qed.

Maybe you are trying to insist that the statements being swapped are identical? But you allowed them to be different except when I moved to an abstract procedure.

[alleystoughton]

One unpleasant workaround for this example, is to have Or2 use the variables of Or1, and prove instead

lemma eager_adv (Adv <: ADV{-Or1}) :
  eager[Or1.incr_x(); , Adv(Or1).main ~
        Adv(Or2).main, Or1.incr_x(); :
        ={glob Adv} /\ ={Or1.x, Or1.y} ==> ={res, Or1.x, Or1.y}].

(so it's Or1.incr_x that is being swapped). Since the tracing is discarded at the end, this works. This is akin to how FRO and RRO are used in PROM, where it's RRO.resample() that is being swapped over FRO -> RRO. But I find the existing flexibility attractive.

[loutr]

The new logic indeed insists on using the same swapping statement on both sides. It's true that the syntax of eager[ ... ] statements hasn't been modified to take that into account, and eager proc will still convert it into the corresponding equiv goal even when the statements are distinct. Maybe this should be modified too.

We made the choice to restrict to a single swapping statement after noticing that it would not cause any problem in the real uses of eager-related tactics. This restriction makes for simpler proofs of the rules and thus less susceptible to being unsound :) I can take some time to find what a straightforward way to prove your statement would look like in this new setup. It's possible that it won't be as convenient. Do you have a more "concrete" example where this flexibility would really be worth keeping? (Given the very-close-to-zero amount of times eager tactics are used)

[alleystoughton]

OK, I see. I'll be sad to see the opportunity to have different swapping statements go away, as I think it's more elegant. Unless I'm missing something, the new logic forces a style where the procedures of the second module use the variables of the first. I personally find this ugly.

My only "real" example is a different proof of part of PROM that I use for pedagogical purposes, in part. In it, I do use the flexibility. I'll see if I can adapt it to the new logic in a not too ugly way.

Clearly, you should also prohibit using different statements in the concrete case (my first 2 lemmas). It was a surprise when I could not lift them to the lemma using the abstract module.

[alleystoughton]

Update: I reworked my "real" usage of eager to use the new logic, and it wasn't too hard or messy, and the user-facing result is unchanged. Given that hardly anyone uses eager directly, I can see the advantage of the TCB being simpler, even if it's (in my opinion) a little more awkward to use.

[fdupress]

@strub As discuss: a ping in exchange for your review. Ping.

[strub]

If everybody is happy with this new tactic, we can go.

[strub]

@loutr Squash your commits first.

[fdupress]

We (@Cameron-Low and I) confirm that this does not break our more exotic use of eager in the Igor dev, so good from our side.

[loutr]

(I forgot to ping anyone but the commits have been squashed, so I believe everything is in order now @strub)

[Cameron-Low]

We (@Cameron-Low and I) confirm that this does not break our more exotic use of eager in the Igor dev, so good from our side.

@loutr, I've just run into something that is causing me issues. Sorry for catching this late.

MWE:

module M = {
  proc f() = {
    var x;
    x <- (fun v => v) 1;
    while (false) {}
    return x;
  }
  proc g() = {
    var x;
    while (false) {}
    x <- (fun v => v) 1;
    return x;
  }
}.

equiv bug: M.f ~ M.g: true ==> ={res}.
proof.
proc.
eager while (true).
(* ERROR
eager: the tail of the right statement is not of the right form:
x <- (fun (v : int) => v) 1; should be
x <- (fun (v : int) => v) 1;
*)

[loutr]

@Cameron-Low I can actually reproduce this issue with the current version of the logic, with the old syntax:

eager while
 (H: x <- (fun (v : int) => v) 1; ~ x <- (fun (v : int) => v) 1; : true ==> true ).

This is because both versions do not perform alpha-conversion when comparing the instructions (i_equal tests physical equality between instructions). I (hopefully) solved this by using EqTest.for_stmt from the ecReduction.ml module.

[loutr]

I don't know why the errors in the examples have not been detected earlier by the CI on this PR. Anyway all should be good now.
@strub @Cameron-Low