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

1 files changed, 835 insertions, 0 deletions

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])

+  }

+}