Repository navigation
feat(formal): add Lean 4 discrete-event kernel model and CI gate - #10
Merged
Merged
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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
Adds the formal Lean 4 discrete-event kernel model, mechanized proofs, and CI gate for Milestone 1 formal verification of the FunnelScript event kernel.
Key Deliverables
formal/Formal/Kernel.lean): Pinned to Lean 4.35.0, implements finite discrete-time event calendar ordering by(time, priority, insertion ordinal), small-step functional transitionadvance, legal non-retrograde emission witness, and fuel-boundedrun.formal/Formal/Theorems.lean):timestamp_monotonicity: Mechanized proof that processed event timestamps are monotonically non-decreasing over successful executions (ChronologicalFrom).deterministic_replay: Mechanized proof that identical initial machine state, seed, and fuel produce identical final trace.unique_advance: Functional determinism theorem proving transition results cannot diverge.sorry,admit, or custom axioms)..github/workflows/formal-lean.yml): Automated CI runninglake buildand untrusted construct check on push and pull requests..gitignore): Hardened gitignore against OS metadata and build artifacts.Verification
cd formal && lake build: 5 jobs completed successfully.sorry/admit/axiomoccurrences found.uv run --no-project --python 3.12 --with pytest pytest -v(63 passed, 154 subtests passed).python3 -m unittest discover -s tests -v(10 passed).