Mutable fields #338
Mutable fields #338
Conversation
| @@ -0,0 +1,48 @@ | |||
| /- | |||
There was a problem hiding this comment.
Can we rename "Boogie" to "StrataCore"?
| assert y == 2; | ||
| assert false; | ||
| // ^^^^^^^^^^^^^ error: assertion does not hold | ||
| procedure NestedImpureStatements() { |
There was a problem hiding this comment.
Ideally these (and below) would be defined using:
#strata
...
#end
There was a problem hiding this comment.
(Not blocking)
| def transformProcedureBody (body : StmtExpr) : StmtExpr := | ||
| let (seqStmts, _) := transformStmt body |>.run {} | ||
| def transformProcedureBody (body : StmtExpr) : SequenceM StmtExpr := do | ||
| let seqStmts <- transformStmt body |
There was a problem hiding this comment.
| let seqStmts <- transformStmt body | |
| let seqStmts ← transformStmt body |
| let seqBody := transformProcedureBody bodyExpr | ||
| { proc with body := .Transparent seqBody } | ||
| | _ => proc -- Opaque and Abstract bodies unchanged | ||
| let seqBody <- transformProcedureBody bodyExpr |
There was a problem hiding this comment.
| let seqBody <- transformProcedureBody bodyExpr | |
| let seqBody ← transformProcedureBody bodyExpr |
| | .TInt => LMonoTy.int | ||
| | .TBool => LMonoTy.bool | ||
| | .TVoid => LMonoTy.bool -- Using bool as placeholder for void | ||
| | .TVoid => LMonoTy.bool |
There was a problem hiding this comment.
Do we want this long-term?
| let check : Core.Procedure.Check := { expr := translateExpr constants initEnv postcond } | ||
| [("ensures", check)] | ||
| | _ => [] | ||
| -- Add $heap to modifies clause only if this procedure writes to the heap |
There was a problem hiding this comment.
Calling this "Add" when modifies is ["$heap"] or [] confused me. Maybe just remove this comment?
| modifies := [] | ||
| preconditions := [] | ||
| postconditions := [] | ||
| modifies := modifies |
There was a problem hiding this comment.
| modifies := modifies | |
| modifies, |
| preconditions := [] | ||
| postconditions := [] | ||
| modifies := modifies | ||
| preconditions := preconditions |
There was a problem hiding this comment.
| preconditions := preconditions | |
| preconditions, |
| postconditions := [] | ||
| modifies := modifies | ||
| preconditions := preconditions | ||
| postconditions := postconditions |
There was a problem hiding this comment.
| postconditions := postconditions | |
| postconditions, |
| body := none | ||
| } | ||
|
|
||
| -- Axiom 1: read-over-write-same |
There was a problem hiding this comment.
Having axioms in the translator feels weird to me. Could this go in a prelude?
| IO.FS.withTempDir (fun tempDir => | ||
| EIO.toIO (fun f => IO.Error.userError (toString f)) | ||
| (Core.verify smtsolver coreProgram tempDir options)) | ||
| match boogieProgramExcept with |
There was a problem hiding this comment.
| match boogieProgramExcept with | |
| match strataCoreProgramExcept with |
| (options : Options := Options.default) | ||
| (tempDir : Option String := .none) | ||
| : IO (Except (Array DiagnosticModel) VCResults) := do | ||
| let boogieProgramExcept := translate program |
There was a problem hiding this comment.
| let boogieProgramExcept := translate program | |
| let strataCoreProgramExcept := translate program |
| deriving Repr, BEq | ||
|
|
||
| def toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Core.VCResult) : Option Diagnostic := do | ||
| def DiagnosticModel.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (dm: DiagnosticModel): Diagnostic := |
There was a problem hiding this comment.
Diagnostic seems like a more general notion, and I think it may make sense to place it where it can be reusable. Maybe your new PR (that I haven't seen yet) about metadata locations does that?
There was a problem hiding this comment.
I'm also a little unclear on whether the diagnostic printing will lose the kind of proof-obligation specific printing we've got going in this file (e.g., VCResults formatting). Mind helping me understand the implications here?
6 participants
Changes
Testing
T1_MutableFields.leanT2_ImpureExpressionsNotSupported