feat(formal): add Lean 4 discrete-event kernel model and CI gate

.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

.gitignore

@@ -1,7 +1,19 @@
-# 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

formal/Formal.lean

@@ -0,0 +1,2 @@
+import Formal.Kernel
+import Formal.Theorems

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

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

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.

formal/lake-manifest.json

@@ -0,0 +1,6 @@
+{"version": "1.3.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "funnelscript_formal",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

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 := "."

formal/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.35.0