From 4cbeeb7937c212280c1a8f08a9703ca4347e1f11 Mon Sep 17 00:00:00 2001 From: Mamdouh Aboammar Date: Fri, 13 Nov 2026 08:40:31 +0200 Subject: [PATCH 1/2] feat(formal): add Lean 4 discrete-event kernel model and CI gate --- .github/workflows/formal-lean.yml | 32 +++++++++ .gitignore | 3 + formal/Formal.lean | 2 + formal/Formal/Kernel.lean | 115 ++++++++++++++++++++++++++++++ formal/Formal/Theorems.lean | 48 +++++++++++++ formal/README.md | 33 +++++++++ formal/lake-manifest.json | 6 ++ formal/lakefile.lean | 9 +++ formal/lean-toolchain | 1 + 9 files changed, 249 insertions(+) create mode 100644 .github/workflows/formal-lean.yml create mode 100644 formal/Formal.lean create mode 100644 formal/Formal/Kernel.lean create mode 100644 formal/Formal/Theorems.lean create mode 100644 formal/README.md create mode 100644 formal/lake-manifest.json create mode 100644 formal/lakefile.lean create mode 100644 formal/lean-toolchain diff --git a/.github/workflows/formal-lean.yml b/.github/workflows/formal-lean.yml new file mode 100644 index 0000000..8f52648 --- /dev/null +++ b/.github/workflows/formal-lean.yml @@ -0,0 +1,32 @@ +name: Lean formal verification + +on: + push: + branches: [main] + pull_request: + workflow_dispatch: + +permissions: + contents: read + +jobs: + formal: + name: Build machine-checked kernel theorems + runs-on: ubuntu-latest + defaults: + run: + working-directory: formal + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - name: Install pinned Lean toolchain + run: | + curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + - name: Build and check theorems + run: "$HOME/.elan/bin/lake build" + - name: Reject holes and custom axioms + run: | + if grep -RnE '\b(sorry|admit)\b|^[[:space:]]*axiom[[:space:]]' Formal.lean Formal/; then + echo 'Untrusted proof construct detected' + exit 1 + fi diff --git a/.gitignore b/.gitignore index 809472e..99cff42 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,9 @@ __pycache__/ *.py[oc] .pytest_cache/ +# Lean build artifacts +.lake/ + # Agent workspaces and plans /plans /.agents diff --git a/formal/Formal.lean b/formal/Formal.lean new file mode 100644 index 0000000..57a9898 --- /dev/null +++ b/formal/Formal.lean @@ -0,0 +1,2 @@ +import Formal.Kernel +import Formal.Theorems diff --git a/formal/Formal/Kernel.lean b/formal/Formal/Kernel.lean new file mode 100644 index 0000000..d1d191a --- /dev/null +++ b/formal/Formal/Kernel.lean @@ -0,0 +1,115 @@ +import Std + +namespace FunnelScript.Formal + +/-! +A domain-neutral, discrete-time abstraction of EventMachine v0. +Time is a natural number rather than the finite non-negative float of the +Python implementation. The abstraction does not establish float/PRNG parity. +-/ + +structure Event where + time : Nat + priority : Int + ordinal : Nat + name : String + deriving Repr, Inhabited, DecidableEq + +structure EventDraft where + time : Nat + priority : Int + name : String + deriving Repr, Inhabited, DecidableEq + +structure Transition (σ : Type) where + state : σ + seed : Nat + emitted : List EventDraft + +abbrev Reducer (σ : Type) := σ → Event → Nat → Transition σ + +structure Machine (σ : Type) where + state : σ + seed : Nat + clock : Nat + nextOrdinal : Nat + pending : List Event + +/-- Lexicographic ordering: timestamp, priority, insertion ordinal. -/ +def eventLE (a b : Event) : Bool := + if a.time < b.time then true + else if b.time < a.time then false + else if a.priority < b.priority then true + else if b.priority < a.priority then false + else decide (a.ordinal ≤ b.ordinal) + +/-- A list implementation of the Python heap's selection policy. -/ +def sortedCalendar (events : List Event) : List Event := + events.mergeSort eventLE + +/-- Allocate stable, increasing ordinals to locally emitted events. -/ +def stamp : Nat → List EventDraft → List Event × Nat + | next, [] => ([], next) + | next, e :: es => + let (tail, last) := stamp (next + 1) es + ({ time := e.time, priority := e.priority, + ordinal := next, name := e.name } :: tail, last) + +/-- Enforce causal time and forbid priority retrogression at equal time. -/ +def legalEmissions (parent : Event) (events : List EventDraft) : Bool := + events.all fun e => decide + (parent.time ≤ e.time ∧ + (e.time = parent.time → parent.priority ≤ e.priority)) + +/-- Evidence carried by a successful, machine-checked kernel step. -/ +structure Advance {σ : Type} (previous : Machine σ) where + event : Event + next : Machine σ + legalTime : previous.clock ≤ event.time + nextClock : next.clock = event.time + +/-- A finite-step executable kernel with explicit rejection of illegal emissions. -/ +def advance {σ : Type} (reduce : Reducer σ) + (machine : Machine σ) : Option (Advance machine) := + match sortedCalendar machine.pending with + | [] => none + | event :: remaining => + if legal : machine.clock ≤ event.time then + let transition := reduce machine.state event machine.seed + if legalEmissions event transition.emitted then + let (generated, nextOrdinal) := + stamp machine.nextOrdinal transition.emitted + let next : Machine σ := { + state := transition.state + seed := transition.seed + clock := event.time + nextOrdinal := nextOrdinal + pending := remaining ++ generated + } + some { + event := event + next := next + legalTime := legal + nextClock := rfl + } + else none + else none + +/-- Processing fuel is the event limit; pending events remain when fuel expires. -/ +def run {σ : Type} (reduce : Reducer σ) : + Nat → Machine σ → Machine σ × List Event + | 0, machine => (machine, []) + | fuel + 1, machine => + match advance reduce machine with + | none => (machine, []) + | some step => + let (final, trace) := run reduce fuel step.next + (final, step.event :: trace) + +/-- Each event is at or later than the preceding processed timestamp. -/ +def ChronologicalFrom (clock : Nat) : List Event → Prop + | [] => True + | event :: rest => + clock ≤ event.time ∧ ChronologicalFrom event.time rest + +end FunnelScript.Formal diff --git a/formal/Formal/Theorems.lean b/formal/Formal/Theorems.lean new file mode 100644 index 0000000..c0aae76 --- /dev/null +++ b/formal/Formal/Theorems.lean @@ -0,0 +1,48 @@ +import Formal.Kernel + +namespace FunnelScript.Formal + +/-- Every successfully executed event respects the preceding clock. -/ +theorem timestamp_monotonicity {σ : Type} (reduce : Reducer σ) : + (fuel : Nat) → (initial : Machine σ) → + ChronologicalFrom initial.clock (run reduce fuel initial).2 := by + intro fuel + induction fuel with + | zero => + intro initial + simp [run, ChronologicalFrom] + | succ fuel ih => + intro initial + cases h : advance reduce initial with + | none => + simp [run, h, ChronologicalFrom] + | some step => + have tail : + ChronologicalFrom step.event.time + (run reduce fuel step.next).2 := by + simpa [step.nextClock] using ih step.next + simpa [run, h, ChronologicalFrom] using + (And.intro step.legalTime tail) + +/-- A fixed pure reducer and identical complete input give identical replay. -/ +theorem deterministic_replay {σ : Type} (reduce : Reducer σ) + (fuel : Nat) (first second : Machine σ) + (sameInput : first = second) : + run reduce fuel first = run reduce fuel second := by + cases sameInput + rfl + +/-- The small-step transition is functional: two results cannot diverge. -/ +theorem unique_advance {σ : Type} (reduce : Reducer σ) + (initial : Machine σ) (a b : Advance initial) + (ha : advance reduce initial = some a) + (hb : advance reduce initial = some b) : a = b := by + rw [ha] at hb + cases hb + rfl + +end FunnelScript.Formal + +#print axioms FunnelScript.Formal.timestamp_monotonicity +#print axioms FunnelScript.Formal.deterministic_replay +#print axioms FunnelScript.Formal.unique_advance diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 0000000..38c385e --- /dev/null +++ b/formal/README.md @@ -0,0 +1,33 @@ +# FunnelScript Event Kernel: Mechanized Model, Milestone 1 + +## Research anchor and falsifiable claims + +Contract: `spec/event-kernel-v0.md`, especially H-K1 to H-K3. The event-calendar model follows discrete-event semantics (Zeigler, 1989) and stable priority queue ordering (`heapq`, Python documentation). + +* **H-F1**: For all successful finite runs in the Lean model, each processed event's timestamp is no earlier than the previous event's timestamp. Counterexample: a trace violating `ChronologicalFrom`. +* **H-F2**: The same reducer, complete machine state (including seed, clock, pending events and insertion ordinal), and event limit produce equal final state and trace. Counterexample: two calls to `run` on equal inputs producing different results. + +The model orders `(time, priority, insertion ordinal)`, rejects emissions into the past and same-time priority retrogression, and gives every emission an ordinal. `run` uses explicit finite fuel, not unrestricted recursion. + +## Verification boundary + +The formal model uses `Nat` time and a pure Lean reducer with an explicit deterministic seed threaded through transitions. Python accepts finite, non-negative `int` and `float` timestamps, and uses Python `random.Random`. This Lean artifact **does not** prove floating-point ordering equivalence, CPython PRNG bit parity, the absence of external side effects in arbitrary Python reducers, or Python runtime type soundness. + +In this milestone, invalid emission and time contracts yield `none` in `advance`; the reference Python implementation throws an exception. The theorem applies to successful executions, not to error-message equivalence. `run` stops when fuel expires, while Python raises on exceeding `max_events`. This distinction requires separate verification before asserting interpreter conformance. + +`timestamp_monotonicity` is about the executable `run` function, not an assumed pre-sorted trace. The theorem follows from the time-checking witness built by `advance`. `deterministic_replay` establishes extensional determinism of the pure model, conditional on identical full inputs. Neither theorem claims scientific predictive accuracy. + +## Build + +From the `formal/` directory: + +```bash +lake build +rg -n '\b(sorry|admit)\b|^\s*axiom\b' Formal.lean Formal/ +``` + +The source is intended to compile without `sorry`, `admit`, or custom axioms. Only a successful real `lake build` establishes verified build status. + +## Deferred + +Typed Worlds, progress and preservation, guard and payload soundness, exact stochastic distribution semantics, float fidelity, bounded-recursion error parity, and the differential oracle belong to subsequent milestones. The initial property-based suite in the implementation repository focuses on the existing Python kernel's observable contracts. diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json new file mode 100644 index 0000000..eb10e0b --- /dev/null +++ b/formal/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "funnelscript_formal", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/lakefile.lean b/formal/lakefile.lean new file mode 100644 index 0000000..8a1416a --- /dev/null +++ b/formal/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open Lake DSL + +package funnelscript_formal where + version := v!"0.1.0" + +@[default_target] +lean_lib Formal where + srcDir := "." diff --git a/formal/lean-toolchain b/formal/lean-toolchain new file mode 100644 index 0000000..a6aff06 --- /dev/null +++ b/formal/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0 From 84465a25048eca425d247aa33268c32756d38e07 Mon Sep 17 00:00:00 2001 From: Mamdouh Aboammar Date: Sat, 14 Nov 2026 16:35:36 +0200 Subject: [PATCH 2/2] chore(git): harden gitignore with OS and build artifacts --- .gitignore | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 99cff42..37709b6 100644 --- a/.gitignore +++ b/.gitignore @@ -1,11 +1,20 @@ -# Python caches +# Python caches and artifacts __pycache__/ *.py[oc] .pytest_cache/ +.hypothesis/ +build/ +dist/ +*.egg-info +.venv/ # Lean build artifacts .lake/ +# OS metadata +.DS_Store +Thumbs.db + # Agent workspaces and plans /plans /.agents