Conversation
…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
| @@ -1 +1 @@ | |||
| /- | |||
There was a problem hiding this comment.
Why the rename of this test?
| body := body | ||
| }) .empty | ||
|
|
||
| def arrayTypeSynonym : Core.Decl := .type (.syn { name := "Array", typeArgs := ["T"], type := .tcons "Map" [.int, .ftvar "T"] }) |
There was a problem hiding this comment.
Can you move these static Core definition to CorePrelude.lean ?
| explicitPreconditions := explicitPreconditions ++ [(s!"{proc.name}_pre_{i}", check)] | ||
| let preconditions := inputConstraints ++ arrayLenConstraints ++ explicitPreconditions | ||
| -- Generate constraint checks for output parameters with constrained types | ||
| let outputConstraints : List (Core.CoreLabel × Core.Procedure.Check) ← |
There was a problem hiding this comment.
Can you generate the implicit pre and postconditions in a separate pass in a separate file?
| | some expr => pure (some (s!"{proc.name}_input_{p.name}_constraint", { expr, md := p.type.md })) | ||
| | none => pure none) | ||
| -- Array lengths are implicitly >= 0 | ||
| let arrayLenConstraints : List (Core.CoreLabel × Core.Procedure.Check) := |
There was a problem hiding this comment.
Can you move everything related to arrays to a separate file? Can you elaborate on the design of Array support? How come it's not a Laurel library? The length constraint seems like a type invariant or constrained type.
|
|
||
| /-- Extract sequence bounds from Seq.From/Take/Drop chain. | ||
| Note: Seq.From only works with simple Identifier arguments; complex expressions are not supported. -/ | ||
| def translateSeqBounds (env : TypeEnv) (expr : StmtExprMd) : Except String SeqBounds := |
There was a problem hiding this comment.
Can everything related to sequences be in a separate file? Can it be a separate pass?
| @@ -0,0 +1,42 @@ | |||
| /- | |||
There was a problem hiding this comment.
Can you move and Sequence support tests into a separate folder?
|
Can you add Laurel test |
| match outputParams.head? with | ||
| | some _ => do | ||
| let coreExpr ← translateExpr ctMap tcMap env stmt | ||
| mkReturnStmts (some coreExpr) |
There was a problem hiding this comment.
Is this the scenario where we return "naturally" because we reach the end of a block? Since this is not a jump, should we not call something different than mkReturnStmt which does do a jump?
| op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";"; | ||
| op return (value : StmtExpr) : StmtExpr => "return " value ";"; | ||
| op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}"; | ||
| op block (stmts : NewlineSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{" indent(2, "\n" stmts) "\n}"; |
There was a problem hiding this comment.
The indent(2, is never used anywhere, right? I don't think we're ever printing Laurel through the DDM. Why did you add this?
| return commands | ||
| let (some tree, true) ← runChecked <| elabCommand leanEnv | ||
| | return commands | ||
| -- Prevent infinite loop if parser makes no progress |
| | q`Init.SpacePrefixSepBy, 1 => | ||
| let inner := mkCApp ``Array #[args[0]] | ||
| return if addAnn then mkCApp ``Ann #[inner, annType] else inner | ||
| | q`Init.NewlineSepBy, 1 => |
There was a problem hiding this comment.
Can you say more about this NewlineSepBy operator? What is it for?
Contains a subset of the changes from #385 ### Changes - Fix to Strata/DDM/Parser.lean so it can handle parsing comments `//` in languages that have a division operator - New operators: `-`, `*`, `/`, `%`, `/t`, `%t` (truncating), `==>`, `!`, unary `-` - Quantifiers: `forall`, `exists` - While loops with multiple invariants ### Testing - Added tests for the new features --------- Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
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,existsrequiresclauses per procedureInfrastructure
NewlineSepByseparator type for formatting preservationSourceRangeoverloadsCLI Commands
laurelParse,laurelAnalyze,laurelToCore,laurelPrintBug Fixes
MaptypesubstFvarLiftingfor proper de Bruijn index handlingTests