Variant records for globals

[strub]

This would allow to refer to the components of a glob by name.

[alleystoughton]

As someone who is trying to machine-generate code involving glob, it would be helpful if the field names were easily predictable. (Of course we can always reverse engineer from the EC code, but...)

[alleystoughton]

Here is an example of thinking of glob in a hierarchical way. Unfortunately, in proof goals, glob is always eagerly expanded out into its components, which in the case of a complex hierarchy would be distracting and take up a lot of screen space. Is there a way to keep glob symbolic longer? I'm thinking/hoping this might be a consequence of moving to records for glob, which is why I'm posing this question on this issue.

require import AllCore.

module N = {
  var x : int
  proc f() : unit = {
    x <- x - 1;
  }
}.

(* we make all the metrics smt_opaque so SMT has to treat them
   as black boxes *)

op [smt_opaque] metric_N (g : glob N) : int = g.

lemma N_f_metric (n : int) :
  hoare [N.f : metric_N (glob N) = n ==> metric_N (glob N) < n].
proof.
rewrite /metric_N; proc; auto; smt().
qed.

module M = {
  var b : bool
  proc f() : unit = {
    if (b) {
      b <- false;
    }
    else {
      N.f();
    }
  }
}.

op glob_M_self (g : glob M) / : bool = g.`1.

op glob_M_to_N (g : glob M) / : glob N = g.`2.

op [smt_opaque] metric_M (g : glob M) : int =
  (if glob_M_self g then 1 else 0) +
  metric_N (glob_M_to_N g).

lemma M_f_metric (n : int) :
  hoare [M.f : metric_M (glob M) = n ==> metric_M (glob M) < n].
proof.
(*
Current goal

Type variables: <none>

n: int
------------------------------------------------------------------------
pre = metric_M (M.b, N.x) = n

    M.f

post = metric_M (M.b, N.x) < n
*)
proc.
if.
rewrite /metric_M; auto => |> /= /#.
exlim (glob M) => g.
call (N_f_metric (metric_N (glob_M_to_N g))).
rewrite /metric_M; auto => |>.
qed.