A taste of logical relations using Dafny

stlc.dfy

datatype ty =
| TBool
| TFun (t1: ty, t2: ty)

type id = nat

datatype tm =
| ttrue
| tfalse
| tvar (n: id)
| tapp (t1: tm, t2: tm)
| tabs (t: tm)

ghost predicate has_type (G: seq<ty>, t: tm, T: ty)
    decreases t {
  match t {
    case ttrue => T == TBool
    case tfalse => T == TBool
    case tvar(n) =>
      n < |G| && G[n] == T
    case tapp(t1, t2) =>
      exists T2 ::
        has_type(G, t1, TFun(T2, T)) &&
        has_type(G, t2, T2)
    case tabs(t) =>
      exists T1, T2 ::
        T == TFun(T1, T2) &&
        has_type(G + [T1], t, T2)
  }
}

datatype vl =
| vbool(bool)
| vabs(seq<vl>, tm) 

datatype res =
| timeout
| stuck
| result(v: vl)

function teval (n: nat, env: seq<vl>, t: tm): res {
  if n == 0 then timeout else match t {
    case ttrue => result(vbool(true))
    case tfalse => result(vbool(false))
    case tvar(x) =>
      if x < |env|
        then result(env[x])
        else stuck
    case tabs(y) => result(vabs(env, y))
    case tapp(ef, ex) => 
      match teval(n-1, env, ef) {
        case timeout => timeout
        case result(vabs(env2, ey)) =>
          match teval(n-1, env, ex) {
            case timeout => timeout
            case stuck => stuck
            case result(vx) => teval(n-1, env2 + [vx], ey)
          }
        case _ => stuck
      }
  }
}

ghost predicate tevalnm(nm: nat, env: seq<vl>, e: tm, v: vl) {
  forall n :: n > nm ==> teval(n, env, e) == result(v)
}

ghost predicate tevaln (env: seq<vl>, e: tm, v: vl) {
  exists nm :: tevalnm(nm, env, e, v)
}

ghost predicate val_type(v: vl, T: ty) decreases T {
  match (v, T) {
    case (vbool(b), TBool) => true
    case (vabs(G, ty), TFun(T1, T2)) =>
      forall H, tx, vx :: tevaln(H, tx, vx) && val_type(vx, T1) ==>
        exists vy :: tevaln(G + [vx], ty, vy) && val_type(vy, T2)
    case (_, _) => false
  }
}

ghost predicate exp_type(H: seq<vl>, t: tm, v: vl, T: ty) {
  tevaln(H, t, v) && val_type(v, T)
}

ghost predicate env_type(H: seq<vl>, G: seq<ty>) {
  |H| == |G| && forall x: nat, T1 ::
    x < |G| && G[x] == T1 ==> exists v :: exp_type(H, tvar(x), v, T1)
}

ghost predicate sem_type(G: seq<ty>, e: tm, T: ty) {
  forall H :: env_type(H, G) ==> exists v :: exp_type(H, e, v, T)
}

lemma envt_extend(H: seq<vl>, G: seq<ty>, v: vl, T: ty)
    requires env_type(H, G)
    requires val_type(v, T)
    ensures env_type(H + [v], G + [T]) {
  var H1 := H + [v];
  var G1 := G + [T];
  forall x: nat, T1 | x < |G1| && G1[x] == T1
      ensures exists v :: exp_type(H1, tvar(x), v, T1) {
    if {
      case x < |G| =>
        forall v | exp_type(H, tvar(x), v, T1)
            ensures exp_type(H1, tvar(x), v, T1) {
          forall n: nat | tevalnm(n, H, tvar(x), v)
              ensures tevalnm(n, H1, tvar(x), v) {
            assert teval(n+1, H, tvar(x)) == result(v);
          }
        }
      case x == |G| =>
        assert tevalnm(0, H1, tvar(x), v);
        assert exp_type(H1, tvar(x), v, T);
    }
  }
}

lemma full_total_safety(e: tm, G: seq<ty>, T: ty)
    requires has_type(G, e, T)
    ensures sem_type(G, e, T) {
  match e {
    case ttrue =>
      forall H | env_type(H, G) ensures exp_type(H, ttrue, vbool(true), TBool) {
        assert tevalnm(0, H, ttrue, vbool(true));
      }
    case tfalse =>
      forall H | env_type(H, G) ensures exp_type(H, tfalse, vbool(false), TBool) {
        assert tevalnm(0, H, tfalse, vbool(false));
      }
    case tvar(_) =>
    case tabs(y) =>
      forall H, T1, T2 | env_type(H, G) && has_type(G, tabs(y), TFun(T1, T2))
          ensures exp_type(H, tabs(y), vabs(H, y), TFun(T1, T2)) {
        assert sem_type(G + [T1], y, T2);
        forall H1, tx, vx | tevaln(H1, tx, vx) && val_type(vx, T1) {
          envt_extend(H, G, vx, T1);
        }
        assert val_type(vabs(H, y), TFun(T1, T2));
        assert tevalnm(0, H, tabs(y), vabs(H, y));
      }
    case tapp(e1, e2) =>
      forall T2 | has_type(G, e1, TFun(T2, T)) && has_type(G, e2, T2)
          ensures sem_type(G, tapp(e1, e2), T) {
        assert sem_type(G, e1, TFun(T2, T));
        forall H, H1, y, v2 | env_type(H, G) && exp_type(H, e1, vabs(H1, y), TFun(T2, T)) && exp_type(H, e2, v2, T2)
            ensures exists v :: exp_type(H, tapp(e1, e2), v, T) {
          forall vy, n: nat, n1: nat, n2: nat
              | tevalnm(n, H1 + [v2], y, vy) && val_type(vy, T) &&
                tevalnm(n1, H, e1, vabs(H1, y)) && tevalnm(n2, H, e2, v2)
              ensures exp_type(H, tapp(e1, e2), vy, T) {
            assert tevalnm(n+n1+n2+1, H, tapp(e1, e2), vy);
          }
        }
      }
  }
}