From efc11762c9d697aef9eae0cebd1d17aaf229d2a8 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 28 Feb 2014 18:29:55 -0800 Subject: Moved the (long running) CloudMake test files to their own directory --- Test/cloudmake/Answer | 12 + Test/cloudmake/CloudMake-CachedBuilds.dfy | 1321 +++++++++++++++++++++++++ Test/cloudmake/CloudMake-ConsistentBuilds.dfy | 660 ++++++++++++ Test/cloudmake/CloudMake-ParallelBuilds.dfy | 835 ++++++++++++++++ Test/cloudmake/runtest.bat | 7 + 5 files changed, 2835 insertions(+) create mode 100644 Test/cloudmake/Answer create mode 100644 Test/cloudmake/CloudMake-CachedBuilds.dfy create mode 100644 Test/cloudmake/CloudMake-ConsistentBuilds.dfy create mode 100644 Test/cloudmake/CloudMake-ParallelBuilds.dfy create mode 100644 Test/cloudmake/runtest.bat (limited to 'Test/cloudmake') diff --git a/Test/cloudmake/Answer b/Test/cloudmake/Answer new file mode 100644 index 00000000..3758853e --- /dev/null +++ b/Test/cloudmake/Answer @@ -0,0 +1,12 @@ + +-------------------- CloudMake-ParallelBuilds.dfy -------------------- + +Dafny program verifier finished with 244 verified, 0 errors + +-------------------- CloudMake-CachedBuilds.dfy -------------------- + +Dafny program verifier finished with 104 verified, 0 errors + +-------------------- CloudMake-ConsistentBuilds.dfy -------------------- + +Dafny program verifier finished with 59 verified, 0 errors diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy new file mode 100644 index 00000000..f1150809 --- /dev/null +++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy @@ -0,0 +1,1321 @@ +// This module proves the correctness of the algorithms. It leaves a number of things undefined. +// They are defined in refinement modules below. +abstract module M0 { + /******* State *******/ + type State + function DomSt(st: State): set + function GetSt(p: Path, st: State): Artifact + requires p in DomSt(st); + + // cached part of state + type HashValue + function DomC(st: State): set + 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, exps: set, 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) + { + 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) + requires forall s :: s in sts ==> Extends(stOrig, s); + ensures Compatible(sts); + { + reveal_Extends(); + } + + function {:opaque} Combine(sts: set, useCache: bool): State + requires sts != {}; + { + var st := PickOne(sts); + if sts == {st} then + st + else + Union(Combine(sts - {st}, useCache), st, useCache) + } + function PickOne(s: set): T + requires s != {}; + { + var x :| x in s; x + } + + lemma Lemma_Combine(sts: set, 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, exps: set, st: State): Tuple, State> + + lemma ExecProperty(cmd: string, deps: set, exps: set, 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, exps: set, 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, exps: set, paths: set) + { + // 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, exps: set, 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, exps: set, 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, exps: set, stC: State): Tuple, 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) + + 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) | + 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) | + litArrOfStrings(strs: set) | + litArray(arr: seq) + + datatype Primitive = primCreatePath | primExec + + datatype Reason = rCompatibility | rValidity | rInconsistentCache + + type Path(==) + function Loc(cmd: string, deps: set, exp: string): Path + + type string(==) + type Artifact + type Identifier + + datatype Tuple = Pair(fst: A, snd: B) + datatype Triple = 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 + requires Legal(prog.stmts); + { + do(prog.stmts, st, EmptyEnv(), useCache) + } + + /******* Function 'do' *******/ + function do(stmts: seq, st: State, env: Env, useCache: bool): Tuple + 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) + { + |stmts| != 0 + } + + /******* Function 'eval' *******/ + function {:opaque} eval(expr: Expression, st: State, env: Env, useCache: bool): Tuple + 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, set> + 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, set>, pC: Triple, set>) + 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, set>, pC: Triple, set>) + 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) + 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 + 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, fun: Expression, args: seq, useCache: bool): Tuple + 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, useCache: bool): Tuple + { + 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, stOrig: State, env: Env, useCache: bool): + Tuple, set> + 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, 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, 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, stOrig: State, env: Env, useCache: bool) + returns (exprs: seq, sts: set) + 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, 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, stOrigC: State, stsC: set, fun: Expression, args: seq) + 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, st: State, sts'': set, + pC: Tuple, stC: State, stsC'': set, + fun: Expression, args: seq) + 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, st: State, stCombined: State, + pC: Tuple, stC: State, stCombinedC: State, + fun: Expression, args: seq) + 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, stOrig: State, stOrigC: State, env: Env) + returns (exprs: seq, sts: set, stsC: set) + 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): set + { + if sts == {} then {} else + var st := PickOne(sts); DomSt(st) + DomSt_Union(sts - {st}) + } + lemma Combine_DomSt_X(sts: set, useCache: bool) + requires sts != {}; + ensures DomSt(Combine(sts, useCache)) == DomSt_Union(sts); + { + reveal_Combine(); + } + lemma DomSt_Union_Cons(st: State, sts: set) + 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, 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, stC: State, stsC: set) + 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, 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, 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, useCache: bool) + requires st in sts; + ensures p in DomSt(st) ==> p in DomSt(Combine(sts, useCache)); + { + reveal_Combine(); + } + +} // module M0 diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy new file mode 100644 index 00000000..dcfa1a2b --- /dev/null +++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy @@ -0,0 +1,660 @@ +/******* State *******/ +type State + +function GetSt(p: Path, st: State): Artifact +function SetSt(p: Path, a: Artifact, st: State): State + +function DomSt(st: State): set + +function Restrict(paths: set, 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 +function SetC(h: HashValue, cmd: Triple, 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 + requires ss != {}; +{ + var s :| s in ss; s +} + +function DomC(c: Cache): set + +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) +{ + 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 + 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) + 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 + +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 + 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) + +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) | + exprError(r: Reason) + +datatype Literal = litTrue | litFalse | litUndefined | litNull | + litNumber(num: int) | litString(str: string) | + litPrimitive(prim: Primitive) | + litArrOfPaths(paths: set) | + litArrOfStrings(strs: set) | + litArray(arr: seq) + +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 = Pair(fst: A, snd: B) +datatype Triple = Trio(fst: A, snd: B, trd: C) + +/******* Values *******/ +predicate Value(expr: Expression) +{ + expr.exprLiteral? +} + +/******* Semantics *******/ + +predicate Legal(stmts: seq) +{ + |stmts| != 0 +} + +function Arity(prim: Primitive): nat +{ + match prim + case primCreatePath => 1 + case primExec => 3 +} + +/******* Function 'buildC' *******/ +function buildC(prog: Program, stC: StateC): Tuple + requires Legal(prog.stmts); +{ + doC(prog.stmts, stC, EmptyEnv()) +} + +/******* Function 'doC' *******/ +function doC(stmts: seq, stC: StateC, env: Env): Tuple + 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 + 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, stC: StateC, env: Env): + Tuple, set> + requires forall arg :: arg in args ==> arg < expr; + decreases expr, |args| + 1; + +{ + evalArgsC'(expr, args, stC, env, [], {}) +} + +function evalArgsC'(expr: Expression, args: seq, stC: StateC, env: Env, + args': seq, stsC': set): + Tuple, set> + 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, 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, 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, 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, stC: StateC, env: Env, + args': seq, stsC': set) + requires ConsistentCache(stC); + requires forall stC' :: stC' in stsC' ==> ConsistentCache(stC'); + requires forall arg :: arg in args ==> arg < expr; + ensures + var result := evalArgsC'(expr, args, stC, env, args', stsC'); + var stsC'' := result.snd; + forall stC'' :: stC'' in stsC'' ==> ConsistentCache(stC''); + decreases expr, |args|; +{ + if args == [] { + } else { + var arg := args[0]; + EvalCLemma(arg, stC, env); + var result := evalC(arg, stC, env); + var arg', stC' := result.fst, result.snd; + EvalArgsC'Lemma(expr, args[1..], stC, env, args' + [arg'], stsC' + {stC'}); + } +} \ No newline at end of file diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy new file mode 100644 index 00000000..e76f60d8 --- /dev/null +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy @@ -0,0 +1,835 @@ +// This module proves the correctness of the algorithms. It leaves a number of things undefined. +// They are defined in refinement modules below. +abstract module M0 { + /******* State *******/ + type State + function DomSt(st: State): set + 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) + { + 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 + requires sts != {}; + { + var st :| st in sts; + if sts == {st} then + st + else + Union(st, Combine(sts - {st})) + } + lemma Lemma_Combine(sts: set, 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, exps: set, st: State): Tuple, State> + + lemma ExecProperty(cmd: string, deps: set, exps: set, 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, exps: set, 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, exps: set, paths: set) + { + forall e :: e in exps ==> Loc(cmd, deps, e) in paths + } + + predicate Post(cmd: string, deps: set, exps: set, 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) + + 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) | + 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) | + litArrOfStrings(strs: set) | + litArray(arr: seq) + + datatype Primitive = primCreatePath | primExec + + datatype Reason = rCompatibility | rValidity + + type Path(==) + function Loc(cmd: string, deps: set, exp: string): Path + + type string(==) + type Artifact + type Identifier + + datatype Tuple = Pair(fst: A, snd: B) + + /******* Values *******/ + predicate Value(expr: Expression) + { + expr.exprLiteral? + } + + /******* Semantics *******/ + + /******* Function 'build' *******/ + function build(prog: Program, st: State): Tuple + requires Legal(prog.stmts); + { + do(prog.stmts, st, EmptyEnv()) + } + + /******* Function 'do' *******/ + function do(stmts: seq, st: State, env: Env): Tuple + 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) + { + |stmts| != 0 + } + + /******* Function 'eval' *******/ + function eval(expr: Expression, st: State, env: Env): Tuple + 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, stOrig: State, env: Env): Tuple, set> + 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, 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, 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, stOrig: State, env: Env) returns (args': seq, sts': set) + 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) + + function GetSt(p: Path, st: State): Artifact + { + st.m[p] + } + + function DomSt(st: State): set + 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, st: State): map + { + map p | p in paths && p in DomSt(st) :: GetSt(p, st) + } + lemma RestrictMonotonicity(paths: set, st0: State, st1: State) + requires paths <= DomSt(st0) && Extends(st0, st1); + ensures Restrict(paths, st0) == Restrict(paths, st1); + { + } + + function PickOne(s: set): 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) + + + // 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, exp: string): Artifact + + function exec(cmd: string, deps: set, exps: set, st: State): Tuple, State> + { + execOne(cmd, deps, Restrict(deps, st), exps, st) + } + function execOne(cmd: string, deps: set, restrictedState: map, exps: set, st: State): Tuple, 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, exps: set, st: State) + { + ExecOneProperty(cmd, deps, Restrict(deps, st), exps, st); + } + lemma ExecOneProperty(cmd: string, deps: set, restrictedState: map, exps: set, 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 + function LocInv_Exp(p: Path): string + lemma LocInjectivity(cmd: string, deps: set, 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, st: State): map + 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 + 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, 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, 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, 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, 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, exp: string) | + ExternalPath(string) + function createPath(fn: string): Path + { + ExternalPath(fn) + } + lemma PathProperty(fn: string, fn': string) + { + } + function Loc(cmd: string, deps: set, 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 + { + 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, exp: string) + { + } + + datatype Env = EnvCons(m: map) + function EmptyEnv(): Env + { + EnvCons(map[]) + } + function GetEnv(id: Identifier, env: Env): Expression + { + if id in env.m then env.m[id] else var lit :| true; exprLiteral(lit) + } + function SetEnv(id: Identifier, expr: Expression, env: Env): Env + { + EnvCons(env.m[id := expr]) + } + predicate ValidEnv(env: Env) + { + forall id :: id in env.m ==> Value(env.m[id]) + } +} diff --git a/Test/cloudmake/runtest.bat b/Test/cloudmake/runtest.bat new file mode 100644 index 00000000..8fc7ccbb --- /dev/null +++ b/Test/cloudmake/runtest.bat @@ -0,0 +1,7 @@ +@echo off +setlocal + +set BINARIES=..\..\Binaries +set DAFNY_EXE=%BINARIES%\Dafny.exe + +%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CloudMake-ParallelBuilds.dfy CloudMake-CachedBuilds.dfy CloudMake-ConsistentBuilds.dfy -- cgit v1.2.3