Conversation
Add HighTypeMd.sizeOf_val_lt lemma and use it to prove translateType terminates. The remaining partial defs recurse through List StmtExprMd which requires the same sizeOf bridging pattern that is a known issue across the codebase (see PR #396).
Make translateTypeWithCT, translateSimpleExpr, translateSeqBounds,
translateExpr, collectConstrainedArrayAccesses, translateStmt, and
isPureExpr total using the match _h : e.val pattern with
StmtExprMd.sizeOf_val_lt + rw/simp in decreasing_by.
For list recursion (args.mapM, args.all, args.flatMap), use
args.attach.{mapM,all,flatMap} to provide membership proofs,
combined with List.sizeOf_lt_of_mem.
Only resolveBaseType remains partial (needs acyclicity assumption
on ConstrainedTypeMap).
…ion proofs Replace 6 identical decreasing_by blocks with a shared tactic macro. Also unify the two HighTypeMd decreasing_by proofs.
Resolve conflicts from bab0508 'Add metadata to more places in Laurel': - Adopt main's WithMetadata generic struct with HighTypeMd/StmtExprMd abbrevs - Keep branch's richer AST: plural pre/postconditions/invariants, DivT/ModT/Implies ops - Keep branch's Determinism removal (was dead code) - Keep branch's .reverse bug fix in transformProcedureBody - Update sizeOf_val_lt references to use WithMetadata.sizeOf_val_lt - Add deriving Repr for HighType and WithMetadata
Resolve conflicts from c0409bb 'Add tactic for simplifying termination proofs': - Use term_by_mem where applicable in Laurel termination proofs - Keep manual proofs where term_by_mem can't handle the goal (HighType recursion, attach patterns)
| inputs : List Parameter | ||
| outputs : List Parameter | ||
| precondition : WithMetadata StmtExpr | ||
| determinism : Determinism |
There was a problem hiding this comment.
What happened to determinism?
There was a problem hiding this comment.
Intentionally removed in 67931730 — it was only ever set to .nondeterministic and never pattern-matched on.
There was a problem hiding this comment.
I know it wasn't used but that doesn't mean it shouldn't be there. The whole AST wasn't used when it was first merged. Can you bring it back?
|
|
||
| theorem WithMetadata.sizeOf_val_lt {t : Type} [SizeOf t] (e : WithMetadata t) : sizeOf e.val < sizeOf e := by | ||
| cases e; grind | ||
| cases e <;> simp_wf <;> omega |
There was a problem hiding this comment.
Intentional. omega is simpler and more predictable than grind here, and it proves the goal.
| | _ => none | ||
|
|
||
| /-- Collect Array.Get accesses with constrained element types -/ | ||
| def collectConstrainedArrayAccesses (env : TypeEnv) (tcMap : TranslatedConstraintMap) (e : StmtExprMd) : List (StmtExprMd × StmtExprMd × TranslatedConstraint) := |
There was a problem hiding this comment.
Shouldn't the implementation of constraints be independent of the implementation of Arrays? If this is temporary code, can we mark it as such?
There was a problem hiding this comment.
Added a TODO. Array.Get is special because it's a built-in (SMT select), not a procedure call, so there's no contract to assume from. Other constrained type sources (procedure returns, field reads) get their assumes via contracts. If more built-ins return constrained types in the future, this should be generalized.
| let belse ← match elseBranch with | ||
| | some e => do let (_, s) ← translateStmt ctMap tcMap env outputParams postconds e; pure s | ||
| | none => pure [] | ||
| pure (env, arrayElemAssumes ++ [Imperative.Stmt.ite bcond bthen belse stmt.md]) |
There was a problem hiding this comment.
Why does the translation of IfThenElse refer to arrayElemAssumes? That can't be right
There was a problem hiding this comment.
Good catch — fixed in fb9c7f60. Compound statements (Block, IfThenElse, While) no longer generate arrayElemAssumes at the top level. Their sub-statements handle their own assumes via recursive translateStmt calls.
| (e', acc ++ ss)) (env, []) | ||
| (env', stmtsList) | ||
| | .LocalVariable name ty initializer => | ||
| def translateStmt (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) (env : TypeEnv) (outputParams : List Parameter) (postconds : List (String × Core.Expression.Expr)) (stmt : StmtExprMd) : Except String (TypeEnv × List Core.Statement) := do |
There was a problem hiding this comment.
Why would you introduce assert statements related to postconditions? Core will already check that procedure bodies adhere to the postconditions of that procedure.
There was a problem hiding this comment.
These asserts are needed for early returns. Laurel's return is translated to result := value; assert postconditions; assume false. The assume false prevents fall-through but also makes the path vacuously true, so Core's VCG won't check postconditions on it.
Without the asserts, a postcondition-violating early return passes verification silently. I verified this by writing a Core program where the early return path sets result := -x (violating ensures result >= 0):
- Without the assert before
assume false: ✅ pass (unsound) - With the assert before
assume false: ❌ fail (correct)
There was a problem hiding this comment.
Laurel's return is translated to
result := value; assert postconditions; assume false
Is that new? It's not mentioned in the PR. I think it would be better to encode a return using a jump than an assume false. With the assume false it would be incorrect when executing the code, since then the assume is ignored, and having to assert the postconditions introduces a lot of duplication.
There was a problem hiding this comment.
You're right that goto would be better. I tried implementing it (return value → result := value; goto "\$return" with \$return: {} at the end of the body), and it works correctly for individual procedures.
However, I found a Core VCG issue: when a procedure has a goto inside an if branch, processIteBranches produces multiple EnvWithNext results, and these multiply across procedures via ProgramEval.flatMap. A second procedure's assertions get checked N times instead of once.
Filed as #419 with a proposed fix (merge paths by nextLabel in processIteBranches). Keeping assume false for now until that's resolved.
There was a problem hiding this comment.
I would rather not have the assert <postcondition>; assume false solution merged, for two reasons:
- It duplicates the postconditions for each return so it breaks our goal of having transformations that are linear in size.
- It unnecessarily complicates our code and the intermediate programs, slowing down development.
If we can't implement it with goto due to a Core bug, could you move the related feature to another PR so we can wait for the Core issue to be resolved?
…aints - Don't generate arrayElemAssumes for compound statements (Block, IfThenElse, While). Their sub-statements handle their own assumes via recursive translateStmt calls. Previously, assumes for array accesses inside branches were incorrectly hoisted before the if/while statement. - Add TODO comment explaining why constraint injection is array-specific: Array.Get is a built-in (SMT select), not a procedure call, so there's no contract to assume from.
joehendrix
left a comment
joehendrix
left a comment
There was a problem hiding this comment.
I added a few suggestions, but this looks reasonable to me. I'll approve this if you don't like the suggestions.
- Parser.lean: use Id.run do + early return for comment parsing, replace startsWith with utf8ByteSize check (comment 6) - Java/Gen.lean: match on DDM category name (Init.Num/Init.Decimal) instead of Java type string for builder parameter generation (comment 7) - Format.lean: collapse comma/space/newline seq formatting into single sepBy arm, eliminating duplication (comment 8) - Java/Gen.lean: consolidate getSeparator with SepFormat.toIonName by adding fromCategoryName? and moving Ion-specific functions to Strata.DDM.Ion (comment 9)
fabiomadge
force-pushed
the
jverify-strata-backend
branch
from
80b2cc2 to
88d1a43
Compare
6 participants
Summary
Expands the Laurel language with additional operators, data types, and verification constructs. Improves formatting across multiple dialects.
Key Changes
Laurel Grammar & Translator
-,*,/,%,/t,%t(truncating),==>,!, unary-Array<T>type, indexing, lengthSeq.From,Seq.Take,Seq.Drop,Seq.Containsforall,existsrequires/ensuresclauses per procedureStmtExprMd,HighTypeMd) threaded through ASTInfrastructure
NewlineSepByseparator type for formatting preservationSourceRangeoverloadsCLI Commands
laurelParse,laurelAnalyze,laurelToCore,laurelPrintBug Fixes
insideConditionflag not resetting after conditionalsMaptypesubstFvarLiftingfor proper de Bruijn index handlingTests