Laurel Language Enhancements #385
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
fabiomadge
force-pushed
the
jverify-strata-backend
branch
from
2924fc9 to
8122075
Compare
…t assignments Feature changes: - Assign AST now takes a list of targets for multi-output procedure calls - Remove Determinism enum from Body.Opaque - TField replaced with TTypedField carrying the value type - Heap parameterization uses explicit $heap_in/$heap_out parameters instead of a single global $heap variable - Heap-writing calls in expressions produce multi-target assignments - Expression assignment lifting uses per-variable snapshots for correct evaluation order - Composite type parsing implemented (was a TODO) - New tests: caller, expression-context heap calls, sequential mutations, implicit equality Bug fixes: - Remove stale $heap global references in LaurelToCoreTranslator - Remove unused global $heap variable declaration and modifies clause - Fix .get! crash in HeapParameterization FieldSelect read path - Use actual callee return type for fresh variables instead of hardcoded TInt - Fix incorrect .reverse in transformProcedureBody - Remove dead SequenceM.setInsideCondition
fabiomadge
force-pushed
the
jverify-strata-backend
branch
2 times, most recently
from
db4618f to
1ecb548
Compare
# Conflicts: # Strata/DDM/Integration/Lean/Gen.lean # Strata/DL/Util/Func.lean # Strata/Languages/C_Simp/DDMTransform/Parse.lean # Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean # Strata/Languages/Laurel/Grammar/LaurelGrammar.st # Strata/Languages/Laurel/HeapParameterization.lean # Strata/Languages/Laurel/Laurel.lean # Strata/Languages/Laurel/LaurelFormat.lean # Strata/Languages/Laurel/LaurelToCoreTranslator.lean # Strata/Languages/Laurel/LiftExpressionAssignments.lean # StrataTest/Languages/C_Simp/Examples/Coprime.lean # StrataTest/Languages/C_Simp/Examples/LinearSearch.lean # StrataTest/Languages/C_Simp/Examples/LoopSimple.lean # StrataTest/Languages/C_Simp/Examples/LoopTrivial.lean # StrataTest/Languages/C_Simp/Examples/Min.lean # StrataTest/Languages/C_Simp/Examples/SimpleTest.lean # StrataTest/Languages/C_Simp/Examples/Trivial.lean # StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean # StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
fabiomadge
force-pushed
the
jverify-strata-backend
branch
from
1ecb548 to
7517b51
Compare
- Remove dead mkStmtExprMdEmpty' in LiftExpressionAssignments - Move duplicate StmtExprMd.sizeOf_val_lt theorem to Laurel.lean - Restore type info in TTypedField formatting - Fix StmtExprMd doc comment (was copy-pasted from HighTypeMd)
…necessary Strata. qualifications in MetaData
…vert unused LaurelEval changes
…lication - Remove local boolImpliesOp duplicate; use Core.boolImpliesOp via open - Remove dead translateParameterToCore (unused, superseded by WithCT variant) - Remove dead HighType.isHeap (zero call sites) - Remove dead fnTy binding (always none) - Remove heapWriters param from translateStmt (never read, only forwarded) - Fix isPureExpr: reject IfThenElse without else branch (wrong default in function translation path) - Remove stale debug comment and blank line
…ent decreases/invariant in C_Simp while loops
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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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