diff options
Diffstat (limited to 'Test/dafny4')
| -rw-r--r-- | Test/dafny4/Answer | 12 | ||||
| -rw-r--r-- | Test/dafny4/CloudMake-CachedBuilds.dfy | 1321 | ||||
| -rw-r--r-- | Test/dafny4/CloudMake-ConsistentBuilds.dfy | 660 | ||||
| -rw-r--r-- | Test/dafny4/CloudMake-ParallelBuilds.dfy | 835 | ||||
| -rw-r--r-- | Test/dafny4/runtest.bat | 2 |
5 files changed, 2829 insertions, 1 deletions
diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer index 61eedf16..4a09a1d8 100644 --- a/Test/dafny4/Answer +++ b/Test/dafny4/Answer @@ -33,3 +33,15 @@ Dafny program verifier finished with 33 verified, 0 errors -------------------- Circ.dfy --------------------
Dafny program verifier finished with 16 verified, 0 errors
+
+-------------------- 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/dafny4/CloudMake-CachedBuilds.dfy b/Test/dafny4/CloudMake-CachedBuilds.dfy new file mode 100644 index 00000000..f1150809 --- /dev/null +++ b/Test/dafny4/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/dafny4/CloudMake-ConsistentBuilds.dfy b/Test/dafny4/CloudMake-ConsistentBuilds.dfy new file mode 100644 index 00000000..dcfa1a2b --- /dev/null +++ b/Test/dafny4/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/dafny4/CloudMake-ParallelBuilds.dfy b/Test/dafny4/CloudMake-ParallelBuilds.dfy new file mode 100644 index 00000000..e76f60d8 --- /dev/null +++ b/Test/dafny4/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/dafny4/runtest.bat b/Test/dafny4/runtest.bat index c6778179..ea4869db 100644 --- a/Test/dafny4/runtest.bat +++ b/Test/dafny4/runtest.bat @@ -4,4 +4,4 @@ setlocal set BINARIES=..\..\Binaries
set DAFNY_EXE=%BINARIES%\Dafny.exe
-%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy
+%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy
|