Skip to content

Commit

Permalink
Add comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@xumingkuan
xumingkuan committed Aug 24, 2023
1 parent 090a2cc commit 805ca73
Show file tree
Hide file tree
Showing 3 changed files with 62 additions and 18 deletions.
5 changes: 5 additions & 0 deletions TypeInjections/TypeInjections/Resources/MapBuiltinTypes.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,11 @@ module Translations.MapBuiltinTypes {
}

module Translations.Utils {
/* We requires false here because Dafny 4 does not allow non-determinism like ":|" in functions.
* This function is to convert name resolution errors in stubs generated in translation functions
* to verification errors (cannot prove false), so Dafny will not stop verifying the entire program
* when it sees "???".
*/
function ???<X(0)>(): X
requires false
{
Expand Down
42 changes: 25 additions & 17 deletions TypeInjections/TypeInjections/Translation.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -321,7 +321,7 @@ module Translation =
translationCondition (fst f1) (fst f2) inO inN, snd f1)
(List.zip3 insT insO insN)
and lossless (tO: Type) (tT: (Expr -> Expr) * (Expr -> Expr)) : Condition =
// forall x1_O: U_O :: U_back(U(x1_O)) == x1_O
// forall x1_O: U_O :: U_backward(U_forward(x1_O)) == x1_O
let nO, _, _ = name "x"
let ld = LocalDecl(nO, tO, true)
EQuant(Forall, [ ld ], None, EEqual((snd tT) ((fst tT) (EVar nO)), EVar nO)), None
Expand Down Expand Up @@ -799,29 +799,37 @@ module Translation =
ctxNi.add(outsD.namedDecls.getNew ()).enterBody ()
// we ignore changes in in/output conditions here and only compare declarations
// in fact, ensures clauses (no matter if changed) are ignored entirely
(*if not (insD.decls.getUpdate().IsEmpty) then
failwith (
unsupported "update to individual inputs: "
+ p.ToString()
)
if not outsD.decls.isSame then
failwith (unsupported "change in outputs: " + p.ToString())*)
// if modifies, reads, decreases clauses change, throw an error
// TODO here
// we ignore changes in modifies, reads, decreases clauses
//
// as "methods", we only consider pure functions here
// a more general approach might also generate two-state lemmas for method invocations on class instances
// (i.e., calling corresponding methods with related arguments on related objects yields related values and
// leaves the (possibly changed) objects related)
//
// For a static method without specification:
// method p<u,v>(x:a,y:u,z:u->v):B = {_} --->
// lemma p<uO,uN,vO,vN>(uT:uO->uN, uT_back:uN->uO, vT:vO->vN, xO:aO, xN:aN, yO:uO, yN:uN, zO:uO->vO, zN:uN->vN))
// requires xN==aT(xO)
// requires yN==uT(yO)
// requires ((x1_N:uN) => vT(zO(uT_back(x1_N)))) == zN
// ensures pN(xN,uN)==BT(pO(xO,uO))
// method p<u,v>(x:a,y:u,z:u->v):B
// requires some_property(x)
// { ... }
// --->
// lemma p_bc<uO,uN,vO,vN>(u_forward:uO->uN, u_backward:uN->uO, v_forward:vO->vN, v_backward: vN->vO,
// xO:aO, xN:aN, yO:uO, yN:uN, zO:uO->vO, zN:uN->vN)
// requires some_property(xO)
// requires xN == a_forward(xO)
// requires yN == u_forward(yO)
// (either) requires forall x1_N: uN :: zN(x1_N) == v_forward(zO(u_backward(x1_N))
// (or) requires zN == ((x1_N:uN) => v_forward(zO(u_backward(x1_N))))
// ensures some_property(xN)
// ensures New.p(xN,uN)==B_forward(Old.p(xO,uO))
// and accordingly for the general case. If not static, the lemma additionally quantifies over the receivers.
//
// We change "requires some_property(xN)" to "ensures some_property(xN)" because
// we can easily prove false if we have "requires some_property(xO)", "requires some_property(xN)",
// "requires xN == a_forward(xO)", and a "slightly incorrect" function "a_forward".
// The function "a_forward" should be enough for proving "ensures some_property(xN)" from
// the precondition "requires some_property(xN)".
// The reason why we want to explicitly state this postcondition is we need to prove it when calling
// New.p(xN,uN) anyway, and Dafny sometimes cannot prove the precondition of New.p(xN,uN) if we
// did not state the postcondition explicitly.
let parentDeclO = contextO.lookupCurrent ()

let parentDeclN = contextN.lookupCurrent ()
Expand Down
33 changes: 32 additions & 1 deletion TypeInjections/TypeInjections/YIL.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -613,6 +613,16 @@ module YIL =
| ETypeTest of Expr * Type
// *** control flow etc.
| EBlock of exprs: Expr list
(* let expressions
var x1,...,xn := V1,...,Vn; body
var x1,...,xn := V; body (if V is call to a method with n outputs)
Note that ":=" can be replaced with ":-" (when orfail is true) or ":|" (when exact is false)
Similar to EDecls. Consider also using UpdateRHS here?
Each x on the LHS can be a case pattern.
In LHS, "(x, y)" is one case pattern (ETuple) expecting a function call on RHS
but "x, y" are two variables (EVar, EVar) expecting two values on RHS.
In all cases, "vars" stores all local variables visible in the body.
*)
| ELet of vars: LocalDecl list * exact: bool * orfail: bool * lhs: Expr list * df: Expr list * body: Expr // not exact = non-deterministic
| EIf of cond: Expr * thn: Expr * els: Expr option // cond must not have side-effects; els non-optional if this is an expression; see also flattenIf
| EAlternative of conds: Expr list * bodies: Expr list // if case cond1 => body1 case cond2 => body2
Expand All @@ -627,6 +637,9 @@ module YIL =
In the former case, x1 may not occur in V2.
The latter is at most needed before ghosts are eliminated because we allow only one non-ghost output.
Note that ":=" can be replaced with ":-" or ":|" (see UpdateRHS).
Each x on the LHS can be a case pattern.
In LHS, "(x, y)" is one case pattern (ETuple) expecting a function call on RHS
but "x, y" are two variables (EVar, EVar) expecting two values on RHS.
In all cases, "vars" stores all local variables visible after this statement.
*)
| EDecls of vars: LocalDecl list * lhs: Expr list * rhs: UpdateRHS list
Expand All @@ -637,6 +650,10 @@ module YIL =
Dafny allows an omitted lhs, in which case this is just an expression;
in particular, lemma calls are represented that way; because we merge statements and expressions,
we do not need a special case for that.
Each x on the LHS can be a case pattern.
In LHS, "(x, y)" is one case pattern (ETuple) expecting a function call on RHS
but "x, y" are two variables (EVar, EVar) expecting two values on RHS.
In all cases, "vars" stores all local variables visible after this statement.
*)
| EUpdate of name: Expr list * UpdateRHS
| EPrint of exprs: Expr list
Expand Down Expand Up @@ -1507,6 +1524,7 @@ module YIL =
// but we need to add parentheses if we encounter "<" (with precedence 4).
//
// expr 0 e: no need to add parentheses
// expr 1 e: add parentheses to lemma call expressions (lemma_call(); expr)
// expr 11 e: add parentheses unless it's a primary expression, e.g., EVar
let expr p e = this.exprWithPrecedence e p pctx
let exprs es = this.exprs es pctx
Expand All @@ -1525,7 +1543,6 @@ module YIL =
| ObjectReceiver _ -> this.receiver (r, pctx)
let case c = this.case c pctx
let tp = this.tp
let tps = this.tps

match e with
| EVar n ->
Expand All @@ -1548,7 +1565,12 @@ module YIL =
| EInt (v, _) -> v.ToString()
| EReal (v, _) -> v.ToDecimalString()
| EQuant (q, lds, r, b) ->
// Dafny complains about unusual indentation if we do not indent when there is a new line
// inside the condition or the body.
let forallCondition =
// single line: ... :: cond ==>
// multiple lines: ... ::
// cond ==>
match q, r with
| Forall, Some e ->
// ==> is 2
Expand All @@ -1569,6 +1591,15 @@ module YIL =
| _ -> ""
| _ -> ""
let body =
// single line: ... :: cond ==> body
// or ... ::
// cond ==> body
//
// multiple lines: ... :: cond ==>
// body
// or ... ::
// cond ==>
// body
match q, r with
| Forall, Some _ ->
expr 3 b // ==> is 2
Expand Down

0 comments on commit 805ca73

Please sign in to comment.