Conversation
added 27 commits
February 4, 2026 13:45
…handling Now produces definition-time and call-time wf assumptions Preserves implications in exprs to avoid losing information Handles calls in quantifiers and lambdas correctly Some more test cases
Don't generate VCs directly, instead transform into asserts with extra procedures Includes tests Reverts many prior changes
Need to duplicate Factory datatype parts (for now) because of type aliases
Fix issue with indices in Translate.lean Add test case in PrecondElim.lean Need to thread Factory through to keep track of func preconditions
Factory generated on the fly, not all at once Correctly handle function decl statement scopes Improve comments and formatting
joscoh
dismissed
MikaelMayer’s stale review
Discussed separately, Mikael is unavailable at the moment
aqjune-aws
reviewed
Feb 20, 2026
aqjune-aws
previously approved these changes
Feb 20, 2026
shigoel
reviewed
Feb 23, 2026
added 4 commits
February 23, 2026 15:03
Run after FilterProcedures and add test to ensure nothing about filtered procedure is verified
shigoel
approved these changes
Feb 23, 2026
aqjune-aws
approved these changes
Feb 23, 2026
fabiomadge
added a commit
that referenced
this pull request
Feb 24, 2026
Merged commits: f6ff88b, a6e5f93, 64fd6d6, 6f67113, 9dccebf, a0716de, 1221d67, d1c7ddd, cb2411d Conflict resolutions: - IntBoolFactory.lean: took HEAD (has full function set + DivT/ModT). Added intSafeDivFunc/intSafeModFunc with preconditions (PR #444). Added Inhabited constraint to IntBoolFactory. - SMTEncoder.lean: added main's SafeMod + DivT/ModT SMT encodings. - LaurelToCoreTranslator.lean: took HEAD logic, wrapped init RHS values in `some` for PR #432's Cmd.init signature change. - Laurel.lean: took main's version (PR #434 docstrings), then restored branch-specific changes: preconditions (list) in Procedure, postconditions (list) in Body.Opaque/Abstract, removed Determinism, added deriving Repr on WithMetadata and HighType, added Repr instance for Imperative.MetaData.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 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.
Description of changes: Adds support for function preconditions to Core. This is done via a transformation
precondElimthat is run before typechecking (to ensure that the generated assertions are typechecked).Structure:
Strata/DL/Lambda/Preconditions.leangenerates well-formedness conditions for Lambda expressionsStrata/Transform/PrecondElim.leancontains the transformation that1. adds assertions at function call sites to verify that preconditions hold
2. checks the well-formedness of procedure and function contracts by ensuring that any preconditions of functions used in the contract hold
3. removes preconditions from functions, making everything total
Tests
StrataTest/DL/Lambda/PreconditionsTests.leancontains tests for generating well-formedness conditions for Lambda expressions (i.e. preconditions in called functions)StrataTest/Transform/PrecondElim.leancontains tests of theprecondElimtransformationStrataTest/Languages/Core/Examples/FunctionPreconditions.leancontains tests that involve the end-to-end verification of functions (including function decl statements) with preconditionsOther smaller changes include adding syntax for preconditions to the Core grammar, adding metadata for these preconditions, and adding a precondition that the denominator is nonzero to
Int.divandInt.mod(updating the corresponding proof obligations in tests).Note that ADT destructors do NOT by default have a precondition that they are called on the correct constructor (e.g. that
List..headis called on something satisfyingList..isCons). This will happen in a future PR, and we will include both checked and unchecked versions.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.