Moved the (long running) CloudMake test files to their own directory

5 files changed, 2835 insertions, 0 deletions

diff --git a/Test/cloudmake/Answer b/Test/cloudmake/Answer
new file mode 100644
index 00000000..3758853e
--- /dev/null
+++ b/Test/cloudmake/Answer
@@ -0,0 +1,12 @@
+

+-------------------- CloudMake-ParallelBuilds.dfy --------------------

+

+Dafny program verifier finished with 244 verified, 0 errors

+

+-------------------- CloudMake-CachedBuilds.dfy --------------------

+

+Dafny program verifier finished with 104 verified, 0 errors

+

+-------------------- CloudMake-ConsistentBuilds.dfy --------------------

+

+Dafny program verifier finished with 59 verified, 0 errors

diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy
new file mode 100644
index 00000000..f1150809
--- /dev/null
+++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy
@@ -0,0 +1,1321 @@
+// This module proves the correctness of the algorithms.  It leaves a number of things undefined.

+// They are defined in refinement modules below.

+abstract module M0 {

+  /******* State *******/

+  type State

+  function DomSt(st: State): set<Path>

+  function GetSt(p: Path, st: State): Artifact

+    requires p in DomSt(st);

+

+  // cached part of state

+  type HashValue

+  function DomC(st: State): set<HashValue>

+  function Hash(p: Path): HashValue

+  /* Note, in this version of the formalization and proof, we only record which things are in the

+     cache.  The actual cache values can be retrieved from the system state.

+  type Cmd

+  function GetC(h: HashValue, st: State): Cmd

+  */

+  function UpdateC(cmd: string, deps: set<Path>, exps: set<string>, st: State): State

+    ensures

+      var st' := UpdateC(cmd, deps, exps, st);

+      DomSt(st) == DomSt(st') && (forall p :: p in DomSt(st) ==> GetSt(p, st) == GetSt(p, st')) &&

+      // The following is a rather weak property.  It only guarantees that the new things will be

+      // in the cache, and that the cache remains consistent.  It says nothing else about what might

+      // be in the cache or what happened to previous things in the cache.

+      (ConsistentCache(st) ==> ConsistentCache(st')) &&

+      forall e :: e in exps ==> Hash(Loc(cmd, deps, e)) in DomC(st');

+

+

+  predicate ValidState(st: State)

+  {

+    forall p :: p in DomSt(st) ==> WellFounded(p)

+  }

+  predicate WellFounded(p: Path)

+

+  // The specification given for this Union is liberal enough to allow incompatible

+  // states, that is, st and st' are allowed to disagree on some paths.  Any such disagreement

+  // will be resolved in favor of st.  For the purpose of supporting function Combine, we are

+  // only ever interested in combining/unioning compatible states anyhow.

+  function Union(st: State, st': State, useCache: bool): State

+    ensures

+      var result := Union(st, st', useCache);

+      DomSt(result) == DomSt(st) + DomSt(st') &&

+      (forall p :: p in DomSt(result) ==>

+        GetSt(p, result) == GetSt(p, if p in DomSt(st') then st' else st)) &&

+      (useCache ==> DomC(result) == DomC(st) + DomC(st'));

+          

+

+  predicate Compatible(sts: set<State>)

+  {

+    forall st, st' :: st in sts && st' in sts ==>

+      forall p :: p in DomSt(st) && p in DomSt(st') ==> GetSt(p, st) == GetSt(p, st')

+  }

+  lemma CompatibleProperty(stOrig: State, sts: set<State>)

+    requires forall s :: s in sts ==> Extends(stOrig, s);

+    ensures Compatible(sts);

+  {

+    reveal_Extends();

+  }

+

+  function {:opaque} Combine(sts: set<State>, useCache: bool): State

+    requires sts != {};

+  {

+    var st := PickOne(sts);

+    if sts == {st} then

+      st

+    else

+      Union(Combine(sts - {st}, useCache), st, useCache)

+  }

+  function PickOne<T>(s: set<T>): T

+    requires s != {};

+  {

+    var x :| x in s; x

+  }

+

+  lemma Lemma_Combine(sts: set<State>, parent: State, useCache: bool)

+    requires

+      sts != {} &&

+      (forall st :: st in sts ==> ValidState(st) && Extends(parent, st)) &&

+      (useCache ==> forall st :: st in sts ==> ConsistentCache(st));

+    ensures

+      var stCombined := Combine(sts, useCache);

+      ValidState(stCombined) && Extends(parent, stCombined) &&

+      (useCache ==>

+        ConsistentCache(stCombined) &&

+        (forall st :: st in sts ==> DomC(st) <= DomC(stCombined)) &&

+        (forall h :: h in DomC(stCombined) ==> exists st :: st in sts && h in DomC(st)));

+  {

+    reveal_Combine();

+    var st := PickOne(sts);

+    if sts == {st} {

+    } else {

+      var stCombined := Combine(sts, useCache);

+      var smaller := sts - {st};

+      var smallerCombination := Combine(smaller, useCache);

+      assert stCombined == Union(smallerCombination, st, useCache);

+

+      forall p | p !in DomSt(smallerCombination) && p in DomSt(stCombined)

+        ensures GetSt(p, stCombined) == Oracle(p, smallerCombination);

+      {

+        reveal_Extends();

+        OracleProperty(p, parent, smallerCombination);

+      }

+      forall ensures Extends(smallerCombination, stCombined); {

+        reveal_Extends();

+      }

+      Lemma_ExtendsTransitive(parent, smallerCombination, stCombined);

+    }

+  }

+

+  predicate ConsistentCache(stC: State)

+  {

+    forall cmd, deps, e :: Hash(Loc(cmd, deps, e)) in DomC(stC) ==>

+      Loc(cmd, deps, e) in DomSt(stC)

+  }

+  predicate {:opaque} StateCorrespondence(st: State, stC: State)

+  {

+    // This definition, it turns out, is the same as Extends(st, stC)

+    DomSt(st) <= DomSt(stC) &&

+    (forall p :: p in DomSt(st) ==> GetSt(p, stC) == GetSt(p, st)) &&

+    (forall p :: p !in DomSt(st) && p in DomSt(stC) ==> GetSt(p, stC) == Oracle(p, st))

+  }

+

+  /******* Environment *******/

+  type Env

+  predicate ValidEnv(env: Env)

+  function EmptyEnv(): Env

+    ensures ValidEnv(EmptyEnv());

+  function GetEnv(id: Identifier, env: Env): Expression

+    requires ValidEnv(env);

+    ensures Value(GetEnv(id, env));

+  function SetEnv(id: Identifier, expr: Expression, env: Env): Env

+    requires ValidEnv(env) && Value(expr);

+    ensures ValidEnv(SetEnv(id, expr, env));

+

+  /******* Primitive function 'exec' *******/

+  function exec(cmd: string, deps: set<Path>, exps: set<string>, st: State): Tuple<set<Path>, State>

+

+  lemma ExecProperty(cmd: string, deps: set<Path>, exps: set<string>, st: State)

+    requires

+      ValidState(st) &&

+      deps <= DomSt(st) &&

+      Pre(cmd, deps, exps, st);

+    ensures

+      var result := exec(cmd, deps, exps, st);

+      var paths, st' := result.fst, result.snd;

+      ValidState(st') &&

+      Extends(st, st') && ExtendsLimit(cmd, deps, exps, st, st') &&

+      DomC(st) == DomC(st') &&  // no changes to the cache

+      OneToOne(cmd, deps, exps, paths) &&

+      Post(cmd, deps, exps, st');

+

+  predicate Pre(cmd: string, deps: set<Path>, exps: set<string>, st: State)

+  {

+    forall e :: e in exps ==>

+      Loc(cmd, deps, e) in DomSt(st) ==> GetSt(Loc(cmd, deps, e), st) == Oracle(Loc(cmd, deps, e), st)

+  }

+

+  predicate OneToOne(cmd: string, deps: set<Path>, exps: set<string>, paths: set<Path>)

+  {

+    // KRML:  The previous definition only gave a lower bound on the member inclusion in "paths":

+    //    forall e :: e in exps ==> Loc(cmd, deps, e) in paths

+    // but to compare "paths" with what's stored in the cache, we need to know exactly which

+    // elements on in "paths".  So I strengthened the definition of OneToOne as follows:

+    paths == set e | e in exps :: Loc(cmd, deps, e)

+  }

+

+  predicate {:opaque} Post(cmd: string, deps: set<Path>, exps: set<string>, st: State)

+  {

+    forall e :: e in exps ==>

+      Loc(cmd, deps, e) in DomSt(st) && GetSt(Loc(cmd, deps, e), st) == Oracle(Loc(cmd, deps, e), st)

+  }

+

+  predicate ExtendsLimit(cmd: string, deps: set<Path>, exps: set<string>, st: State, st': State)

+  {

+    DomSt(st') == DomSt(st) + set e | e in exps :: Loc(cmd, deps, e)

+  }

+

+  // Oracle is like an oracle, because for a given path and state, it flawlessly predicts the unique artifact

+  // that may live at that path.  This is less magical than it seems, because Loc is injective,

+  // and therefore one can extract a unique (cmd,deps,exp) from p, and it's not so hard to see

+  // how the oracle may "know" the artifact that results from that.

+  function Oracle(p: Path, st: State): Artifact

+

+  // The oracle never changes its mind.  Therefore, if st0 is extended into st1 only by following

+  // what the oracle predicts, then no predictions change.

+  lemma OracleProperty(p: Path, st0: State, st1: State)

+    requires Extends(st0, st1);

+    ensures Oracle(p, st0) == Oracle(p, st1);

+

+  predicate {:opaque} Extends(st: State, st': State)

+  {

+    DomSt(st) <= DomSt(st') &&

+    (forall p :: p in DomSt(st) ==> GetSt(p, st') == GetSt(p, st)) &&

+    (forall p :: p !in DomSt(st) && p in DomSt(st') ==> GetSt(p, st') == Oracle(p, st))

+  }

+

+  lemma Lemma_ExtendsTransitive(st0: State, st1: State, st2: State)

+    requires Extends(st0, st1) && Extends(st1, st2);

+    ensures Extends(st0, st2);

+  {

+    reveal_Extends();

+    forall p { OracleProperty(p, st0, st1); }

+  }

+

+  function execC(cmd: string, deps: set<Path>, exps: set<string>, stC: State): Tuple<set<Path>, State>

+  {

+    if forall e | e in exps :: Hash(Loc(cmd, deps, e)) in DomC(stC) then

+      var paths := set e | e in exps :: Loc(cmd, deps, e);

+      Pair(paths, stC)

+    else

+      var result := exec(cmd, deps, exps, stC);

+      var expr', st' := result.fst, result.snd;

+      var stC' := UpdateC(cmd, deps, exps, st');

+      Pair(expr', stC')

+  }

+

+  /******* Grammar *******/

+  datatype Program = Program(stmts: seq<Statement>)

+

+  datatype Statement = stmtVariable(id: Identifier, expr: Expression) |

+                       stmtReturn(ret: Expression)

+

+  datatype Expression = exprLiteral(lit: Literal) | exprIdentifier(id: Identifier) |

+                        exprIf(cond: Expression, ifTrue: Expression, ifFalse: Expression) |

+                        exprAnd(conj0: Expression, conj1: Expression) |

+                        exprOr(disj0: Expression, disj1: Expression) |

+                        exprInvocation(fun: Expression, args: seq<Expression>) |

+                        exprError(r: Reason)

+

+  datatype Literal = litTrue | litFalse | litUndefined | litNull |

+                     litNumber(num: int) | litString(str: string) |

+                     litPrimitive(prim: Primitive) |

+                     // Q(rustan): How can I check the type of elems?

+                     // Q(rustan): What happens with the sets?

+                     litArrOfPaths(paths: set<Path>) |

+                     litArrOfStrings(strs: set<string>) |

+                     litArray(arr: seq<Expression>)

+

+  datatype Primitive = primCreatePath | primExec

+

+  datatype Reason = rCompatibility | rValidity | rInconsistentCache

+

+  type Path(==)

+  function Loc(cmd: string, deps: set<Path>, exp: string): Path

+

+  type string(==)

+  type Artifact

+  type Identifier

+

+  datatype Tuple<A, B> = Pair(fst: A, snd: B)

+  datatype Triple<A, B, C> = Tri(0: A, 1: B, 2: C)

+

+  /******* Values *******/

+  predicate Value(expr: Expression)

+  {

+    expr.exprLiteral?

+  }

+

+  /******* Semantics *******/

+

+  /******* Function 'build' *******/

+  function build(prog: Program, st: State, useCache: bool): Tuple<Expression, State>

+    requires Legal(prog.stmts);

+  {

+    do(prog.stmts, st, EmptyEnv(), useCache)

+  }

+

+  /******* Function 'do' *******/

+  function do(stmts: seq<Statement>, st: State, env: Env, useCache: bool): Tuple<Expression, State>

+    requires Legal(stmts) && ValidEnv(env);

+  {

+    var stmt := stmts[0];

+    if stmt.stmtVariable? then

+      var result := eval(stmt.expr, st, env, useCache);

+      var expr', st' := result.fst, result.snd;

+      if Value(expr') then

+        var env' := SetEnv(stmt.id, expr', env);

+        if Legal(stmts[1..]) then

+          do(stmts[1..], st', env', useCache)

+        else

+          Pair(expr', st')

+      else

+        Pair(exprError(rValidity), st)

+    // todo(maria): Add the recursive case.

+    else

+      eval(stmt.ret, st, env, useCache)

+  }

+

+  predicate Legal(stmts: seq<Statement>)

+  {

+    |stmts| != 0

+  }

+

+  /******* Function 'eval' *******/

+  function {:opaque} eval(expr: Expression, st: State, env: Env, useCache: bool): Tuple<Expression, State>

+     requires ValidEnv(env);

+     decreases expr;

+  {

+    if Value(expr) then

+      Pair(expr, st)

+    // identifier

+    else if expr.exprIdentifier? then

+      Pair(GetEnv(expr.id, env), st)

+    // if-expression

+    else if expr.exprIf? then

+      var result := eval(expr.cond, st, env, useCache);

+      var cond', st' := result.fst, result.snd;

+      if cond'.exprLiteral? && cond'.lit == litTrue then

+        eval(expr.ifTrue, st', env, useCache)

+      else if cond'.exprLiteral? && cond'.lit == litFalse then

+        eval(expr.ifFalse, st', env, useCache)

+      else

+        Pair(exprError(rValidity), st)  // todo: should this be st' (and same for the error cases below)?

+    // and-expression

+    else if expr.exprAnd? then

+      var result := eval(expr.conj0, st, env, useCache);

+      var conj0', st' := result.fst, result.snd;

+      if conj0'.exprLiteral? && conj0'.lit == litTrue then

+        eval(expr.conj1, st', env, useCache)

+      else if conj0'.exprLiteral? && conj0'.lit == litFalse then

+        Pair(exprLiteral(litFalse), st')

+      else

+        Pair(exprError(rValidity), st)

+    // or-expression

+    else if expr.exprOr? then

+      var result := eval(expr.disj0, st, env, useCache);

+      var disj0', st' := result.fst, result.snd;

+      if disj0'.exprLiteral? && disj0'.lit == litTrue then

+        Pair(exprLiteral(litTrue), st')

+      else if disj0'.exprLiteral? && disj0'.lit == litFalse then

+        eval(expr.disj1, st', env, useCache)

+      else

+        Pair(exprError(rValidity), st)

+    // invocation

+    else if expr.exprInvocation? then

+      var resultFun := eval(expr.fun, st, env, useCache);

+      var fun', st' := resultFun.fst, resultFun.snd;

+      var resultArgs := evalArgs(expr, expr.args, st, env, useCache);

+      var args', sts' := resultArgs.fst, resultArgs.snd;

+      var sts'' := {st'} + sts';

+      if !Compatible(sts'') then

+        Pair(exprError(rCompatibility), st)

+      else

+        var stCombined := Combine(sts'', useCache);

+        // primitive functions

+        if fun'.exprLiteral? && fun'.lit.litPrimitive? then

+          // primitive function 'exec'

+          if fun'.lit.prim.primExec? then

+            if |args'| == Arity(primExec) && ValidArgs(primExec, args', stCombined) then

+              var cmd, deps, exps := args'[0].lit.str, args'[1].lit.paths, args'[2].lit.strs;

+              if !useCache then

+                var ps := exec(cmd, deps, exps, stCombined);

+                Pair(exprLiteral(litArrOfPaths(ps.fst)), ps.snd)

+              else if ConsistentCache(stCombined) then

+                var ps := execC(cmd, deps, exps, stCombined);

+                Pair(exprLiteral(litArrOfPaths(ps.fst)), ps.snd)

+              else

+                Pair(exprError(rValidity), st)

+            else

+              Pair(exprError(rInconsistentCache), st)

+          else

+          // primitive function 'createPath'

+          // todo(maria): Add primitive function 'createPath'.

+            Pair(exprError(rValidity), st)

+        // todo(maria): Add non-primitive invocations.

+        else

+          Pair(exprError(rValidity), st)

+    // error

+    else

+      Pair(exprError(rValidity), st)

+  }

+

+  function evalFunArgs(expr: Expression, st: State, env: Env, useCache: bool): Triple<Expression, seq<Expression>, set<State>>

+    requires expr.exprInvocation? && ValidEnv(env);

+  {

+    var resultFun := eval(expr.fun, st, env, useCache);

+    var fun', st' := resultFun.fst, resultFun.snd;

+    var resultArgs := evalArgs(expr, expr.args, st, env, useCache);

+    var args', sts' := resultArgs.fst, resultArgs.snd;

+    var sts'' := {st'} + sts';

+    Tri(fun', args', sts'')

+  }

+

+  lemma Lemma_EvalFunArgs_TwoState(expr: Expression, st: State, stC: State, env: Env, p: Triple<Expression, seq<Expression>, set<State>>, pC: Triple<Expression, seq<Expression>, set<State>>)

+    requires expr.exprInvocation? && ValidState(st) && ValidState(stC) && ValidEnv(env);

+    requires ConsistentCache(stC);

+    requires StateCorrespondence(st, stC);

+    requires p == evalFunArgs(expr, st, env, false);

+    requires pC == evalFunArgs(expr, stC, env, true);

+    ensures p.0 == pC.0 && p.1 == pC.1;

+    decreases expr, 0;

+  {

+    var fun, funC := eval(expr.fun, st, env, false).fst, eval(expr.fun, stC, env, true).fst;

+    var args, argsC := evalArgs(expr, expr.args, st, env, false).fst, evalArgs(expr, expr.args, stC, env, true).fst;

+

+    assert fun == evalFunArgs(expr, st, env, false).0;

+    assert args == evalFunArgs(expr, st, env, false).1;

+    assert funC == evalFunArgs(expr, stC, env, true).0;

+    assert argsC == evalFunArgs(expr, stC, env, true).1;

+

+    var _, _, _ := Lemma_Eval(expr.fun, st, stC, env);

+    var _, _, _ := Lemma_EvalArgs(expr, expr.args, st, stC, env);

+  }

+

+  lemma Lemma_EvalFunArgs_TwoState_StateCorrespondence(expr: Expression, st: State, stC: State, env: Env, p: Triple<Expression, seq<Expression>, set<State>>, pC: Triple<Expression, seq<Expression>, set<State>>)

+    requires expr.exprInvocation? && ValidState(st) && ValidState(stC) && ValidEnv(env);

+    requires ConsistentCache(stC);

+    requires StateCorrespondence(st, stC);

+    requires p == evalFunArgs(expr, st, env, false);

+    requires pC == evalFunArgs(expr, stC, env, true);

+    ensures StateCorrespondence(Combine(p.2, false), Combine(pC.2, true));

+    decreases expr, 0;

+  {

+    var fun, funC := eval(expr.fun, st, env, false).fst, eval(expr.fun, stC, env, true).fst;

+    var args, argsC := evalArgs(expr, expr.args, st, env, false).fst, evalArgs(expr, expr.args, stC, env, true).fst;

+

+    assert fun == evalFunArgs(expr, st, env, false).0;

+    assert args == evalFunArgs(expr, st, env, false).1;

+    assert funC == evalFunArgs(expr, stC, env, true).0;

+    assert argsC == evalFunArgs(expr, stC, env, true).1;

+

+    var _, stFun, stFunC := Lemma_Eval(expr.fun, st, stC, env);

+    var _, stsArgs, stsArgsC := Lemma_EvalArgs(expr, expr.args, st, stC, env);

+    assert p.2 == {stFun} + stsArgs;

+    assert pC.2 == {stFunC} + stsArgsC;

+    CompatibleProperty(st, p.2);

+    CompatibleProperty(stC, pC.2);

+    StateCorrespondence_Ctor(st, stFun, stsArgs, stFunC, stsArgsC);

+  }

+

+  lemma Lemma_EvalFunArgs(expr: Expression, st: State, env: Env, useCache: bool, sts'': set<State>)

+    requires expr.exprInvocation? && ValidState(st) && ValidEnv(env);

+    requires useCache ==> ConsistentCache(st);

+    requires evalFunArgs(expr, st, env, useCache).2 == sts'';

+    ensures Compatible(sts'');

+    ensures forall s :: s in sts'' ==> ValidState(s) && Extends(st, s) && (useCache ==> ConsistentCache(s));

+  {

+    var resultFun := eval(expr.fun, st, env, useCache);

+    var fun', st' := resultFun.fst, resultFun.snd;

+    var resultArgs := evalArgs(expr, expr.args, st, env, useCache);

+    var args', sts' := resultArgs.fst, resultArgs.snd;

+    assert sts'' == {st'} + sts';

+

+    forall

+      ensures ValidState(st') && Extends(st, st');

+      ensures useCache ==> ConsistentCache(st');

+    {

+      var _, _ := EvalLemma(expr.fun, st, env, useCache);

+    }

+    forall s | s in sts'

+      ensures ValidState(s) && Extends(st, s);

+      ensures useCache ==> ConsistentCache(s);

+    {

+      var _, _ := EvalArgsLemma(expr, expr.args, st, env, useCache);

+    }

+    assert forall s :: s in sts'' ==> s == st' || s in sts';

+    assert forall s :: s in sts'' ==> Extends(st, s);

+    CompatibleProperty(st, sts'');

+  }

+

+  lemma Equiv_SuperCore(expr: Expression, st: State, env: Env, useCache: bool)

+    requires expr.exprInvocation? && ValidEnv(env);

+    ensures eval(expr, st, env, useCache) == evalSuperCore(expr, st, env, useCache);

+  {

+    reveal_eval();

+  }

+

+  function evalSuperCore(expr: Expression, st: State, env: Env, useCache: bool): Tuple<Expression, State>

+    requires expr.exprInvocation? && ValidEnv(env);

+  {

+    var tri := evalFunArgs(expr, st, env, useCache);

+    var fun', args', sts'' := tri.0, tri.1, tri.2;

+    evalCompatCheckCore(st, sts'', fun', args', useCache)

+  }

+

+  function evalCompatCheckCore(stOrig: State, sts: set<State>, fun: Expression, args: seq<Expression>, useCache: bool): Tuple<Expression, State>

+    requires sts != {};

+  {

+    if !Compatible(sts) then

+      Pair(exprError(rCompatibility), stOrig)

+    else

+      var stCombined := Combine(sts, useCache);

+      if fun.exprLiteral? && fun.lit.litPrimitive? then

+        if fun.lit.prim.primExec? then

+          evalCore(stOrig, stCombined, args, useCache)

+        else

+          Pair(exprError(rValidity), stOrig)

+      else

+        Pair(exprError(rValidity), stOrig)

+  }

+

+  function evalCore(stOrig: State, stCombined: State, args: seq<Expression>, useCache: bool): Tuple<Expression, State>

+  {

+    if |args| == Arity(primExec) && ValidArgs(primExec, args, stCombined) then

+      var cmd, deps, exps := args[0].lit.str, args[1].lit.paths, args[2].lit.strs;

+      if !useCache then

+        var ps := exec(cmd, deps, exps, stCombined);

+        Pair(exprLiteral(litArrOfPaths(ps.fst)), ps.snd)

+      else if ConsistentCache(stCombined) then

+        var ps := execC(cmd, deps, exps, stCombined);

+        Pair(exprLiteral(litArrOfPaths(ps.fst)), ps.snd)

+      else

+        Pair(exprError(rValidity), stOrig)

+    else

+      Pair(exprError(rInconsistentCache), stOrig)

+  }

+

+  function evalArgs(context: Expression, args: seq<Expression>, stOrig: State, env: Env, useCache: bool):

+           Tuple<seq<Expression>, set<State>>

+    requires

+      ValidEnv(env) &&

+      forall arg :: arg in args ==> arg < context;

+    decreases context, |args|;

+  {

+    if args == [] then

+      Pair([], {})

+    else

+      var r := eval(args[0], stOrig, env, useCache);

+      var rr := evalArgs(context, args[1..], stOrig, env, useCache);

+      Pair([r.fst] + rr.fst, {r.snd} + rr.snd)

+  }

+

+  function Arity(prim: Primitive): nat

+  {

+    match prim

+    case primCreatePath => 1

+    case primExec => 3

+  }

+

+  predicate ValidArgs(prim: Primitive, args: seq<Expression>, st: State)

+    requires prim.primExec? ==> |args| == 3;

+    requires prim.primCreatePath? ==> |args| == 1;

+  {

+    match prim

+    case primCreatePath => false

+    case primExec =>

+      var cmd, deps, exps := args[0], args[1], args[2];

+      cmd.exprLiteral? && cmd.lit.litString? &&

+      deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+      exps.exprLiteral? && exps.lit.litArrOfStrings? &&

+      deps.lit.paths <= DomSt(st) &&

+      Pre(cmd.lit.str, deps.lit.paths, exps.lit.strs, st)

+  }

+

+  /******* Parallel builds are race-free *******/

+  lemma ParallelBuildsTheorem(prog: Program, st: State, useCache: bool)

+    requires Legal(prog.stmts) && ValidState(st);

+    requires useCache ==> ConsistentCache(st);

+    ensures

+      var result := build(prog, st, useCache);

+      var expr', st' := result.fst, result.snd;

+      ValidState(st') &&

+      (expr'.exprError? ==> expr'.r != rCompatibility);

+  {

+    BuildLemma(prog, st, useCache);

+  }

+

+  lemma BuildLemma(prog: Program, st: State, useCache: bool)

+    requires Legal(prog.stmts) && ValidState(st);

+    requires useCache ==> ConsistentCache(st);

+    ensures

+      var result := build(prog, st, useCache);

+      var expr', st' := result.fst, result.snd;

+      ValidState(st') &&

+      Extends(st, st') &&

+      (expr'.exprError? ==> expr'.r != rCompatibility);

+  {

+    DoLemma(prog.stmts, st, EmptyEnv(), useCache);

+  }

+

+  lemma DoLemma(stmts: seq<Statement>, st: State, env: Env, useCache: bool)

+    requires Legal(stmts) && ValidState(st) && ValidEnv(env);

+    requires useCache ==> ConsistentCache(st);

+    ensures

+      var result := do(stmts, st, env, useCache);

+      var expr', st' := result.fst, result.snd;

+      ValidState(st') &&

+      Extends(st, st') &&

+      (useCache ==> ConsistentCache(st)) &&

+      (expr'.exprError? ==> expr'.r != rCompatibility);

+  {

+    var stmt := stmts[0];

+    if stmt.stmtVariable? {

+      var expr', st' := EvalLemma(stmt.expr, st, env, useCache);

+      if Value(expr') {

+        var env' := SetEnv(stmt.id, expr', env);

+        if Legal(stmts[1..]) {

+          DoLemma(stmts[1..], st', env', useCache);

+          var st'' := do(stmts[1..], st', env', useCache).snd;

+          Lemma_ExtendsTransitive(st, st', st'');

+        } else { 

+        }

+      } else {

+        reveal_Extends();

+      }

+    } else {

+      assert stmt.stmtVariable? || stmt.stmtReturn?;

+      var _, _ := EvalLemma(stmt.ret, st, env, useCache);

+    }

+  }

+

+  lemma LittleEvalLemma(expr: Expression, st: State, env: Env, useCache: bool, outExpr: Expression, outSt: State)

+    requires ValidState(st) && ValidEnv(env);

+    requires useCache ==> ConsistentCache(st);

+    requires eval(expr, st, env, useCache) == Pair(outExpr, outSt);

+    ensures

+      ValidState(outSt) &&

+      Extends(st, outSt) &&

+      (useCache ==> ConsistentCache(outSt)) &&

+      (outExpr.exprError? ==> outExpr.r != rCompatibility);

+  {

+    var _, _ := EvalLemma(expr, st, env, useCache);

+  }

+

+  lemma {:induction false} {:timeLimit 30} EvalLemma(expr: Expression, st: State, env: Env, useCache: bool) returns (outExpr: Expression, outSt: State)

+    requires ValidState(st) && ValidEnv(env);

+    requires useCache ==> ConsistentCache(st);

+    ensures

+      eval(expr, st, env, useCache) == Pair(outExpr, outSt) &&

+      ValidState(outSt) &&

+      Extends(st, outSt) &&

+      (useCache ==> ConsistentCache(outSt)) &&

+      (outExpr.exprError? ==> outExpr.r != rCompatibility);

+    decreases expr;

+  {

+    var result := eval(expr, st, env, useCache);

+    outExpr, outSt := result.fst, result.snd;

+    if Value(expr) {

+      reveal_eval();  reveal_Extends();

+    } else if expr.exprIdentifier? {

+      reveal_eval();  reveal_Extends();

+    } else if expr.exprIf? {

+      reveal_eval();

+      var cond', st' := EvalLemma(expr.cond, st, env, useCache);

+      if cond'.exprLiteral? && cond'.lit == litTrue {

+        var _, st'' := EvalLemma(expr.ifTrue, st', env, useCache);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else if cond'.exprLiteral? && cond'.lit == litFalse {

+        var _, st'' := EvalLemma(expr.ifFalse, st', env, useCache);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else {

+        reveal_Extends();

+      }

+    } else if expr.exprAnd? {

+      reveal_eval();

+      var conj0', st' := EvalLemma(expr.conj0, st, env, useCache);

+      if conj0'.exprLiteral? && conj0'.lit == litTrue {

+        var _, st'' := EvalLemma(expr.conj1, st', env, useCache);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else if conj0'.exprLiteral? && conj0'.lit == litFalse {

+      } else {

+        reveal_Extends();

+      }

+    } else if expr.exprOr? {

+      reveal_eval();

+      var disj0', st' := EvalLemma(expr.disj0, st, env, useCache);

+      if disj0'.exprLiteral? && disj0'.lit == litTrue {

+      } else if disj0'.exprLiteral? && disj0'.lit == litFalse {

+        var _, st'' := EvalLemma(expr.disj1, st', env, useCache);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else {

+        reveal_Extends();

+      }

+    } else if expr.exprInvocation? {

+      reveal_eval();

+      reveal_Extends();

+      var fun', st' := EvalLemma(expr.fun, st, env, useCache);

+      var args', sts' := EvalArgsLemma(expr, expr.args, st, env, useCache);

+      var sts'' := {st'} + sts';

+      CompatibleProperty(st, sts'');

+      if Compatible(sts'') {

+        var stCombined := Combine(sts'', useCache);

+        Lemma_Combine(sts'', st, useCache);

+        if fun'.exprLiteral? && fun'.lit.litPrimitive? {

+          if fun'.lit.prim.primExec? {

+            if |args'| == Arity(primExec) && ValidArgs(primExec, args', stCombined) {

+              var cmd, deps, exps := args'[0].lit.str, args'[1].lit.paths, args'[2].lit.strs;

+              if !useCache {

+                ExecProperty(cmd, deps, exps, stCombined);

+                var ps := exec(cmd, deps, exps, stCombined);

+                Lemma_ExtendsTransitive(st, stCombined, ps.snd);

+              } else if ConsistentCache(stCombined) {

+                var ps := execC(cmd, deps, exps, stCombined);

+                if forall e | e in exps :: Hash(Loc(cmd, deps, e)) in DomC(stCombined) {

+                } else {

+                  ExecProperty(cmd, deps, exps, stCombined);

+                  var result := exec(cmd, deps, exps, stCombined);

+                  var expr', st' := result.fst, result.snd;

+                  Lemma_ExtendsTransitive(st, stCombined, st');

+                  var stC' := UpdateC(cmd, deps, exps, st');

+                  assert outExpr == exprLiteral(litArrOfPaths(expr')) && outSt == stC';

+                  assert useCache ==> ConsistentCache(outSt);  // apparently needed as lemma, if Extends is opaque

+                }

+              } else { }

+            } else { }

+          } else { }

+        } else { }

+      } else { }

+    } else {

+      reveal_eval();

+      reveal_Extends();

+    }

+  }

+

+  lemma EvalArgsLemma(context: Expression, args: seq<Expression>, stOrig: State, env: Env, useCache: bool)

+             returns (exprs: seq<Expression>, sts: set<State>)

+    requires

+      ValidState(stOrig) && ValidEnv(env) &&

+      (useCache ==> ConsistentCache(stOrig)) &&

+      forall arg :: arg in args ==> arg < context;

+    ensures

+      evalArgs(context, args, stOrig, env, useCache) == Pair(exprs, sts) &&

+      forall st' :: st' in sts ==>

+        ValidState(st') && Extends(stOrig, st') &&

+        (useCache ==> ConsistentCache(st'));

+    decreases context, |args|;

+  {

+    if args == [] {

+      exprs, sts := [], {};

+    } else {

+      var a, st := EvalLemma(args[0], stOrig, env, useCache);

+      exprs, sts := EvalArgsLemma(context, args[1..], stOrig, env, useCache);

+      exprs, sts := [a] + exprs, {st} + sts;

+    }

+  }

+

+  /******* Cached builds are equivalent to clean builds *******/

+  lemma CachedBuildsTheorem(prog: Program, st: State, stC: State)

+    requires

+      Legal(prog.stmts) &&

+      ValidState(st) &&

+      ValidState(stC) && ConsistentCache(stC) &&

+      StateCorrespondence(st, stC);

+    ensures

+      var Pair(_, st'), Pair(_, stC') := build(prog, st, false), build(prog, stC, true);

+      StateCorrespondence(st', stC');

+  {

+    var _, _ := Lemma_Do(prog.stmts, st, stC, EmptyEnv());

+  }

+

+  lemma Lemma_Do(stmts: seq<Statement>, st: State, stC: State, env: Env) returns (st': State, stC': State)

+    requires

+      Legal(stmts) && ValidEnv(env) &&

+      ValidState(st) &&

+      ValidState(stC) && ConsistentCache(stC) &&

+      StateCorrespondence(st, stC);

+    ensures

+      st' == do(stmts, st, env, false).snd &&

+      stC' == do(stmts, stC, env, true).snd &&

+      StateCorrespondence(st', stC');

+  {

+    var result, resultC := do(stmts, st, env, false), do(stmts, stC, env, true);

+    st', stC' := result.snd, resultC.snd;

+    var stmt := stmts[0];

+    if stmt.stmtVariable? {

+      var expr', st', stC' := Lemma_Eval(stmt.expr, st, stC, env);

+      if Value(expr') {

+        var env' := SetEnv(stmt.id, expr', env);

+        if Legal(stmts[1..]) {

+          var _, _ := Lemma_Do(stmts[1..], st', stC', env');

+        } else { }

+      } else { }

+    } else {

+      var _, _, _ := Lemma_Eval(stmt.ret, st, stC, env);

+    }

+  }

+

+  lemma Lemma_Eval(expr: Expression, st: State, stC: State, env: Env) returns (outExpr: Expression, outSt: State, outStC: State)

+    requires

+      ValidState(st) && ValidEnv(env) &&

+      ValidState(stC) && ConsistentCache(stC) &&

+      StateCorrespondence(st, stC);

+    ensures

+      Pair(outExpr, outSt) == eval(expr, st, env, false) &&

+      Pair(outExpr, outStC) == eval(expr, stC, env, true) &&

+      ValidState(outSt) && Extends(st, outSt) &&

+      ValidState(outStC) && Extends(stC, outStC) && ConsistentCache(outStC) &&

+      StateCorrespondence(outSt, outStC);

+    decreases expr;

+  {

+    var result, resultC := eval(expr, st, env, false), eval(expr, stC, env, true);

+    outExpr, outSt, outStC := result.fst, result.snd, resultC.snd;

+    if Value(expr) {

+      reveal_eval();

+      reveal_Extends();

+    } else if expr.exprIdentifier? {

+      reveal_eval();

+      reveal_Extends();

+    } else if expr.exprIf? {

+      reveal_eval();

+      var cond', st', stC' := Lemma_Eval(expr.cond, st, stC, env);

+      if cond'.exprLiteral? && cond'.lit == litTrue {

+        var _, st'', stC'' := Lemma_Eval(expr.ifTrue, st', stC', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+        Lemma_ExtendsTransitive(stC, stC', stC'');

+      } else if cond'.exprLiteral? && cond'.lit == litFalse {

+        var _, st'', stC'' := Lemma_Eval(expr.ifFalse, st', stC', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+        Lemma_ExtendsTransitive(stC, stC', stC'');

+      } else {

+        reveal_Extends();

+      }

+    } else if expr.exprAnd? {

+      reveal_eval();

+      var conj0', st', stC' := Lemma_Eval(expr.conj0, st, stC, env);

+      if conj0'.exprLiteral? && conj0'.lit == litTrue {

+        var _, st'', stC'' := Lemma_Eval(expr.conj1, st', stC', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+        Lemma_ExtendsTransitive(stC, stC', stC'');

+      } else if conj0'.exprLiteral? && conj0'.lit == litFalse {

+      } else {

+        reveal_Extends();

+      }

+    } else if expr.exprOr? {

+      reveal_eval();

+      var disj0', st', stC' := Lemma_Eval(expr.disj0, st, stC, env);

+      if disj0'.exprLiteral? && disj0'.lit == litTrue {

+      } else if disj0'.exprLiteral? && disj0'.lit == litFalse {

+        var _, st'', stC'' := Lemma_Eval(expr.disj1, st', stC', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+        Lemma_ExtendsTransitive(stC, stC', stC'');

+      } else {

+        reveal_Extends();

+      }

+    } else if expr.exprInvocation? {

+      outExpr, outSt, outStC := Lemma_Eval_Invocation(expr, st, stC, env);

+      LittleEvalLemma(expr, st, env, false, outExpr, outSt);

+      LittleEvalLemma(expr, stC, env, true, outExpr, outStC);

+    } else {

+      reveal_eval();

+      reveal_Extends();

+    }

+  }

+

+  lemma {:induction false} Lemma_Eval_Invocation(expr: Expression, st: State, stC: State, env: Env) returns (outExpr: Expression, outSt: State, outStC: State)

+    requires

+      expr.exprInvocation? &&

+      ValidState(st) && ValidEnv(env) &&

+      ValidState(stC) && ConsistentCache(stC) &&

+      StateCorrespondence(st, stC);

+    ensures

+      Pair(outExpr, outSt) == eval(expr, st, env, false) &&

+      Pair(outExpr, outStC) == eval(expr, stC, env, true) &&

+      StateCorrespondence(outSt, outStC);

+    decreases expr, 1;

+  {

+    var tri := evalFunArgs(expr, st, env, false);

+    var fun', args', sts'' := tri.0, tri.1, tri.2;

+    var p := evalCompatCheckCore(st, sts'', fun', args', false);

+

+    var triC := evalFunArgs(expr, stC, env, true);

+    var funC', argsC', stsC'' := triC.0, triC.1, triC.2;

+    var pC := evalCompatCheckCore(stC, stsC'', funC', argsC', true);

+

+    outExpr, outSt, outStC := p.fst, p.snd, pC.snd;

+    var outExprC := pC.fst;

+

+    Equiv_SuperCore(expr, st, env, false);

+    Equiv_SuperCore(expr, stC, env, true);

+    assert Pair(outExpr, outSt) == eval(expr, st, env, false);

+    assert Pair(outExprC, outStC) == eval(expr, stC, env, true);

+

+    Lemma_EvalFunArgs(expr, st, env, false, sts'');

+    assert Compatible(sts'');

+    Lemma_EvalFunArgs(expr, stC, env, true, stsC'');

+    assert Compatible(stsC'');

+

+    Lemma_EvalFunArgs_TwoState(expr, st, stC, env, tri, triC);

+    Lemma_EvalFunArgs_TwoState_StateCorrespondence(expr, st, stC, env, tri, triC);

+    Continuation(p, st, sts'', pC, stC, stsC'', fun', args');

+

+    CompatCheckCore_StateCorrespondence(st, sts'', stC, stsC'', funC', argsC');

+  }

+

+  lemma CompatCheckCore_StateCorrespondence(stOrig: State, sts: set<State>, stOrigC: State, stsC: set<State>, fun: Expression, args: seq<Expression>)

+    requires ValidState(stOrig) && ValidState(stOrigC);

+    requires StateCorrespondence(stOrig, stOrigC);

+    requires sts != {} && stsC != {};

+    requires Compatible(sts) && Compatible(stsC);

+    requires forall s :: s in sts ==> ValidState(s) && Extends(stOrig, s);

+    requires forall s :: s in stsC ==> ValidState(s) && Extends(stOrigC, s) && ConsistentCache(s);

+    requires StateCorrespondence(Combine(sts, false), Combine(stsC, true));

+    ensures StateCorrespondence(evalCompatCheckCore(stOrig, sts, fun, args, false).snd, evalCompatCheckCore(stOrigC, stsC, fun, args, true).snd);

+  {

+    var p, pC := evalCompatCheckCore(stOrig, sts, fun, args, false), evalCompatCheckCore(stOrigC, stsC, fun, args, true);

+    var stCombined := Combine(sts, false);

+    Lemma_Combine(sts, stOrig, false);

+    var stCombinedC := Combine(stsC, true);

+    Lemma_Combine(stsC, stOrigC, true);

+    if fun.exprLiteral? && fun.lit.litPrimitive? && fun.lit.prim.primExec? {

+      assert p.snd == evalCore(stOrig, stCombined, args, false).snd;

+      assert pC.snd == evalCore(stOrigC, stCombinedC, args, true).snd;

+

+      EvalCoreDeepen(p, stOrig, stCombined, pC, stOrigC, stCombinedC, fun, args);

+

+      assert StateCorrespondence(p.snd, pC.snd);

+    } else {

+    }

+  }

+

+  lemma Continuation(p: Tuple<Expression, State>, st: State, sts'': set<State>,

+                     pC: Tuple<Expression, State>, stC: State, stsC'': set<State>,

+                     fun: Expression, args: seq<Expression>)

+    requires sts'' != {} && Compatible(sts'');

+    requires stsC'' != {} && Compatible(stsC'');

+    requires p == evalCompatCheckCore(st, sts'', fun, args, false);

+    requires pC == evalCompatCheckCore(stC, stsC'', fun, args, true);

+    requires forall s :: s in sts'' ==> ValidState(s) && Extends(st, s);

+    requires forall s :: s in stsC'' ==> ValidState(s) && Extends(stC, s) && ConsistentCache(s);

+    requires StateCorrespondence(st, stC);

+    requires StateCorrespondence(Combine(sts'', false), Combine(stsC'', true));

+    ensures p.fst == pC.fst;

+  {

+    var outExpr, outExprC := p.fst, pC.fst;

+    var stCombined := Combine(sts'', false);

+    Lemma_Combine(sts'', st, false);

+    var stCombinedC := Combine(stsC'', true);

+    Lemma_Combine(stsC'', stC, true);

+    assert ConsistentCache(stCombinedC);

+    assert StateCorrespondence(stCombined, stCombinedC);

+

+    assert p ==

+      if fun.exprLiteral? && fun.lit.litPrimitive? then

+        if fun.lit.prim.primExec? then

+          evalCore(st, stCombined, args, false)

+        else

+          Pair(exprError(rValidity), st)

+      else

+        Pair(exprError(rValidity), st);

+    assert pC ==

+      if fun.exprLiteral? && fun.lit.litPrimitive? then

+        if fun.lit.prim.primExec? then

+          evalCore(stC, stCombinedC, args, true)

+        else

+          Pair(exprError(rValidity), stC)

+      else

+        Pair(exprError(rValidity), stC);

+

+    if fun.exprLiteral? && fun.lit.litPrimitive? && fun.lit.prim.primExec? {

+      assert p == evalCore(st, stCombined, args, false);

+      assert pC == evalCore(stC, stCombinedC, args, true);

+      EvalCoreDeepen(p, st, stCombined, pC, stC, stCombinedC, fun, args);

+    } else {

+      // trivial

+    }

+  }

+

+  lemma EvalCoreDeepen(p: Tuple<Expression, State>, st: State, stCombined: State,

+                       pC: Tuple<Expression, State>, stC: State, stCombinedC: State,

+                       fun: Expression, args: seq<Expression>)

+    requires p == evalCore(st, stCombined, args, false);

+    requires pC == evalCore(stC, stCombinedC, args, true);

+    requires ValidState(stCombined) && ValidState(stCombinedC);

+    requires ConsistentCache(stCombinedC);

+    requires StateCorrespondence(st, stC) && StateCorrespondence(stCombined, stCombinedC);

+    ensures p.fst == pC.fst;

+    ensures StateCorrespondence(p.snd, pC.snd);

+  {

+    assume |args| == Arity(primExec) ==>

+      ValidArgs(primExec, args, stCombined) == ValidArgs(primExec, args, stCombinedC);  // TODO:  This will require some work!

+

+    if |args| == Arity(primExec) && ValidArgs(primExec, args, stCombined) {

+      var cmd, deps, exts := args[0].lit.str, args[1].lit.paths, args[2].lit.strs;

+      var ps := exec(cmd, deps, exts, stCombined);

+      var psC := execC(cmd, deps, exts, stCombinedC);

+      assert p == Pair(exprLiteral(litArrOfPaths(ps.fst)), ps.snd);

+      assert pC == Pair(exprLiteral(litArrOfPaths(psC.fst)), psC.snd);

+

+      reveal_Extends();

+      reveal_StateCorrespondence();

+      ExecProperty(cmd, deps, exts, stCombined);

+      assert Extends(stCombined, ps.snd);

+      assert ExtendsLimit(cmd, deps, exts, stCombined, ps.snd);

+      var newPaths := set e | e in exts :: Loc(cmd, deps, e);

+      assert DomSt(p.snd) == DomSt(stCombined) + newPaths;

+      if forall e | e in exts :: Hash(Loc(cmd, deps, e)) in DomC(stCombinedC) {

+        var paths := set e | e in exts :: Loc(cmd, deps, e);

+        assert psC.fst == paths;

+        assert psC == Pair(paths, stCombinedC);

+        assert ps.fst == psC.fst;

+        assert psC.snd == stCombinedC;

+

+        assert StateCorrespondence(stCombined, stCombinedC);

+        assert DomSt(stCombined) <= DomSt(stCombinedC);  // follows from the previous line

+        assert newPaths <= DomSt(stCombinedC);

+        assert DomSt(p.snd) <= DomSt(pC.snd);

+        forall pth | pth in DomSt(p.snd)

+          ensures GetSt(pth, p.snd) == GetSt(pth, stCombinedC);

+        {

+          if pth in DomSt(stCombined) {

+            // follows from StateCorrespondence(stCombined, stCombinedC)

+          } else {

+            assert pth in newPaths;

+            assert exists e :: e in exts && pth == Loc(cmd, deps, e);

+            var e :| e in exts && pth == Loc(cmd, deps, e);

+            assert Post(cmd, deps, exts, p.snd);

+            reveal_Post();

+            assert GetSt(pth, p.snd) == Oracle(pth, p.snd);

+          }

+        }

+        Lemma_Extends_StateCorrespondence(stCombined, p.snd, stCombinedC);

+        assert StateCorrespondence(ps.snd, stCombinedC);

+      } else {

+        var result := exec(cmd, deps, exts, stCombinedC);

+        var expr', st' := result.fst, result.snd;

+        var stC' := UpdateC(cmd, deps, exts, st');

+        assert psC == Pair(expr', stC');

+        assert psC.fst == expr' == result.fst;

+        ExecProperty(cmd, deps, exts, stCombinedC);

+        assert psC.fst == ps.fst;

+

+        assert Extends(stCombined, ps.snd) && Extends(stCombinedC, stC');

+        assert DomSt(ps.snd) <= DomSt(st') == DomSt(stC');

+        forall pth | pth in DomSt(ps.snd)

+          ensures GetSt(pth, ps.snd) == GetSt(pth, st');

+        {

+          if pth in DomSt(stCombined) {

+          } else {

+            assert pth in newPaths;

+            assert exists e :: e in exts && pth == Loc(cmd, deps, e);

+            var e :| e in exts && pth == Loc(cmd, deps, e);

+            assert Post(cmd, deps, exts, p.snd);

+            reveal_Post();

+            calc {

+              GetSt(pth, p.snd);

+              // by Post

+              Oracle(pth, p.snd);

+              { OracleProperty(pth, stCombined, p.snd); }

+              Oracle(pth, stCombined);

+              { OracleProperty(pth, stCombined, stCombinedC); }

+              Oracle(pth, stCombinedC);

+              { OracleProperty(pth, stCombinedC, st'); }

+              Oracle(pth, st');

+              // by Post

+              GetSt(pth, st');

+            }

+          }

+        }

+        forall pth | pth !in DomSt(p.snd) && pth in DomSt(st')

+          ensures GetSt(pth, st') == Oracle(pth, p.snd);

+        {

+          assert pth !in DomSt(stCombined);

+          if pth in DomSt(stCombinedC) {

+            calc {

+              GetSt(pth, st');

+              GetSt(pth, stCombinedC);

+              Oracle(pth, stCombined);

+              { OracleProperty(pth, stCombined, p.snd); }

+              Oracle(pth, p.snd);

+            }

+          } else {

+            assert GetSt(pth, st') == Oracle(pth, stCombinedC);

+          }

+        }

+        assert StateCorrespondence(p.snd, st');

+        assert StateCorrespondence(ps.snd, psC.snd);

+      }

+

+      assert ps.fst == psC.fst;  // this is the quintescensce of what needs to be proved

+      assert StateCorrespondence(ps.snd, psC.snd);

+    } else {

+      assert p == Pair(exprError(rInconsistentCache), st);

+      assert pC == Pair(exprError(rInconsistentCache), stC);

+    }

+  }

+

+  lemma Lemma_Extends_StateCorrespondence(st: State, st': State, stC: State)

+    requires Extends(st, st') && StateCorrespondence(st, stC) && DomSt(st') <= DomSt(stC);

+    ensures StateCorrespondence(st', stC);

+  {

+    reveal_Extends();

+    reveal_StateCorrespondence();

+    forall p | p !in DomSt(st') && p in DomSt(stC)

+      ensures GetSt(p, stC) == Oracle(p, st');

+    {

+      OracleProperty(p, st, st');

+    }

+  }

+

+

+

+  lemma Lemma_EvalArgs(context: Expression, args: seq<Expression>, stOrig: State, stOrigC: State, env: Env)

+              returns (exprs: seq<Expression>, sts: set<State>, stsC: set<State>)

+    requires

+      ValidState(stOrig) && ValidEnv(env) &&

+      ValidState(stOrigC) && ConsistentCache(stOrigC) &&

+      StateCorrespondence(stOrig, stOrigC) &&

+      forall arg :: arg in args ==> arg < context;

+    decreases context, 0, |args|;

+    ensures

+      Pair(exprs, sts) == evalArgs(context, args, stOrig, env, false) &&

+      Pair(exprs, stsC) == evalArgs(context, args, stOrigC, env, true) &&

+      (forall s :: s in sts ==> ValidState(s) && Extends(stOrig, s)) &&

+      (forall sC :: sC in stsC ==> ValidState(sC) && Extends(stOrigC, sC) && ConsistentCache(sC)) &&

+      (args == [] ==> sts == stsC == {}) &&

+      (args != [] ==> sts != {} && stsC != {} && StateCorrespondence(Combine(sts, false), Combine(stsC, true)));

+  {

+    if args == [] {

+      exprs, sts, stsC := [], {}, {};

+    } else {

+      var a, st, stC := Lemma_Eval(args[0], stOrig, stOrigC, env);

+      exprs, sts, stsC := Lemma_EvalArgs(context, args[1..], stOrig, stOrigC, env);

+      CompatibleProperty(stOrig, {st} + sts);

+      CompatibleProperty(stOrigC, {stC} + stsC);

+      StateCorrespondence_Ctor(stOrig, st, sts, stC, stsC);

+      exprs, sts, stsC := [a] + exprs, {st} + sts, {stC} + stsC;

+    }

+  }

+

+  function DomSt_Union(sts: set<State>): set<Path>

+  {

+    if sts == {} then {} else

+    var st := PickOne(sts); DomSt(st) + DomSt_Union(sts - {st})

+  }

+  lemma Combine_DomSt_X(sts: set<State>, useCache: bool)

+    requires sts != {};

+    ensures DomSt(Combine(sts, useCache)) == DomSt_Union(sts);

+  {

+    reveal_Combine();

+  }

+  lemma DomSt_Union_Cons(st: State, sts: set<State>)

+    ensures DomSt_Union({st} + sts) == DomSt(st) + DomSt_Union(sts);

+  {

+    var big := {st} + sts;

+    if st in sts {

+      assert forall states :: st in states ==> DomSt(st) <= DomSt_Union(states);

+      assert {st} + sts == sts;

+    } else {

+      var stPick := PickOne(big);

+      if st == stPick {

+        assert big - {stPick} == sts;

+      } else {

+        calc {

+          DomSt_Union(big);

+          { assert big - {stPick} == {st} + (sts - {stPick}); }

+          DomSt(stPick) + DomSt_Union({st} + (sts - {stPick}));

+          { DomSt_Union_Cons(st, sts - {stPick}); }

+          DomSt(stPick) + DomSt(st) + DomSt_Union(sts - {stPick});

+          DomSt(st) + DomSt(stPick) + DomSt_Union(sts - {stPick});

+          { DomSt_Union_Cons(stPick, sts - {stPick}); }

+          DomSt(st) + DomSt_Union({stPick} + (sts - {stPick}));

+          { assert {stPick} + (sts - {stPick}) == sts; }

+          DomSt(st) + DomSt_Union(sts);

+        }

+      }

+    }

+  }

+

+  lemma Combine_DomSt(st: State, sts: set<State>, useCache: bool)

+    requires sts != {};

+    ensures DomSt(Combine({st} + sts, useCache)) == DomSt(st) + DomSt(Combine(sts, useCache));

+  {

+    var big := {st} + sts;

+    if st in sts {

+      assert big == sts;

+      assert forall states :: st in states ==> DomSt(st) <= DomSt_Union(states);

+      Combine_DomSt_X(sts, useCache);

+    } else {

+      var stPick := PickOne(big);

+      if stPick == st {

+        Combine_DomSt_X(big, useCache);

+        Combine_DomSt_X(sts, useCache);

+      } else if {stPick} == sts {

+        reveal_Combine();

+        assert Combine(sts, useCache) == stPick;

+        Combine_DomSt_X(big, useCache);

+      } else {

+        // assert forall states :: st in states ==> DomSt_Union(states) == DomSt(st) + DomSt_Union(states - {st});

+        // assert forall aa, bb :: DomSt_Union(aa + bb) == DomSt_Union(aa) + DomSt_Union(bb);

+        reveal_Combine();

+        assert big == {stPick} + ({st} + (sts - {stPick}));

+        calc {

+          DomSt(Combine(big, useCache));

+          { Combine_DomSt_X(big, useCache); }

+          DomSt_Union(big);

+          DomSt(stPick) + DomSt_Union(big - {stPick});

+          { Combine_DomSt_X(big - {stPick}, useCache); }

+          DomSt(stPick) + DomSt(Combine(big - {stPick}, useCache));

+          { assert big - {stPick} == {st} + (sts - {stPick});

+            Combine_DomSt(st, sts - {stPick}, useCache);

+          }

+          DomSt(stPick) + DomSt(st) + DomSt(Combine(big - {stPick} - {st}, useCache));

+          { Combine_DomSt_X(big - {stPick} - {st}, useCache); }

+          DomSt(stPick) + DomSt(st) + DomSt_Union(big - {stPick} - {st});

+          DomSt(st) + DomSt(stPick) + DomSt_Union(big - {stPick} - {st});

+          { DomSt_Union_Cons(stPick, big - {stPick} - {st}); }

+          DomSt(st) + DomSt_Union({stPick} + (big - {stPick} - {st}));

+          { assert {stPick} + (big - {stPick} - {st}) == big - {st} == sts; }

+          DomSt(st) + DomSt_Union(sts);

+          { Combine_DomSt_X(sts, useCache); }

+          DomSt(st) + DomSt(Combine(sts, useCache));

+        }

+      }

+    }

+  }

+  lemma {:timeLimit 15} StateCorrespondence_Ctor(stOrig: State, st: State, sts: set<State>, stC: State, stsC: set<State>)

+    requires ValidState(st) && forall s :: s in sts ==> ValidState(s);

+    requires Extends(stOrig, st) && forall s :: s in sts ==> Extends(stOrig, s);

+    requires StateCorrespondence(st, stC);

+    requires sts == {} <==> stsC == {};

+    requires sts != {} && stsC != {} ==> StateCorrespondence(Combine(sts, false), Combine(stsC, true));

+    requires Compatible({st} + sts) && Compatible({stC} + stsC);

+    ensures StateCorrespondence(Combine({st} + sts, false), Combine({stC} + stsC, true));

+  {

+    reveal_Combine();

+    if sts == {} {

+    } else {

+      reveal_StateCorrespondence();

+      var a, b := Combine({st} + sts, false), Combine({stC} + stsC, true);

+      assert Combine({st}, false) == st;

+      assert Combine({stC}, true) == stC;

+

+      calc {

+        DomSt(a);

+        { Combine_DomSt(st, sts, false); }

+        DomSt(st) + DomSt(Combine(sts, false));

+      <= { assert DomSt(Combine(sts, false)) <= DomSt(Combine(stsC, true)); }

+        DomSt(st) + DomSt(Combine(stsC, true));

+      <=

+        DomSt(stC) + DomSt(Combine(stsC, true));

+        { Combine_DomSt(stC, stsC, true); }

+        DomSt(b);

+      }

+      assert DomSt(a) <= DomSt(b);

+

+      forall p | p in DomSt(a)

+        ensures GetSt(p, a) == GetSt(p, b);

+      {

+        var stRepr := Combine_Representative(p, {st} + sts, false);

+        if stRepr == st {

+          CompatiblePick(p, stC, {stC} + stsC, true);

+        } else {

+          assert stRepr in sts;

+          CombineExpandsDomain(p, stRepr, sts, false);

+          CompatiblePick(p, stRepr, sts, false);

+          assert GetSt(p, a) == GetSt(p, stRepr) == GetSt(p, Combine(sts, false)) == GetSt(p, Combine(stsC, true));

+          var stReprC := Combine_Representative(p, stsC, true);

+          assert stReprC in {stC} + stsC;

+          CombineExpandsDomain(p, stReprC, {stC} + stsC, true);

+          CompatiblePick(p, stReprC, {stC} + stsC, true);

+        }

+      }

+      forall p | p !in DomSt(a) && p in DomSt(b)

+        ensures GetSt(p, b) == Oracle(p, a);

+      {

+        forall ensures p !in DomSt(st); {

+          CombineExpandsDomain(p, st, {st} + sts, false);

+        }

+        var stReprC := Combine_Representative(p, {stC} + stsC, true);

+        if stReprC == stC {

+          calc {

+            GetSt(p, b);

+            // by Combine_Representative and stRepr==stC

+            GetSt(p, stC);

+            // by StateCorrespondence(st, stC);

+            Oracle(p, st);

+            { OracleProperty(p, stOrig, st); }

+            Oracle(p, stOrig);

+            { Lemma_Combine({st} + sts, stOrig, false);

+              OracleProperty(p, stOrig, a);

+            }

+            Oracle(p, a);

+          }

+        } else {

+          assert stReprC in stsC;

+          calc {

+            GetSt(p, b);

+            GetSt(p, stReprC);

+            { CombineExpandsDomain(p, stReprC, stsC, true);

+              CompatiblePick(p, stReprC, stsC, true);

+            }

+            GetSt(p, Combine(stsC, true));

+            { Combine_DomSt(st, sts, false);

+              assert p !in DomSt(Combine(sts, false));

+              assert p in DomSt(Combine(stsC, true));

+            }

+            Oracle(p, Combine(sts, false));

+            { Lemma_Combine(sts, stOrig, false);

+              OracleProperty(p, stOrig, Combine(sts, false));

+            }

+            Oracle(p, stOrig);

+            { Lemma_Combine({st} + sts, stOrig, false);

+              OracleProperty(p, stOrig, a);

+            }

+            Oracle(p, a);

+          }

+        }

+      }

+    }

+  }

+

+  lemma CompatiblePick(p: Path, st: State, sts: set<State>, useCache: bool)

+    requires st in sts;

+    requires Compatible(sts);

+    requires p in DomSt(st) && p in DomSt(Combine(sts, useCache));

+    ensures GetSt(p, Combine(sts, useCache)) == GetSt(p, st);

+  {

+    reveal_Combine();

+  }

+  ghost method Combine_Representative(p: Path, sts: set<State>, useCache: bool) returns (stRepr: State)

+    requires sts != {} && p in DomSt(Combine(sts, useCache));

+    ensures stRepr in sts && p in DomSt(stRepr) && GetSt(p, stRepr) == GetSt(p, Combine(sts, useCache));

+  {

+    reveal_Combine();

+    var stPick := PickOne(sts);

+    if p in DomSt(stPick) {

+      stRepr := stPick;

+    } else {

+      assert GetSt(p, Combine(sts, useCache)) == GetSt(p, Combine(sts - {stPick}, useCache));

+      stRepr := Combine_Representative(p, sts - {stPick}, useCache);

+    }

+  }

+  lemma CombineExpandsDomain(p: Path, st: State, sts: set<State>, useCache: bool)

+    requires st in sts;

+    ensures p in DomSt(st) ==> p in DomSt(Combine(sts, useCache));

+  {

+    reveal_Combine();

+  }

+

+} // module M0

diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
new file mode 100644
index 00000000..dcfa1a2b
--- /dev/null
+++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
@@ -0,0 +1,660 @@
+/******* State *******/

+type State

+

+function GetSt(p: Path, st: State): Artifact

+function SetSt(p: Path, a: Artifact, st: State): State

+

+function DomSt(st: State): set<Path>

+

+function Restrict(paths: set<Path>, st: State): State

+  requires paths <= DomSt(st);

+  ensures

+    var st' := Restrict(paths, st);

+    DomSt(st') == paths && forall p :: p in paths ==> GetSt(p, st) == GetSt(p, st');

+

+function Union(st: State, st': State): State

+  ensures

+    var result := Union(st, st');

+    DomSt(result) == DomSt(st) + DomSt(st') &&

+    forall p :: p in DomSt(result) ==>

+      (p in DomSt(st) ==> GetSt(p, result) == GetSt(p, st)) &&

+      (p in DomSt(st') ==> GetSt(p, result) == GetSt(p, st'));

+

+ghost method StateEqualityProperty(st: State, st': State)

+  requires DomSt(st) == DomSt(st');

+  requires forall p :: p in DomSt(st) ==> GetSt(p, st) == GetSt(p, st');

+  ensures st == st';

+

+/******* Cached state *******/

+datatype StateC = S(st: State, c: Cache)

+

+function EmptyCache(): Cache

+  ensures DomC(EmptyCache()) == {};

+

+function GetC(h: HashValue, c: Cache): Triple<Expression, Expression, string>

+function SetC(h: HashValue, cmd: Triple<Expression, Expression, string>, c: Cache): Cache

+  ensures DomC(SetC(h, cmd, c)) == DomC(c) + {h};

+

+function UpdateC(cmd: Expression, deps: Expression, exts: Expression, stC: StateC): StateC

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings?;

+  ensures

+    var stC' := UpdateC(cmd, deps, exts, stC);

+    var hashValues := set e | e in exts.lit.strs :: Hash(Loc(cmd, deps, e));

+    stC'.st == stC.st &&

+    DomC(stC.c) + hashValues == DomC(stC'.c);

+  decreases exts.lit.strs;

+{

+  var strs := exts.lit.strs;

+  if strs == {} then

+    stC

+  else

+    var e := Choose(strs);

+    var c' := SetC(Hash(Loc(cmd, deps, e)), Trio(cmd, deps, e), stC.c);

+    var exts' := exprLiteral(litArrOfStrings(strs - {e}));

+    UpdateC(cmd, deps, exts', S(stC.st, c'))

+}

+

+ghost method UpdateCLemma(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings? &&

+    ConsistentCache(stC) &&

+    forall e :: e in exts.lit.strs ==> Loc(cmd, deps, e) in DomSt(stC.st);

+  ensures

+    var stC' := UpdateC(cmd, deps, exts, stC);

+    ConsistentCache(stC') &&

+    forall e :: e in exts.lit.strs ==> Hash(Loc(cmd, deps, e)) in DomC(stC'.c);

+  decreases exts.lit.strs;

+{

+  var strs := exts.lit.strs;

+  var stC' := UpdateC(cmd, deps, exts, stC);

+  if strs == {} {

+  } else {

+    var e := Choose(strs);

+    var c' := SetC(Hash(Loc(cmd, deps, e)), Trio(cmd, deps, e), stC.c);

+    var exts' := exprLiteral(litArrOfStrings(strs - {e}));

+    // note: This assertion is necessary.

+    assert stC' == UpdateC(cmd, deps, exts', S(stC.st, c'));

+    forall (cmd', deps', e' | Hash(Loc(cmd', deps', e')) == Hash(Loc(cmd, deps, e))) {

+      HashProperty(cmd', deps', e', cmd, deps, e);

+    }

+  }

+}

+

+function Choose(ss: set<string>): string

+  requires ss != {};

+{

+  var s :| s in ss; s

+}

+

+function DomC(c: Cache): set<HashValue>

+

+function UnionC(stC: StateC, stC': StateC): StateC

+  ensures

+    var result := UnionC(stC, stC');

+    DomSt(result.st) == DomSt(stC.st) + DomSt(stC'.st) &&

+    (forall p :: p in DomSt(result.st) ==>

+      (p in DomSt(stC.st) ==> GetSt(p, result.st) == GetSt(p, stC.st)) &&

+      (p in DomSt(stC'.st) ==> GetSt(p, result.st) == GetSt(p, stC'.st))) &&

+    DomC(result.c) == DomC(stC.c) + DomC(stC'.c) &&

+    (forall h :: h in DomC(result.c) ==>

+      (h in DomC(stC.c) ==> GetC(h, result.c) == GetC(h, stC.c)) &&

+      (h in DomC(stC'.c) ==> GetC(h, result.c) == GetC(h, stC'.c)));

+

+predicate CompatibleC(stsC: set<StateC>)

+{

+  forall stC, stC', p, h :: stC in stsC && stC' in stsC &&

+    p in DomSt(stC.st) && p in DomSt(stC'.st) &&

+    h in DomC(stC.c) && h in DomC(stC'.c) ==>

+      GetSt(p, stC.st) == GetSt(p, stC'.st) && GetC(h, stC.c) == GetC(h, stC'.c)

+}

+

+function CombineC(stsC: set<StateC>): StateC

+  requires stsC != {};

+  ensures

+    var stCombinedC := CombineC(stsC);

+    (forall stC :: stC in stsC ==> DomSt(stC.st) <= DomSt(stCombinedC.st)) &&

+    (forall stC, p :: stC in stsC && p in DomSt(stC.st) ==>

+      GetSt(p, stC.st) == GetSt(p, stCombinedC.st)) &&

+    (forall p :: p in DomSt(stCombinedC.st) ==> exists stC :: stC in stsC && p in DomSt(stC.st)) &&

+    (forall stC :: stC in stsC ==> DomC(stC.c) <= DomC(stCombinedC.c)) &&

+    (forall stC, h :: stC in stsC && h in DomC(stC.c) ==>

+      GetC(h, stC.c) == GetC(h, stCombinedC.c)) &&

+    (forall h :: h in DomC(stCombinedC.c) ==> exists stC :: stC in stsC && h in DomC(stC.c));

+{

+  var stC :| stC in stsC;

+  if stsC == {stC} then

+    stC

+  else

+    UnionC(stC, CombineC(stsC - {stC}))

+}

+

+ghost method CombineCLemma(stsC: set<StateC>)

+  requires stsC != {};

+  requires forall stC :: stC in stsC ==> ConsistentCache(stC);

+  ensures

+   var stC' := CombineC(stsC);

+   ConsistentCache(stC');

+{

+}

+

+predicate ConsistentCache(stC: StateC)

+{

+  forall cmd, deps, e :: Hash(Loc(cmd, deps, e)) in DomC(stC.c) ==>

+    Loc(cmd, deps, e) in DomSt(stC.st)

+}

+

+/******* {true} init {consistent_cache} *******/

+function ClearCache(stC: StateC): StateC

+  ensures

+    var stC' := ClearCache(stC);

+    // note: This follows directly from the definition.

+    stC.st == stC'.st && DomC(stC'.c) == {} &&

+    ConsistentCache(stC');

+{

+  S(stC.st, EmptyCache())

+}

+

+/******* Environment *******/

+type Env

+

+function EmptyEnv(): Env

+function GetEnv(id: Identifier, env: Env): Expression

+  ensures Value(GetEnv(id, env));

+function SetEnv(id: Identifier, expr: Expression, env: Env): Env

+  requires Value(expr);

+

+/******* Primitive function 'exec' *******/

+function exec(cmd: Expression, deps: Expression, exts: Expression, st: State): Tuple<Expression, State>

+

+ghost method ExecProperty(cmd: Expression, deps: Expression, exts: Expression, st: State)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings? &&

+    deps.lit.paths <= DomSt(st) &&

+    Pre(cmd, deps, exts, Restrict(deps.lit.paths, st));

+  ensures

+    var result := exec(cmd, deps, exts, st);

+    var expr', st' := result.fst, result.snd;

+    expr'.exprLiteral? && expr'.lit.litArrOfPaths? &&

+    expr'.lit.paths <= DomSt(st') &&

+    // note: We need this for the precondition of Restrict.

+    DomSt(st) <= DomSt(st') && st == Restrict(DomSt(st), st') &&

+    OneToOne(cmd, deps, exts, expr') &&

+    Post(cmd, deps, exts, Restrict(deps.lit.paths, st')) &&

+    forall p :: p !in DomSt(st) && p in DomSt(st') ==> p.OpaquePath?;

+

+predicate Pre(cmd: Expression, deps: Expression, exts: Expression, st: State)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings?;

+{

+  forall e :: e in exts.lit.strs ==>

+    Loc(cmd, deps, e) in DomSt(st) ==> GetSt(Loc(cmd, deps, e), st) == Res(cmd, deps, e, st)

+}

+

+predicate Post(cmd: Expression, deps: Expression, exts: Expression, st: State)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings?;

+{

+  forall e :: e in exts.lit.strs ==>

+    Loc(cmd, deps, e) in DomSt(st) && GetSt(Loc(cmd, deps, e), st) == Res(cmd, deps, e, st)

+}

+

+function Res(cmd: Expression, deps: Expression, ext: string, st: State): Artifact

+

+predicate OneToOne(cmd: Expression, deps: Expression, exts: Expression, paths: Expression)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings? &&

+    paths.exprLiteral? && paths.lit.litArrOfPaths?;

+{

+  forall e :: e in exts.lit.strs ==> Loc(cmd, deps, e) in paths.lit.paths

+}

+

+function Loc(cmd: Expression, deps: Expression, ext: string): Path

+

+/******* Primitive function 'execC' *******/

+function execC(cmd: Expression, deps: Expression, exts: Expression, stC: StateC): Tuple<Expression, StateC>

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings?;

+{

+  if forall e | e in exts.lit.strs :: Hash(Loc(cmd, deps, e)) in DomC(stC.c) then

+    var paths := set e | e in exts.lit.strs :: Loc(cmd, deps, e);

+    var expr' := exprLiteral(litArrOfPaths(paths));

+    Pair(expr', stC)

+  else

+    var result := exec(cmd, deps, exts, stC.st);

+    var expr', st' := result.fst, result.snd;

+    var stC' := UpdateC(cmd, deps, exts, S(st', stC.c));

+    Pair(expr', stC')

+}

+

+ghost method ExecCProperty(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings? &&

+    deps.lit.paths <= DomSt(stC.st) &&

+    PreC(cmd, deps, exts, stC) &&

+    ConsistentCache(stC);

+  ensures

+    var result := execC(cmd, deps, exts, stC);

+    var expr', stC' := result.fst, result.snd;

+    expr'.exprLiteral? && expr'.lit.litArrOfPaths? &&

+    expr'.lit.paths <= DomSt(stC'.st) &&

+    // note: We need this for the precondition of Restrict.

+    DomSt(stC.st) <= DomSt(stC'.st) && stC.st == Restrict(DomSt(stC.st), stC'.st) &&

+    OneToOne(cmd, deps, exts, expr') &&

+    PostC(cmd, deps, exts, stC') &&

+    (forall p :: p !in DomSt(stC.st) && p in DomSt(stC'.st) ==> p.OpaquePath?) &&

+    ConsistentCache(stC');

+{

+  var result := execC(cmd, deps, exts, stC);

+  var expr', stC' := result.fst, result.snd;

+  if forall e | e in exts.lit.strs :: Hash(Loc(cmd, deps, e)) in DomC(stC.c) {

+    StateEqualityProperty(stC.st, Restrict(DomSt(stC.st), stC'.st));

+  } else {

+    ExecProperty(cmd, deps, exts, stC.st);

+    var execResult := exec(cmd, deps, exts, stC.st);

+    var st' := execResult.snd;

+    assert DomSt(stC.st) <= DomSt(st');

+    StateEqualityProperty(stC'.st, st');

+    UpdateCLemma(cmd, deps, exts, S(st', stC.c));

+  }

+}

+

+predicate PreC(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings? &&

+    // note: We need this for the precondition of Restrict.

+    deps.lit.paths <= DomSt(stC.st);

+{

+  Pre(cmd, deps, exts, Restrict(deps.lit.paths, stC.st)) &&

+  forall e :: e in exts.lit.strs ==> Hash(Loc(cmd, deps, e)) in DomC(stC.c) ==>

+    Loc(cmd, deps, e) in deps.lit.paths

+}

+

+predicate PostC(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

+  requires

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings? &&

+    // note: We need this for the precondition of Restrict.

+    deps.lit.paths <= DomSt(stC.st);

+{

+  Post(cmd, deps, exts, Restrict(deps.lit.paths, stC.st)) &&

+  forall e :: e in exts.lit.strs ==> Hash(Loc(cmd, deps, e)) in DomC(stC.c)

+}

+

+function Hash(p: Path): HashValue

+

+ghost method HashProperty(cmd: Expression, deps: Expression, ext: string, cmd': Expression, deps': Expression, ext': string)

+  requires Hash(Loc(cmd, deps, ext)) == Hash(Loc(cmd', deps', ext'));

+  ensures cmd == cmd' && deps == deps' && ext == ext';

+

+/******* Grammar *******/

+datatype Program = Program(stmts: seq<Statement>)

+

+datatype Statement = stmtVariable(id: Identifier, expr: Expression) |

+                     stmtReturn(ret: Expression)

+

+datatype Expression = exprLiteral(lit: Literal) | exprIdentifier(id: Identifier) |

+                      exprIf(cond: Expression, ifTrue: Expression, ifFalse: Expression) |

+                      exprAnd(conj0: Expression, conj1: Expression) |

+                      exprOr(disj0: Expression, disj1: Expression) |

+                      exprInvocation(fun: Expression, args: seq<Expression>) |

+                      exprError(r: Reason)

+

+datatype Literal = litTrue | litFalse | litUndefined | litNull |

+                   litNumber(num: int) | litString(str: string) |

+                   litPrimitive(prim: Primitive) |

+                   litArrOfPaths(paths: set<Path>) |

+                   litArrOfStrings(strs: set<string>) |

+                   litArray(arr: seq<Expression>)

+

+datatype Primitive = primCreatePath | primExec

+

+datatype Reason = rCompatibility | rValidity | rInconsistentCache

+

+datatype Path = OpaquePath(int) | TransparentPath(int)

+type string(==)

+type Artifact

+type Identifier

+

+type Cache

+type HashValue

+

+datatype Tuple<A, B> = Pair(fst: A, snd: B)

+datatype Triple<A, B, C> = Trio(fst: A, snd: B, trd: C)

+

+/******* Values *******/

+predicate Value(expr: Expression)

+{

+  expr.exprLiteral?

+}

+

+/******* Semantics *******/

+

+predicate Legal(stmts: seq<Statement>)

+{

+  |stmts| != 0

+}

+

+function Arity(prim: Primitive): nat

+{

+  match prim

+  case primCreatePath => 1

+  case primExec => 3

+}

+

+/******* Function 'buildC' *******/

+function buildC(prog: Program, stC: StateC): Tuple<Expression, StateC>

+  requires Legal(prog.stmts);

+{

+  doC(prog.stmts, stC, EmptyEnv())

+}

+

+/******* Function 'doC' *******/

+function doC(stmts: seq<Statement>, stC: StateC, env: Env): Tuple<Expression, StateC>

+  requires Legal(stmts);

+{

+  var stmt := stmts[0];

+  if stmt.stmtVariable? then

+    var result := evalC(stmt.expr, stC, env);

+    var expr', stC' := result.fst, result.snd;

+    if Value(expr') then

+      var env' := SetEnv(stmt.id, expr', env);

+      if Legal(stmts[1..]) then

+        doC(stmts[1..], stC', env')

+      else

+        Pair(expr', stC')

+    else

+      Pair(exprError(rValidity), stC)

+  // todo(maria): Add the recursive case.

+  else

+    assert stmt.stmtVariable? || stmt.stmtReturn?;

+    evalC(stmt.ret, stC, env)

+}

+

+/******* Function 'evalC' *******/

+function evalC(expr: Expression, stC: StateC, env: Env): Tuple<Expression, StateC>

+  decreases expr;

+{

+  if Value(expr) then

+    Pair(expr, stC)

+  // identifier

+  else if expr.exprIdentifier? then

+    Pair(GetEnv(expr.id, env), stC)

+  // if-expression

+  else if expr.exprIf? && expr.cond.exprLiteral? && expr.cond.lit == litTrue then

+    evalC(expr.ifTrue, stC, env)

+  else if expr.exprIf? && expr.cond.exprLiteral? && expr.cond.lit == litFalse then

+    evalC(expr.ifFalse, stC, env)

+  else if expr.exprIf? then

+    var result := evalC(expr.cond, stC, env);

+    var cond', stC' := result.fst, result.snd;

+    if cond'.exprLiteral? && cond'.lit == litTrue then

+      evalC(expr.ifTrue, stC', env)

+    else if cond'.exprLiteral? && cond'.lit == litFalse then

+      evalC(expr.ifFalse, stC', env)

+    else

+      Pair(exprError(rValidity), stC)

+  // and-expression

+  else if expr.exprAnd? then

+    var result := evalC(expr.conj0, stC, env);

+    var conj0', stC' := result.fst, result.snd;

+    if conj0'.exprLiteral? && conj0'.lit == litTrue then

+      evalC(expr.conj1, stC', env)

+    else if conj0'.exprLiteral? && conj0'.lit == litFalse then

+      Pair(exprLiteral(litFalse), stC')

+    else

+      Pair(exprError(rValidity), stC)

+  // or-expression

+  else if expr.exprOr? then

+    var result := evalC(expr.disj0, stC, env);

+    var disj0', stC' := result.fst, result.snd;

+    if disj0'.exprLiteral? && disj0'.lit == litTrue then

+      Pair(exprLiteral(litTrue), stC')

+    else if disj0'.exprLiteral? && disj0'.lit == litFalse then

+      evalC(expr.disj1, stC', env)

+    else

+      Pair(exprError(rValidity), stC)

+  // invocation

+  else if expr.exprInvocation? then

+    var resultFun := evalC(expr.fun, stC, env);

+    var fun', stC' := resultFun.fst, resultFun.snd;

+    var resultArgs := evalArgsC(expr, expr.args, stC, env);

+    var args', stsC' := resultArgs.fst, resultArgs.snd;

+    var stsC'' := {stC'} + stsC';

+    if CompatibleC(stsC'') then

+      var stCombinedC := CombineC(stsC'');

+      // primitive functions

+      if fun'.exprLiteral? && fun'.lit.litPrimitive? then

+        // primitive function 'execC'

+        if fun'.lit.prim.primExec? then

+          if |args'| == Arity(primExec) && ValidArgsC(primExec, args', stCombinedC) then

+            execC(args'[0], args'[1], args'[2], stCombinedC)

+          else

+            if ConsistentCache(stCombinedC) then

+              Pair(exprError(rValidity), stC)

+            else

+              Pair(exprError(rInconsistentCache), stC)

+        else

+        // primitive function 'createPath'

+        // todo(maria): Add primitive function 'createPath'.

+          Pair(exprError(rValidity), stC)

+      // todo(maria): Add non-primitive invocations.

+      else

+        Pair(exprError(rValidity), stC)

+    else

+      Pair(exprError(rCompatibility), stC)

+  // error

+  else

+    Pair(exprError(rValidity), stC)

+}

+

+function evalArgsC(expr: Expression, args: seq<Expression>, stC: StateC, env: Env):

+         Tuple<seq<Expression>, set<StateC>>

+  requires forall arg :: arg in args ==> arg < expr;

+  decreases expr, |args| + 1;

+

+{

+  evalArgsC'(expr, args, stC, env, [], {})

+}

+

+function evalArgsC'(expr: Expression, args: seq<Expression>, stC: StateC, env: Env,

+                    args': seq<Expression>, stsC': set<StateC>):

+         Tuple<seq<Expression>, set<StateC>>

+  requires forall arg :: arg in args ==> arg < expr;

+  decreases expr, |args|;

+{

+  if args == [] then

+    Pair(args', stsC')

+  else

+    var arg := args[0];

+    var result := evalC(arg, stC, env);

+    var arg', stC' := result.fst, result.snd;

+    evalArgsC'(expr, args[1..], stC, env, args' + [arg'], stsC' + {stC'})

+}

+

+predicate ValidArgsC(prim: Primitive, args: seq<Expression>, stC: StateC)

+  requires prim.primExec? ==> |args| == 3;

+  requires prim.primCreatePath? ==> |args| == 1;

+{

+  match prim

+  case primCreatePath => false

+  case primExec =>

+    var cmd, deps, exts := args[0], args[1], args[2];

+    cmd.exprLiteral? && cmd.lit.litString? &&

+    deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+    exts.exprLiteral? && exts.lit.litArrOfStrings? &&

+    deps.lit.paths <= DomSt(stC.st) &&

+    PreC(cmd, deps, exts, stC)

+}

+

+/******* {consistent_cache} buildC {no_bad_cache_error /\ consistent_cache} *******/

+ghost method CachedBuildsTheorem(prog: Program, stC: StateC)

+  requires Legal(prog.stmts);

+  requires ConsistentCache(stC);

+  ensures

+    var result := buildC(prog, stC);

+    var expr', stC' := result.fst, result.snd;

+    ConsistentCache(stC') &&

+    expr'.exprError? ==> expr'.r != rInconsistentCache;

+{

+  BuildCLemma(prog, stC);

+}

+

+ghost method BuildCLemma(prog: Program, stC: StateC)

+  requires Legal(prog.stmts);

+  requires ConsistentCache(stC);

+  ensures

+    var result := buildC(prog, stC);

+    var expr', stC' := result.fst, result.snd;

+    ConsistentCache(stC') && (expr'.exprError? ==> expr'.r != rInconsistentCache);

+{

+  DoCLemma(prog.stmts, stC, EmptyEnv());

+}

+

+ghost method DoCLemma(stmts: seq<Statement>, stC: StateC, env: Env)

+  requires Legal(stmts);

+  requires ConsistentCache(stC);

+  ensures

+    var result := doC(stmts, stC, env);

+    var expr', stC' := result.fst, result.snd;

+    ConsistentCache(stC') && (expr'.exprError? ==> expr'.r != rInconsistentCache);

+{

+  var stmt := stmts[0];

+  if stmt.stmtVariable? {

+    EvalCLemma(stmt.expr, stC, env);

+    var result := evalC(stmt.expr, stC, env);

+    var expr', stC' := result.fst, result.snd;

+    if Value(expr') {

+      var env' := SetEnv(stmt.id, expr', env);

+      if Legal(stmts[1..]) {

+        DoCLemma(stmts[1..], stC', env');

+      } else { }

+    } else { }

+  // todo(maria): Add the recursive case.

+  } else {

+    assert stmt.stmtVariable? || stmt.stmtReturn?;

+    EvalCLemma(stmt.ret, stC, env);

+  }

+}

+

+ghost method {:induction expr} EvalCLemma(expr: Expression, stC: StateC, env: Env)

+  requires ConsistentCache(stC);

+  ensures

+    var result := evalC(expr, stC, env);

+    var expr', stC' := result.fst, result.snd;

+    ConsistentCache(stC') && (expr'.exprError? ==> expr'.r != rInconsistentCache);

+  decreases expr;

+{

+  if Value(expr) {

+  } else if expr.exprIdentifier? {

+  } else if expr.exprIf? && expr.cond.exprLiteral? && expr.cond.lit == litTrue {

+  } else if expr.exprIf? && expr.cond.exprLiteral? && expr.cond.lit == litFalse {

+  } else if expr.exprIf? {

+    var result := evalC(expr.cond, stC, env);

+    var cond', stC' := result.fst, result.snd;

+    if cond'.exprLiteral? && cond'.lit == litTrue {

+      EvalCLemma(expr.ifTrue, stC', env);

+    } else if cond'.exprLiteral? && cond'.lit == litFalse {

+      EvalCLemma(expr.ifFalse, stC', env);

+    } else { }

+  } else if expr.exprAnd? {

+    var result := evalC(expr.conj0, stC, env);

+    var conj0', stC' := result.fst, result.snd;

+    if conj0'.exprLiteral? && conj0'.lit == litTrue {

+      EvalCLemma(expr.conj1, stC', env);

+    } else if conj0'.exprLiteral? && conj0'.lit == litFalse {

+    } else { }

+  } else if expr.exprOr? {

+    var result := evalC(expr.disj0, stC, env);

+    var disj0', stC' := result.fst, result.snd;

+    if disj0'.exprLiteral? && disj0'.lit == litTrue {

+    } else if disj0'.exprLiteral? && disj0'.lit == litFalse {

+      EvalCLemma(expr.disj1, stC', env);

+    } else { }

+  } else if expr.exprInvocation? {

+    EvalCLemma(expr.fun, stC, env);

+    var resultFun := evalC(expr.fun, stC, env);

+    var fun', stC' := resultFun.fst, resultFun.snd;

+    EvalArgsCLemma(expr, expr.args, stC, env);

+    var resultArgs := evalArgsC(expr, expr.args, stC, env);

+    var args', stsC' := resultArgs.fst, resultArgs.snd;

+    var stsC'' := {stC'} + stsC';

+    if CompatibleC(stsC'') {

+      CombineCLemma(stsC'');

+      var stCombinedC := CombineC(stsC'');

+      if fun'.exprLiteral? && fun'.lit.litPrimitive? {

+        if fun'.lit.prim.primExec? {

+          if |args'| == Arity(primExec) && ValidArgsC(primExec, args', stCombinedC) {

+            ExecCProperty(args'[0], args'[1], args'[2], stCombinedC);

+            var resultExec := execC(args'[0], args'[1], args'[2], stCombinedC);

+            var stExecC := resultExec.snd;

+            // note: This assertion is necessary.

+            assert DomSt(stC'.st) <= DomSt(stCombinedC.st);

+            forall (p | p in DomSt(stCombinedC.st) && p in DomSt(stExecC.st))

+              ensures GetSt(p, stCombinedC.st) == GetSt(p, stExecC.st);

+            {

+              assert DomSt(stCombinedC.st) <= DomSt(stExecC.st);

+              assert stCombinedC.st == Restrict(DomSt(stCombinedC.st), stExecC.st);

+            }

+          } else {

+            if ConsistentCache(stCombinedC) {

+            } else { }

+          }

+        } else { }

+      } else { }

+    } else { }

+  } else { }

+}

+

+ghost method EvalArgsCLemma(expr: Expression, args: seq<Expression>, stC: StateC, env: Env)

+  requires ConsistentCache(stC);

+  requires forall arg :: arg in args ==> arg < expr;

+  ensures

+    var result := evalArgsC(expr, args, stC, env);

+    var stsC' := result.snd;

+    forall stC' :: stC' in stsC' ==> ConsistentCache(stC');

+  decreases expr, |args| + 1;

+

+{

+  EvalArgsC'Lemma(expr, args, stC, env, [], {});

+}

+

+ghost method EvalArgsC'Lemma(expr: Expression, args: seq<Expression>, stC: StateC, env: Env,

+                             args': seq<Expression>, stsC': set<StateC>)

+  requires ConsistentCache(stC);

+  requires forall stC' :: stC' in stsC' ==> ConsistentCache(stC');

+  requires forall arg :: arg in args ==> arg < expr;

+  ensures

+    var result := evalArgsC'(expr, args, stC, env, args', stsC');

+    var stsC'' := result.snd;

+    forall stC'' :: stC'' in stsC'' ==> ConsistentCache(stC'');

+  decreases expr, |args|;

+{

+  if args == [] {

+  } else {

+    var arg := args[0];

+    EvalCLemma(arg, stC, env);

+    var result := evalC(arg, stC, env);

+    var arg', stC' := result.fst, result.snd;

+    EvalArgsC'Lemma(expr, args[1..], stC, env, args' + [arg'], stsC' + {stC'});

+  }

+}
\ No newline at end of file
diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
new file mode 100644
index 00000000..e76f60d8
--- /dev/null
+++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
@@ -0,0 +1,835 @@
+// This module proves the correctness of the algorithms.  It leaves a number of things undefined.

+// They are defined in refinement modules below.

+abstract module M0 {

+  /******* State *******/

+  type State

+  function DomSt(st: State): set<Path>

+  function GetSt(p: Path, st: State): Artifact

+    requires p in DomSt(st);

+

+  predicate ValidState(st: State)

+  {

+    forall p :: p in DomSt(st) ==> WellFounded(p)

+  }

+  predicate WellFounded(p: Path)

+

+  // The specification given for this Union is liberal enough to allow incompatible

+  // states, that is, st and st' are allowed to disagree on some paths.  Any such disagreement

+  // will be resolved in favor of st.  For the purpose of supporting function Combine, we are

+  // only ever interested in combining/unioning compatible states anyhow.

+  function Union(st: State, st': State): State

+    ensures

+      var result := Union(st, st');

+      DomSt(result) == DomSt(st) + DomSt(st') &&

+      forall p :: p in DomSt(result) ==>

+        GetSt(p, result) == GetSt(p, if p in DomSt(st) then st else st');

+

+  predicate Compatible(sts: set<State>)

+  {

+    forall st, st', p :: st in sts && st' in sts && p in DomSt(st) && p in DomSt(st') ==>

+      GetSt(p, st) == GetSt(p, st')

+  }

+

+  function Combine(sts: set<State>): State

+    requires sts != {};

+  {

+    var st :| st in sts;

+    if sts == {st} then

+      st

+    else

+      Union(st, Combine(sts - {st}))

+  }

+  lemma Lemma_Combine(sts: set<State>, parent: State)

+    requires sts != {};

+    requires forall st :: st in sts ==> ValidState(st) && Extends(parent, st);

+    ensures ValidState(Combine(sts)) && Extends(parent, Combine(sts));

+  {

+    forall st | st in sts && (sts == {st} || Combine(sts) == Union(st, Combine(sts - {st})))

+      ensures Extends(parent, Combine(sts));

+    {

+    }

+  }

+

+  /******* Environment *******/

+  type Env

+  predicate ValidEnv(env: Env)

+  function EmptyEnv(): Env

+    ensures ValidEnv(EmptyEnv());

+  function GetEnv(id: Identifier, env: Env): Expression

+    requires ValidEnv(env);

+    ensures Value(GetEnv(id, env));

+  function SetEnv(id: Identifier, expr: Expression, env: Env): Env

+    requires ValidEnv(env) && Value(expr);

+    ensures ValidEnv(SetEnv(id, expr, env));

+

+  /******* Primitive function 'exec' *******/

+  function exec(cmd: string, deps: set<Path>, exps: set<string>, st: State): Tuple<set<Path>, State>

+

+  lemma ExecProperty(cmd: string, deps: set<Path>, exps: set<string>, st: State)

+    requires

+      ValidState(st) &&

+      deps <= DomSt(st) &&

+      Pre(cmd, deps, exps, st);

+    ensures

+      var Pair(paths, st') := exec(cmd, deps, exps, st);

+      ValidState(st') &&

+      Extends(st, st') &&

+      OneToOne(cmd, deps, exps, paths) &&

+      Post(cmd, deps, exps, st');

+

+  predicate Pre(cmd: string, deps: set<Path>, exps: set<string>, st: State)

+  {

+    forall e :: e in exps ==>

+      Loc(cmd, deps, e) in DomSt(st) ==> GetSt(Loc(cmd, deps, e), st) == Oracle(Loc(cmd, deps, e), st)

+  }

+

+  predicate OneToOne(cmd: string, deps: set<Path>, exps: set<string>, paths: set<Path>)

+  {

+    forall e :: e in exps ==> Loc(cmd, deps, e) in paths

+  }

+

+  predicate Post(cmd: string, deps: set<Path>, exps: set<string>, st: State)

+  {

+    forall e :: e in exps ==>

+      Loc(cmd, deps, e) in DomSt(st) && GetSt(Loc(cmd, deps, e), st) == Oracle(Loc(cmd, deps, e), st)

+  }

+

+  // Oracle is like an oracle, because for a given path and state, it flawlessly predicts the unique artifact

+  // that may live at that path.  This is less magical than it seems, because Loc is injective,

+  // and therefore one can extract a unique (cmd,deps,exp) from p, and it's not so hard to see

+  // how the oracle may "know" the artifact that results from that.

+  function Oracle(p: Path, st: State): Artifact

+

+  // The oracle never changes its mind.  Therefore, if st0 is extended into st1 only by following

+  // what the oracle predicts, then no predictions change.

+  lemma OracleProperty(p: Path, st0: State, st1: State)

+    requires Extends(st0, st1);

+    ensures Oracle(p, st0) == Oracle(p, st1);

+

+  predicate Extends(st: State, st': State)

+  {

+    DomSt(st) <= DomSt(st') &&

+    (forall p :: p in DomSt(st) ==> GetSt(p, st') == GetSt(p, st)) &&

+    (forall p :: p !in DomSt(st) && p in DomSt(st') ==> GetSt(p, st') == Oracle(p, st))

+  }

+

+  lemma Lemma_ExtendsTransitive(st0: State, st1: State, st2: State)

+    requires Extends(st0, st1) && Extends(st1, st2);

+    ensures Extends(st0, st2);

+  {

+    forall p { OracleProperty(p, st0, st1); }

+  }

+

+

+  /******* Grammar *******/

+  datatype Program = Program(stmts: seq<Statement>)

+

+  datatype Statement = stmtVariable(id: Identifier, expr: Expression) |

+                       stmtReturn(ret: Expression)

+

+  datatype Expression = exprLiteral(lit: Literal) | exprIdentifier(id: Identifier) |

+                        exprIf(cond: Expression, ifTrue: Expression, ifFalse: Expression) |

+                        exprAnd(conj0: Expression, conj1: Expression) |

+                        exprOr(disj0: Expression, disj1: Expression) |

+                        exprInvocation(fun: Expression, args: seq<Expression>) |

+                        exprError(r: Reason)

+

+  datatype Literal = litTrue | litFalse | litUndefined | litNull |

+                     litNumber(num: int) | litString(str: string) |

+                     litPrimitive(prim: Primitive) |

+                     // Q(rustan): How can I check the type of elems?

+                     // Q(rustan): What happens with the sets?

+                     litArrOfPaths(paths: set<Path>) |

+                     litArrOfStrings(strs: set<string>) |

+                     litArray(arr: seq<Expression>)

+

+  datatype Primitive = primCreatePath | primExec

+

+  datatype Reason = rCompatibility | rValidity

+

+  type Path(==)

+  function Loc(cmd: string, deps: set<Path>, exp: string): Path

+

+  type string(==)

+  type Artifact

+  type Identifier

+

+  datatype Tuple<A, B> = Pair(fst: A, snd: B)

+

+  /******* Values *******/

+  predicate Value(expr: Expression)

+  {

+    expr.exprLiteral?

+  }

+

+  /******* Semantics *******/

+

+  /******* Function 'build' *******/

+  function build(prog: Program, st: State): Tuple<Expression, State>

+    requires Legal(prog.stmts);

+  {

+    do(prog.stmts, st, EmptyEnv())

+  }

+

+  /******* Function 'do' *******/

+  function do(stmts: seq<Statement>, st: State, env: Env): Tuple<Expression, State>

+    requires Legal(stmts) && ValidEnv(env);

+  {

+    var stmt := stmts[0];

+    if stmt.stmtVariable? then

+      var Pair(expr', st') := eval(stmt.expr, st, env);

+      if Value(expr') then

+        var env' := SetEnv(stmt.id, expr', env);

+        if Legal(stmts[1..]) then

+          do(stmts[1..], st', env')

+        else

+          Pair(expr', st')

+      else

+        Pair(exprError(rValidity), st)

+    // todo(maria): Add the recursive case.

+    else

+      eval(stmt.ret, st, env)

+  }

+

+  predicate Legal(stmts: seq<Statement>)

+  {

+    |stmts| != 0

+  }

+

+  /******* Function 'eval' *******/

+  function eval(expr: Expression, st: State, env: Env): Tuple<Expression, State>

+     requires ValidEnv(env);

+     decreases expr;

+  {

+    if Value(expr) then

+      Pair(expr, st)

+    // identifier

+    else if expr.exprIdentifier? then

+      Pair(GetEnv(expr.id, env), st)

+    // if-expression

+    else if expr.exprIf? then

+      var Pair(cond', st') := eval(expr.cond, st, env);

+      if cond'.exprLiteral? && cond'.lit == litTrue then

+        eval(expr.ifTrue, st', env)

+      else if cond'.exprLiteral? && cond'.lit == litFalse then

+        eval(expr.ifFalse, st', env)

+      else

+        Pair(exprError(rValidity), st)  // todo: should this be st' (and same for the error cases below)?

+    // and-expression

+    else if expr.exprAnd? then

+      var Pair(conj0', st') := eval(expr.conj0, st, env);

+      if conj0'.exprLiteral? && conj0'.lit == litTrue then

+        eval(expr.conj1, st', env)

+      else if conj0'.exprLiteral? && conj0'.lit == litFalse then

+        Pair(exprLiteral(litFalse), st')

+      else

+        Pair(exprError(rValidity), st)

+    // or-expression

+    else if expr.exprOr? then

+      var Pair(disj0', st') := eval(expr.disj0, st, env);

+      if disj0'.exprLiteral? && disj0'.lit == litTrue then

+        Pair(exprLiteral(litTrue), st')

+      else if disj0'.exprLiteral? && disj0'.lit == litFalse then

+        eval(expr.disj1, st', env)

+      else

+        Pair(exprError(rValidity), st)

+    // invocation

+    else if expr.exprInvocation? then

+      var Pair(fun', st') := eval(expr.fun, st, env);

+      var Pair(args', sts') := evalArgs(expr, expr.args, st, env);

+      var sts'' := {st'} + sts';

+      if !Compatible(sts'') then

+        Pair(exprError(rCompatibility), st)

+      else

+        var stCombined := Combine(sts'');

+        // primitive functions

+        if fun'.exprLiteral? && fun'.lit.litPrimitive? then

+          // primitive function 'exec'

+          if fun'.lit.prim.primExec? then

+            if |args'| == Arity(primExec) && ValidArgs(primExec, args', stCombined) then

+              var ps := exec(args'[0].lit.str, args'[1].lit.paths, args'[2].lit.strs, stCombined);

+              Pair(exprLiteral(litArrOfPaths(ps.fst)), ps.snd)

+            else

+              Pair(exprError(rValidity), st)

+          else

+          // primitive function 'createPath'

+          // todo(maria): Add primitive function 'createPath'.

+            Pair(exprError(rValidity), st)

+        // todo(maria): Add non-primitive invocations.

+        else

+          Pair(exprError(rValidity), st)

+    // error

+    else

+      Pair(exprError(rValidity), st)

+  }

+

+  function evalArgs(context: Expression, args: seq<Expression>, stOrig: State, env: Env): Tuple<seq<Expression>, set<State>>

+    requires

+      ValidEnv(env) &&

+      forall arg :: arg in args ==> arg < context;

+    decreases context, |args|;

+  {

+    if args == [] then

+      Pair([], {})

+    else

+      var r := eval(args[0], stOrig, env);

+      var rr := evalArgs(context, args[1..], stOrig, env);

+      Pair([r.fst] + rr.fst, {r.snd} + rr.snd)

+  }

+

+  function Arity(prim: Primitive): nat

+  {

+    match prim

+    case primCreatePath => 1

+    case primExec => 3

+  }

+

+  predicate ValidArgs(prim: Primitive, args: seq<Expression>, st: State)

+    requires prim.primExec? ==> |args| == 3;

+    requires prim.primCreatePath? ==> |args| == 1;

+  {

+    match prim

+    case primCreatePath => false

+    case primExec =>

+      var cmd, deps, exps := args[0], args[1], args[2];

+      cmd.exprLiteral? && cmd.lit.litString? &&

+      deps.exprLiteral? && deps.lit.litArrOfPaths? &&

+      exps.exprLiteral? && exps.lit.litArrOfStrings? &&

+      deps.lit.paths <= DomSt(st) &&

+      Pre(cmd.lit.str, deps.lit.paths, exps.lit.strs, st)

+  }

+

+  /******* Parallel builds are race-free *******/

+  lemma ParallelBuildsTheorem(prog: Program, st: State)

+    requires Legal(prog.stmts) && ValidState(st);

+    ensures

+      var Pair(expr', st') := build(prog, st);

+      ValidState(st') &&

+      (expr'.exprError? ==> expr'.r == rValidity);

+  {

+    var _, _ := BuildLemma(prog, st);

+  }

+

+  lemma BuildLemma(prog: Program, st: State) returns (expr': Expression, st': State)

+    requires Legal(prog.stmts) && ValidState(st);

+    ensures

+      build(prog, st) == Pair(expr', st') &&

+      ValidState(st') &&

+      Extends(st, st') &&

+      (expr'.exprError? ==> expr'.r == rValidity);

+  {

+    var result := build(prog, st);

+    expr', st' := result.fst, result.snd;

+    var _, _ := DoLemma(prog.stmts, st, EmptyEnv());

+  }

+

+  lemma DoLemma(stmts: seq<Statement>, st: State, env: Env) returns (expr': Expression, st': State)

+    requires Legal(stmts) && ValidState(st) && ValidEnv(env);

+    ensures

+      Pair(expr', st') == do(stmts, st, env) &&

+      ValidState(st') &&

+      Extends(st, st') &&

+      (expr'.exprError? ==> expr'.r == rValidity);

+  {

+    var result := do(stmts, st, env);

+    expr', st' := result.fst, result.snd;

+    var stmt := stmts[0];

+    if stmt.stmtVariable? {

+      var expr', st' := EvalLemma(stmt.expr, st, env);

+      if Value(expr') {

+        var env' := SetEnv(stmt.id, expr', env);

+        if Legal(stmts[1..]) {

+          var _, st'' := DoLemma(stmts[1..], st', env');

+          Lemma_ExtendsTransitive(st, st', st'');

+        } else { 

+        }

+      } else { }

+    } else {

+      assert stmt.stmtVariable? || stmt.stmtReturn?;

+      var _, _ := EvalLemma(stmt.ret, st, env);

+    }

+  }

+

+  lemma EvalLemma(expr: Expression, st: State, env: Env) returns (expr': Expression, st': State)

+    requires ValidState(st) && ValidEnv(env);

+    ensures

+      Pair(expr', st') == eval(expr, st, env) &&

+      ValidState(st') &&

+      Extends(st, st') &&

+      (expr'.exprError? ==> expr'.r == rValidity);

+    decreases expr;

+  {

+    var result := eval(expr, st, env);

+    expr', st' := result.fst, result.snd;

+    if Value(expr) {

+    } else if expr.exprIdentifier? {

+    } else if expr.exprIf? {

+      var cond', st' := EvalLemma(expr.cond, st, env);

+      if cond'.exprLiteral? && cond'.lit == litTrue {

+        var _, st'' := EvalLemma(expr.ifTrue, st', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else if cond'.exprLiteral? && cond'.lit == litFalse {

+        var _, st'' := EvalLemma(expr.ifFalse, st', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else { }

+    } else if expr.exprAnd? {

+      var conj0', st' := EvalLemma(expr.conj0, st, env);

+      if conj0'.exprLiteral? && conj0'.lit == litTrue {

+        var _, st'' := EvalLemma(expr.conj1, st', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else if conj0'.exprLiteral? && conj0'.lit == litFalse {

+      } else { }

+    } else if expr.exprOr? {

+      var disj0', st' := EvalLemma(expr.disj0, st, env);

+      if disj0'.exprLiteral? && disj0'.lit == litTrue {

+      } else if disj0'.exprLiteral? && disj0'.lit == litFalse {

+        var _, st'' := EvalLemma(expr.disj1, st', env);

+        Lemma_ExtendsTransitive(st, st', st'');

+      } else { }

+    } else if expr.exprInvocation? {

+      var fun', st' := EvalLemma(expr.fun, st, env);

+      var args', sts' := EvalArgsLemma(expr, expr.args, st, env);

+      var sts'' := {st'} + sts';

+      if Compatible(sts'') {

+        var stCombined := Combine(sts'');

+        Lemma_Combine(sts'', st);

+        if fun'.exprLiteral? && fun'.lit.litPrimitive? {

+          if fun'.lit.prim.primExec? {

+            if |args'| == Arity(primExec) && ValidArgs(primExec, args', stCombined) {

+              var cmd, deps, exp := args'[0].lit.str, args'[1].lit.paths, args'[2].lit.strs;

+              ExecProperty(cmd, deps, exp, stCombined);

+              var resultExec := exec(cmd, deps, exp, stCombined);

+              var stExec := resultExec.snd;

+              Lemma_ExtendsTransitive(st, stCombined, stExec);

+            } else { }

+          } else { }

+        } else { }

+      } else { }

+    } else { }

+  }

+

+  lemma EvalArgsLemma(context: Expression, args: seq<Expression>, stOrig: State, env: Env) returns (args': seq<Expression>, sts': set<State>)

+    requires

+      ValidState(stOrig) && ValidEnv(env) &&

+      forall arg :: arg in args ==> arg < context;

+    ensures

+      Pair(args', sts') == evalArgs(context, args, stOrig, env) &&

+      forall st' :: st' in sts' ==> ValidState(st') && Extends(stOrig, st');

+    decreases context, |args|;

+  {

+    if args == [] {

+      args', sts' := [], {};

+    } else {

+      var rArg, rSts := EvalLemma(args[0], stOrig, env);

+      var rrArg, rrSts := EvalArgsLemma(context, args[1..], stOrig, env);

+      args', sts' := [rArg] + rrArg, {rSts} + rrSts;

+    }

+  }

+} // module M0

+

+abstract module M1 refines M0 {

+  datatype State = StateCons(m: map<Path, Artifact>)

+

+  function GetSt(p: Path, st: State): Artifact

+  {

+    st.m[p]

+  }

+

+  function DomSt(st: State): set<Path>

+    ensures forall p :: p in DomSt(st) ==> p in st.m;

+  {

+    set p | p in st.m

+  }

+

+  // A tiny test harness, just to show that it is possible to call build(...)

+  ghost method Main()

+  {

+    var calcC: string, calcH: Path, calcObj: string;

+    var cmd := exprLiteral(litString(calcC));

+    var deps := exprLiteral(litArrOfPaths({calcH}));

+    var exps := exprLiteral(litArrOfStrings({calcObj}));

+    var exec := exprInvocation(exprLiteral(litPrimitive(primExec)), [cmd, deps, exps]);

+

+    var h;

+    var st := StateCons(map[calcH := h]);

+

+    assert calcH != Loc(calcC, {calcH}, calcObj) ==> ValidArgs(primExec, exec.args, st);

+

+    var program := Program.Program([stmtReturn(exec)]);

+    var result := build(program, st);

+    var e, st' := result.fst, result.snd;

+  }

+}

+

+// This module does the heavy lifting of the consistency proof.

+abstract module M2 refines M1 {

+  function SetSt(p: Path, a: Artifact, st: State): State

+  {

+    StateCons(st.m[p := a])

+  }

+

+  function Restrict(paths: set<Path>, st: State): map<Path, Artifact>

+  {

+    map p | p in paths && p in DomSt(st) :: GetSt(p, st)

+  }

+  lemma RestrictMonotonicity(paths: set<Path>, st0: State, st1: State)

+    requires paths <= DomSt(st0) && Extends(st0, st1);

+    ensures Restrict(paths, st0) == Restrict(paths, st1);

+  {

+  }

+

+  function PickOne<T>(s: set<T>): T

+    requires s != {};

+  {

+    var x :| x in s; x

+  }

+

+  predicate WellFounded(p: Path)

+  {

+    exists cert :: CheckWellFounded(p, cert)

+  }

+  predicate CheckWellFounded(p: Path, cert: WFCertificate)

+    decreases cert;

+  {

+    cert.p == p &&

+    (forall d :: d in LocInv_Deps(p) ==> exists c :: c in cert.certs && c.p == d) &&

+    (forall c :: c in cert.certs ==> CheckWellFounded(c.p, c))

+  }

+  datatype WFCertificate = Cert(p: Path, certs: set<WFCertificate>)

+

+

+  // We take as a given the existence of a function that carries out the work of "exec".

+  // Instead of reading the system state directly and restricting such reads to the

+  // given set of dependencies, "RunTool" is not given the whole system state but only

+  // a part of it, namely the part that has artifacts for the declared dependencies.

+  function RunTool(cmd: string, deps: map<Path, Artifact>, exp: string): Artifact

+

+  function exec(cmd: string, deps: set<Path>, exps: set<string>, st: State): Tuple<set<Path>, State>

+  {

+    execOne(cmd, deps, Restrict(deps, st), exps, st)

+  }

+  function execOne(cmd: string, deps: set<Path>, restrictedState: map<Path, Artifact>, exps: set<string>, st: State): Tuple<set<Path>, State>

+  {

+    if exps == {} then

+      Pair({}, st)

+    else

+      var exp := PickOne(exps);

+      var Pair(paths, st') := execOne(cmd, deps, restrictedState, exps - {exp}, st);

+      var p := Loc(cmd, deps, exp);

+      Pair(paths + {p}, if p in DomSt(st') then st' else SetSt(p, RunTool(cmd, restrictedState, exp), st'))

+  }

+

+  lemma ExecProperty(cmd: string, deps: set<Path>, exps: set<string>, st: State)

+  {

+    ExecOneProperty(cmd, deps, Restrict(deps, st), exps, st);

+  }

+  lemma ExecOneProperty(cmd: string, deps: set<Path>, restrictedState: map<Path, Artifact>, exps: set<string>, st: State)

+    requires

+      ValidState(st) &&

+      deps <= DomSt(st) &&

+      Pre(cmd, deps, exps, st) &&

+      restrictedState == Restrict(deps, st);

+    ensures

+      var result'' := execOne(cmd, deps, restrictedState, exps, st);

+      var paths'', st'' := result''.fst, result''.snd;

+      ValidState(st'') &&

+      Extends(st, st'') &&

+      OneToOne(cmd, deps, exps, paths'') &&

+      Post(cmd, deps, exps, st'');

+  {

+    if exps == {} {

+    } else {

+      var exp := PickOne(exps);

+      var rest := execOne(cmd, deps, restrictedState, exps - {exp}, st);

+      var paths, st' := rest.fst, rest.snd;

+      var p := Loc(cmd, deps, exp);

+      var a := RunTool(cmd, restrictedState, exp);

+      var paths'', st'' := paths + {p}, if p in DomSt(st') then st' else SetSt(p, a, st');

+      ExecOneProperty(cmd, deps, restrictedState, exps - {exp}, st);

+      assert execOne(cmd, deps, restrictedState, exps, st).snd == st'';

+

+      calc ==> {

+        true;

+        { LocInjectivity(cmd, deps, exp); }

+        LocInv_Deps(p) == deps;

+        { ExecOne_Lemma0(p); }

+        WellFounded(p);

+        ValidState(st'');

+      }

+

+      forall

+        ensures Extends(st', st'') && Extends(st, st'');

+      {

+        LocInjectivity(cmd, deps, exp);

+        if p !in DomSt(st') {

+          calc {

+            a;

+            // def. a

+            RunTool(cmd, restrictedState, exp);

+            // def. restrictedState

+            RunTool(cmd, Restrict(deps, st), exp);

+            { RestrictMonotonicity(deps, st, st'); }

+            RunTool(cmd, Restrict(deps, st'), exp);

+            { CollectRestrict_Lemma(p, GetCert(p), deps, st'); }

+            RunTool(cmd, CollectDependencies(p, GetCert(p), deps, st'), exp);

+            // we use LocInjectivity here

+            RunTool(LocInv_Cmd(p), CollectDependencies(p, GetCert(p), LocInv_Deps(p), st'), LocInv_Exp(p));

+            // def. OracleWF

+            OracleWF(p, GetCert(p), st');

+            { assert WellFounded(p); }

+            Oracle(p, st');

+          }

+        }

+        assert Extends(st', st'');

+        Lemma_ExtendsTransitive(st, st', st'');

+      }

+

+      assert OneToOne(cmd, deps, exps, paths'');

+

+      forall e | e in exps

+        ensures Loc(cmd, deps, e) in DomSt(st'') && GetSt(Loc(cmd, deps, e), st'') == Oracle(Loc(cmd, deps, e), st'');

+      {

+        var p := Loc(cmd, deps, e);

+        assert p in DomSt(st'');

+        if p in DomSt(st') {

+          calc {

+            GetSt(p, st'');

+            { assert p in DomSt(st') && Extends(st', st''); }

+            GetSt(p, st');

+            // (I don't fully understand this step, but evidently Dafny can do it)

+            Oracle(p, st);

+            { OracleProperty(p, st, st''); }

+            Oracle(p, st'');

+          }

+        } else {

+          calc {

+            GetSt(p, st'');

+            RunTool(cmd, restrictedState, exp);

+            RunTool(cmd, Restrict(deps, st), exp);

+            // ?  -- I'm amazed!  How can it prove this step automatically?

+            Oracle(p, st);

+            { OracleProperty(p, st, st''); }

+            Oracle(p, st'');

+          }

+        }

+      }

+    }

+  }

+  lemma ExecOne_Lemma0(p: Path)

+    requires forall d :: d in LocInv_Deps(p) ==> WellFounded(d);

+    ensures WellFounded(p);

+  {

+    var certs := set d | d in LocInv_Deps(p) :: GetCert(d);

+    assert CheckWellFounded(p, Cert(p, certs));

+  }

+  function GetCert(p: Path): WFCertificate

+    requires WellFounded(p);

+    ensures CheckWellFounded(p, GetCert(p));

+  {

+    var c :| CheckWellFounded(p, c);

+    c

+  }

+

+  // Loc is injective.  Here are its inverse functions:

+  function LocInv_Cmd(p: Path): string

+  function LocInv_Deps(p: Path): set<Path>

+  function LocInv_Exp(p: Path): string

+  lemma LocInjectivity(cmd: string, deps: set<Path>, exp: string)

+    ensures LocInv_Cmd(Loc(cmd, deps, exp)) == cmd;

+    ensures LocInv_Deps(Loc(cmd, deps, exp)) == deps;

+    ensures LocInv_Exp(Loc(cmd, deps, exp)) == exp;

+

+  function Oracle(p: Path, st: State): Artifact

+  {

+    if WellFounded(p) then OracleWF(p, GetCert(p), st) else OracleArbitrary(p)

+  }

+  function OracleArbitrary(p: Path): Artifact

+  {

+    var a :| true;

+    a  // return an arbitrary artifact (note, the same "a" will be used for every call to function OracleArbitrary(p) for the same "p")

+  }

+  function OracleWF(p: Path, cert: WFCertificate, st: State): Artifact

+    requires CheckWellFounded(p, cert);

+    decreases cert, 1;

+  {

+    var cmd, deps, e := LocInv_Cmd(p), LocInv_Deps(p), LocInv_Exp(p);

+    RunTool(cmd, CollectDependencies(p, cert, deps, st), e)

+  }

+  function CollectDependencies(p: Path, cert: WFCertificate, deps: set<Path>, st: State): map<Path, Artifact>

+    requires CheckWellFounded(p, cert) && deps == LocInv_Deps(p);

+    decreases cert, 0;

+  {

+    map d | d in deps :: if d in DomSt(st) then GetSt(d, st) else OracleWF(d, FindCert(d, cert.certs), st)

+  }

+  function FindCert(d: Path, certs: set<WFCertificate>): WFCertificate

+    requires exists c :: c in certs && c.p == d;

+  {

+    var c :| c in certs && c.p == d;

+    c

+  }

+

+  // A well-founded path has a certificate, but certificates are not unique.  However, OracleWF gives the same value

+  // for any cerificate for the path.

+  lemma OracleWF_CertificateInsensitivity(p: Path, cert0: WFCertificate, cert1: WFCertificate, st: State)

+    requires CheckWellFounded(p, cert0) && CheckWellFounded(p, cert1);

+    ensures OracleWF(p, cert0, st) == OracleWF(p, cert1, st);

+    decreases cert0, 1;

+  {

+    Collect_CertificateInsensitivity(p, cert0, cert1, LocInv_Deps(p), st);

+  }

+  lemma Collect_CertificateInsensitivity(p: Path, cert0: WFCertificate, cert1: WFCertificate, deps: set<Path>, st: State)

+    requires CheckWellFounded(p, cert0) && CheckWellFounded(p, cert1) && deps == LocInv_Deps(p);

+    ensures CollectDependencies(p, cert0, deps, st) == CollectDependencies(p, cert1, deps, st);

+    decreases cert0, 0;

+  {

+    forall d | d in deps { OracleWF_CertificateInsensitivity(d, FindCert(d, cert0.certs), FindCert(d, cert1.certs), st); }

+  }

+

+  lemma CollectRestrict_Lemma(p: Path, cert: WFCertificate, deps: set<Path>, st: State)

+    requires ValidState(st) && deps <= DomSt(st);

+    requires CheckWellFounded(p, cert) && deps == LocInv_Deps(p);

+    ensures CollectDependencies(p, cert, deps, st) == Restrict(deps, st);

+  {

+    var a, b := CollectDependencies(p, cert, deps, st), Restrict(deps, st);

+    assert (set q | q in a) == deps == (set q | q in b);

+    forall d | d in deps

+      ensures a[d] == b[d];

+    {

+      calc {

+        a[d];

+        if d in DomSt(st) then GetSt(d, st) else OracleWF(d, FindCert(d, cert.certs), st);

+        { assert d in DomSt(st); }

+        GetSt(d, st);

+        b[d];

+      }

+    }

+  }

+

+  lemma OracleProperty(p: Path, st0: State, st1: State)

+    // This is the inherited specification:

+    // requires Extends(st0, st1);

+    // ensures Oracle(p, st0) == Oracle(p, st1);

+  {

+    if !WellFounded(p) {

+      // trivial

+    } else {

+      var cert := GetCert(p);

+      OracleWF_Property(p, cert, st0, st1);

+    }

+  }

+  lemma OracleWF_Property(p: Path, cert: WFCertificate, st0: State, st1: State)

+    requires Extends(st0, st1) && CheckWellFounded(p, cert);

+    ensures OracleWF(p, cert, st0) == OracleWF(p, cert, st1);

+    decreases cert, 1;

+  {

+    var cmd, deps, e := LocInv_Cmd(p), LocInv_Deps(p), LocInv_Exp(p);

+    CollectProperty(p, cert, deps, st0, st1);

+  }

+  lemma CollectProperty(p: Path, cert: WFCertificate, deps: set<Path>, st0: State, st1: State)

+    requires Extends(st0, st1) && CheckWellFounded(p, cert) && deps == LocInv_Deps(p);

+    ensures CollectDependencies(p, cert, deps, st0) == CollectDependencies(p, cert, deps, st1);

+    decreases cert, 0;

+  {

+    forall d | d in deps

+      ensures (if d in DomSt(st0) then GetSt(d, st0) else OracleWF(d, FindCert(d, cert.certs), st0)) ==

+              (if d in DomSt(st1) then GetSt(d, st1) else OracleWF(d, FindCert(d, cert.certs), st1));

+    {

+      if d in DomSt(st0) {

+        assert d in DomSt(st1);

+      } else if d in DomSt(st1) {

+        calc {

+          if d in DomSt(st0) then GetSt(d, st0) else OracleWF(d, FindCert(d, cert.certs), st0);

+          OracleWF(d, FindCert(d, cert.certs), st0);

+          { // any certificate is as good as any other

+            OracleWF_CertificateInsensitivity(d, FindCert(d, cert.certs), GetCert(d), st0);

+          }

+          OracleWF(d, GetCert(d), st0);

+          { assert WellFounded(d); }

+          if WellFounded(d) then OracleWF(d, GetCert(d), st0) else OracleArbitrary(d);

+          Oracle(d, st0);

+          { assert Extends(st0, st1); }

+          GetSt(d, st1);

+          if d in DomSt(st1) then GetSt(d, st1) else OracleWF(d, FindCert(d, cert.certs), st1);

+        }

+      } else {

+        OracleWF_Property(d, FindCert(d, cert.certs), st0, st1);

+      }

+    }

+  }

+}

+

+// Finally, this module defines any remaining arbitrary types and function bodies and proves any

+// remaining lemmas about these.  The actual definitions are not so interesting and are not meant

+// to suggest that a deployed CloudMake use these definitions.  Rather, these definitions are here

+// only to establish mathematical feasibility of previously axiomatized properties.

+module M3 refines M2 {

+  function Union(st: State, st': State): State

+  {

+    StateCons(map p | p in DomSt(st) + DomSt(st') :: GetSt(p, if p in DomSt(st) then st else st'))

+  }

+

+  function RunTool(cmd: string, deps: map<Path, Artifact>, exp: string): Artifact

+  {

+    // return an arbitrary artifact

+    var a :| true;

+    a

+  }

+

+  datatype string = stringCons(int)

+  datatype Artifact = ArtifactCons(int)

+  datatype Identifier = IdentifierCons(int)

+

+  datatype Path =

+    InternalPath(cmd: string, deps: set<Path>, exp: string) |

+    ExternalPath(string)

+  function createPath(fn: string): Path

+  {

+    ExternalPath(fn)

+  }

+  lemma PathProperty(fn: string, fn': string)

+  {

+  }

+  function Loc(cmd: string, deps: set<Path>, exp: string): Path

+  {

+    InternalPath(cmd, deps, exp)

+  }

+  function LocInv_Cmd(p: Path): string

+  {

+    match p

+    case InternalPath(cmd, deps, exp) => cmd

+    case ExternalPath(_) => var cmd :| true; cmd

+  }

+  function LocInv_Deps(p: Path): set<Path>

+  {

+    match p

+    case InternalPath(cmd, deps, exp) => deps

+    case ExternalPath(_) => var deps :| true; deps

+  }

+  function LocInv_Exp(p: Path): string

+  {

+    match p

+    case InternalPath(cmd, deps, exp) => exp

+    case ExternalPath(_) => var exp :| true; exp

+  }

+  lemma LocInjectivity(cmd: string, deps: set<Path>, exp: string)

+  {

+  }

+

+  datatype Env = EnvCons(m: map<Identifier, Expression>)

+  function EmptyEnv(): Env

+  {

+    EnvCons(map[])

+  }

+  function GetEnv(id: Identifier, env: Env): Expression

+  {

+    if id in env.m then env.m[id] else var lit :| true; exprLiteral(lit)

+  }

+  function SetEnv(id: Identifier, expr: Expression, env: Env): Env

+  {

+    EnvCons(env.m[id := expr])

+  }

+  predicate ValidEnv(env: Env)

+  {

+    forall id :: id in env.m ==> Value(env.m[id])

+  }

+}

diff --git a/Test/cloudmake/runtest.bat b/Test/cloudmake/runtest.bat
new file mode 100644
index 00000000..8fc7ccbb
--- /dev/null
+++ b/Test/cloudmake/runtest.bat
@@ -0,0 +1,7 @@
+@echo off

+setlocal

+

+set BINARIES=..\..\Binaries

+set DAFNY_EXE=%BINARIES%\Dafny.exe

+

+%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy