Introduce FunctionsAndProofs IR and rename OrderedLaurel to CoreWithLaurelTypes#925
Introduce FunctionsAndProofs IR and rename OrderedLaurel to CoreWithLaurelTypes#925keyboardDrummer-bot wants to merge 5 commits intomainfrom
Conversation
…aurelTypes - Add FunctionsAndProofsProgram structure with functions, proofs, datatypes, constants - Add temporary laurelToFunctionsAndProofs translation (functional → functions, non-functional → proofs) - Rename OrderedLaurel to CoreWithLaurelTypes - Change OrderedDecl: replace 'procs' with 'funcs' (for function SCCs) and 'procedure' (for individual proofs) - Rewire pipeline: Laurel → FunctionsAndProofs → CoreWithLaurelTypes → Core - Both functions and proofs participate in topological ordering via the call graph Addresses steps (c) and (d) of #924.
|
Can you motivate these changes? |
|
This PR implements steps (c) and (d) from #924. The motivation comes from a planned restructuring of the Laurel-to-Core pipeline to support a new "contract pass" and "proof pass." Currently the pipeline is: The goal (from #924) is to evolve it into: The key idea is to explicitly separate Laurel procedures into functions (pure computation) and proofs (verification-only), which today are conflated under a single Concretely, this PR:
This is scaffolding for the contract and proof passes that will follow. The current |
| public inductive OrderedDecl where | ||
| /-- A group of functions (single non-recursive, or mutually recursive). -/ | ||
| | procs (procs : List Procedure) (isRecursive : Bool) | ||
| | funcs (funcs : List Procedure) (isRecursive : Bool) |
There was a problem hiding this comment.
What would it mean to have >1 functions in the list with isRecursive=false? Or is this disallowed somewhere?
There was a problem hiding this comment.
Good question. Having >1 functions with isRecursive=false shouldn't happen in practice — computeSccDecls sets isRecursive=true whenever the SCC has more than one member (see procs.length > 1 on line 161). The only way to get isRecursive=false is a single-element SCC with no self-loop.
That said, the type doesn't enforce this invariant — it's maintained by the caller. @keyboardDrummer, would you like me to tighten this, e.g. by splitting into separate func/mutualFuncs constructors, or is the current representation fine for now?
| `FunctionsAndProofsProgram`. | ||
| -/ | ||
| public structure OrderedLaurel where | ||
| public structure CoreWithLaurelTypes where |
There was a problem hiding this comment.
Curious why the name was changed. I think OrderedLaurel is more descriptive than CoreWithLaurelTypes, though I think I may know what you mean by the latter (non-blocking).
There was a problem hiding this comment.
The rename was specified in #924 by @keyboardDrummer. The idea is that at this point in the pipeline, declarations have been grouped and topologically ordered (Core's structure), but the types are still Laurel types — the final dumb translation to Core hasn't happened yet. So CoreWithLaurelTypes describes what the IR is: Core's shape, Laurel's types.
I agree OrderedLaurel is also descriptive — happy to defer to whatever you and @keyboardDrummer prefer.
|
Thanks for the review @joscoh! I replied to each of your three comments inline. Summary:
|
| let orderedDecls := (computeSccDecls program).flatMap fun (procs, isRecursive) => | ||
| -- Split the SCC into functions and proofs | ||
| let (funcs, proofs) := procs.partition (fun p => funcNames.contains p.name.text) | ||
| let funcDecl := if funcs.isEmpty then [] else [OrderedDecl.funcs funcs isRecursive] | ||
| let proofDecls := proofs.map OrderedDecl.procedure | ||
| funcDecl ++ proofDecls |
There was a problem hiding this comment.
This SCC splitting has a subtle correctness concern. If an SCC contains both functions and proofs (e.g., a function that calls a proof, or vice versa), two things go wrong:
-
isRecursiveleaks across the split. The flag was computed for the whole SCC. After partitioning, the functions subset might not be recursive among themselves, but they'll be markedisRecursive=truebecause the SCC was recursive due to cross-category edges. This would causetranslateProcedureToFunctionto emit arecFuncBlockfor functions that aren't actually mutually recursive. -
Ordering within the SCC is lost. Proofs are emitted after functions (
funcDecl ++ proofDecls). If a function depends on a proof in the same SCC, the proof won't be available yet.
I suspect mixed SCCs can't happen today (a functional procedure probably can't call a non-functional one), but the code doesn't enforce or document this assumption. At minimum, consider adding an assertion or comment:
-- Mixed SCCs (functions + proofs) should not occur: functional procedures
-- do not call non-functional ones. If this changes, the splitting logic
-- here needs revisiting.
if !funcs.isEmpty && !proofs.isEmpty then
-- log a warning or panic| (program.staticProcedures.filter (fun p => !p.body.isExternal)) | ||
| |>.partition (fun p => p.invokeOn.isSome) | ||
| allProcs.partition (fun p => p.invokeOn.isSome) | ||
| let nonExternal : List Procedure := withInvokeOn ++ withoutInvokeOn |
There was a problem hiding this comment.
Nit: nonExternal is a misleading name now that computeSccDecls takes a FunctionsAndProofsProgram — external procedures are already filtered out by laurelToFunctionsAndProofs. This is just the invokeOn-partitioned list of all procedures. Consider renaming to orderedProcs or allProcsSorted, and updating the comment on line 122 ("Build a call-graph over all non-external procedures") accordingly.
| structure FunctionsAndProofsProgram where | ||
| functions : List Procedure | ||
| proofs : List Procedure | ||
| datatypes : List DatatypeDefinition | ||
| constants : List Constant | ||
|
|
There was a problem hiding this comment.
The structure looks good. One question: should FunctionsAndProofsProgram carry a well-formedness invariant that functions and proofs are disjoint (no procedure name appears in both)? Today this is guaranteed by List.partition, but if the structure is ever constructed differently (e.g., by the upcoming proof pass), the invariant could be violated silently.
Not blocking — just worth considering as the IR evolves.
| def laurelToFunctionsAndProofs (program : Program) : FunctionsAndProofsProgram := | ||
| let nonExternal := program.staticProcedures.filter (fun p => !p.body.isExternal) | ||
| let (functions, proofs) := nonExternal.partition (·.isFunctional) | ||
| let datatypes := program.types.filterMap fun td => match td with | ||
| | .Datatype dt => some dt | ||
| | _ => none | ||
| { functions, proofs, datatypes, constants := program.constants } |
There was a problem hiding this comment.
The doc comment says "Temporary translation" — good. For traceability, consider adding a reference to the issue: "Will be replaced by the contract and proof passes (#924)."
Also: program.types may contain .Composite entries that are silently dropped here. This is correct (they're handled via the program parameter in translateLaurelToCore), but a brief comment would help future readers understand why only .Datatype is kept.
| public inductive OrderedDecl where | ||
| /-- A group of functions (single non-recursive, or mutually recursive). -/ | ||
| | procs (procs : List Procedure) (isRecursive : Bool) | ||
| | funcs (funcs : List Procedure) (isRecursive : Bool) | ||
| /-- A single (non-functional) procedure. -/ | ||
| | procedure (procedure : Procedure) |
There was a problem hiding this comment.
Re joscoh's unresolved thread (line 174): the invariant that funcs has >1 element only when isRecursive=true is maintained by computeSccDecls but not enforced by the type. Since this is scaffolding for #924, I'd suggest at minimum adding a doc comment on the funcs constructor:
| public inductive OrderedDecl where | |
| /-- A group of functions (single non-recursive, or mutually recursive). -/ | |
| | procs (procs : List Procedure) (isRecursive : Bool) | |
| | funcs (funcs : List Procedure) (isRecursive : Bool) | |
| /-- A single (non-functional) procedure. -/ | |
| | procedure (procedure : Procedure) | |
| /-- A group of functions (single non-recursive, or mutually recursive). | |
| Invariant: `funcs.length > 1 → isRecursive = true`. -/ | |
| | funcs (funcs : List Procedure) (isRecursive : Bool) |
| let functionsAndProofs := laurelToFunctionsAndProofs program | ||
| let ordered := orderFunctionsAndProofs functionsAndProofs |
There was a problem hiding this comment.
No direct unit tests for laurelToFunctionsAndProofs or orderFunctionsAndProofs. The coverage comes from end-to-end tests through the full pipeline, which is reasonable for now since this is scaffolding.
However, as the contract and proof passes land, consider adding targeted tests that verify:
laurelToFunctionsAndProofscorrectly partitions functional vs. non-functional proceduresorderFunctionsAndProofspreserves the topological ordering invariant (dependencies before dependents)- No procedures are lost in the Laurel → FunctionsAndProofs → CoreWithLaurelTypes → Core pipeline (a simple count check would suffice)
|
Thanks for the thorough review @tautschnig! I've pushed a commit (ed8ba72) addressing the straightforward items. Here's a summary of each point: Addressed in ed8ba72
Discussion points
|
|
@keyboardDrummer-bot Please resolve git conflicts. |
Keep both the FunctionsAndProofs pipeline from this branch and the overflowChecks field added on main.
|
Resolved the merge conflict in Built |
5 participants
Summary
Implements steps (c) and (d) from #924: introduces the
FunctionsAndProofsIR and renamesOrderedLaureltoCoreWithLaurelTypes.Changes
New file:
FunctionsAndProofs.leanFunctionsAndProofsProgramwithfunctions,proofs,datatypes, andconstantsfields (all usingLaurel.Procedure)laurelToFunctionsAndProofstranslation that partitions Laurel procedures byisFunctional— functional procedures become functions, non-functional become proofsCoreGroupingAndOrdering.leanOrderedLaurel→CoreWithLaurelTypesOrderedDecl:procs→funcs(for function SCCs, withisRecursiveflag)procedure(singular, for individual proofs — no mutual recursion)orderFunctionsAndProofsreplacesorderProgram: takes aFunctionsAndProofsProgram, runs both functions and proofs through the SCC/topological ordering (soinvokeOnaxioms are correctly placed), then classifies each SCC intofuncsorproceduredeclsLaurelToCoreTranslator.leantranslateLaurelToCorenow takesCoreWithLaurelTypesinstead ofOrderedLaurelfuncs(translated to Core functions) andprocedure(translated to Core procedures) separatelyLaurelCompilationPipeline.leanlaurelToFunctionsAndProofs→orderFunctionsAndProofs→translateLaurelToCore→ CorePipeline (new)
Testing
DDM.Integration.Java.TestGenandPython.AnalyzeLaurelTest)Closes steps (c) and (d) of #924.