[Lean] Derive #540's pending ranges from the PR442 schedule (stacked on #540; no new kappa)

research/lean-pending-derivation/PendingBinding.lean

@@ -0,0 +1,48 @@
+import PhysicalSourceConnection
+import PendingDerivation
+
+/-!
+Binds PR540's hand-supplied `PhysicalSourceConnection.pendingTag` to the
+schedule-derived pending sets of `PendingDerivation`. It restates the
+selected-invocation completion theorem with the derived mask. No existing
+definition or theorem is changed.
+
+Apache-2.0. Douglas Colkitt, with Claude (Anthropic) assistance.
+-/
+namespace PendingBinding
+open TreeReplay WholeHosting SourceConnection PhysicalSourceConnection
+
+/-- The hand-supplied ranges `[15,22)` and `[1,29)` are exactly the derived sets. -/
+theorem pendingTag_derived : ∀ (t : SourceOwnership.Tag) (i : SourceOwnership.Axis),
+    pendingTag t i = PendingDerivation.derivedPendingTag t i := by
+  decide +kernel
+
+/-- Pending mask of every host, derived from the source schedule. -/
+def derivedPending : MultiHosting.HostMask Host SourceOwnership.Axis :=
+  fun h => PendingDerivation.derivedPendingTag (SourceOwnership.tag (role h))
+
+theorem pending_eq_derived : pending = derivedPending := by
+  funext h i
+  exact pendingTag_derived _ _
+
+/-- `selected_invocation_completion` with the schedule-derived pending mask. -/
+theorem selected_invocation_completion_derived {K : Type} {Tail : Type v}
+    (gauges : Gauges K) (geometry : HelperRelative gauges)
+    (dataInput dataOutput : Data → Streams K → Streams K)
+    (oldInput oldOutput : Host → Streams K → Streams K)
+    (s : MultiHosting.WindowState Host SourceOwnership.Axis K Bool (Retained K Tail))
+    (oldBank : Host → Streams K) (newBank : Unit) :
+    MultiHosting.onHosts
+        (MultiHosting.remainders derivedPending [event (Tail := Tail) gauges dataInput dataOutput])
+        (relocated gauges dataInput dataOutput (s, newBank)).1 =
+      MultiHosting.onHosts derivedPending
+        (original gauges dataInput dataOutput oldInput oldOutput (s, oldBank)).1 := by
+  rw [← pending_eq_derived]
+  exact selected_invocation_completion gauges geometry dataInput dataOutput oldInput oldOutput
+    s oldBank newBank
+
+end PendingBinding
+
+#print axioms PendingBinding.pendingTag_derived
+#print axioms PendingBinding.pending_eq_derived
+#print axioms PendingBinding.selected_invocation_completion_derived

research/lean-pending-derivation/PendingDerivation.lean

@@ -0,0 +1,106 @@
+import PendingScheduleData
+import OwnershipDatumCore
+
+/-!
+Pending coordinates of the selected invocation, derived from the literal PR442
+schedule instead of supplied by hand.
+
+Level model (PR386 bit geometry, chart `B_port ⊕ I₅₆`): level −1 is span(q),
+which is axis 0; level `l ≥ 0` is the local block `[0,8)` together with the
+exterior route blocks of stages `1..l`. An idle child advancing a pair from
+level `a` to level `b` has pending set `L_b \ L_a`. Its window is the set of
+local invocations strictly after the pair's last local/bridge touch.
+
+What is checked here:
+* every idle event's rank is the size of its derived pending set, and levels nest;
+* the selected stage lies in the window of every hosted child, whose pair is idle;
+* every hosted target mask is the `[offset, offset+width)` slice of its child's
+  ascending derived pending axes.
+
+What is not: the identification of level −1 with span(q) and of these levels
+with the PR386 frames is the stated model, not a theorem here. The schedule and
+blocks are extracted literals (`generate_pending_schedule.py`).
+
+Apache-2.0. Douglas Colkitt, with Claude (Anthropic) assistance.
+-/
+namespace PendingDerivation
+open PendingSchedule
+
+/-- Membership of axis `i` in level `l - 1` (levels are shifted: `0` is level −1). -/
+def inLevel (l i : Nat) : Bool :=
+  if l = 0 then i == 0
+  else i < 8 || (exteriorBlocks.take (l - 1)).any (fun b => b.contains i)
+
+/-- `(pair, rank, source, target)` of the idle child with index `idx`. -/
+def idleData (idx : Nat) : Option (Nat × Nat × Nat × Nat) :=
+  schedule.findSome? fun
+    | .idle j p r s t => if j = idx then some (p, r, s, t) else none
+    | _ => none
+
+/-- Ascending derived pending axes `L_target \ L_source` of an idle child. -/
+def pendingAxes (idx : Nat) : List Nat :=
+  match idleData idx with
+  | some (_, _, s, t) => (List.range 64).filter fun i => inLevel t i && !inLevel s i
+  | none => []
+
+def windowGo (idx p : Nat) : List Event → List Nat → List Nat
+  | [], _ => []
+  | .local s q :: es, acc => if q = p then windowGo idx p es [] else windowGo idx p es (acc ++ [s])
+  | .bridge d s :: es, acc =>
+      if d = p ∨ s = p then windowGo idx p es [] else windowGo idx p es acc
+  | .idle j _ _ _ _ :: es, acc => if j = idx then acc else windowGo idx p es acc
+  | .exchange :: es, acc => windowGo idx p es acc
+
+/-- Stages of the local invocations strictly between the last touch of the
+child's pair and the child. Idle children are not touches. -/
+def window (idx : Nat) : List Nat :=
+  match idleData idx with
+  | some (p, _, _, _) => windowGo idx p schedule []
+  | none => []
+
+def idleConsistent : List Event → Bool
+  | [] => true
+  | .idle idx _ r s t :: es =>
+      s ≤ t && (List.range 64).all (fun i => !inLevel s i || inLevel t i) &&
+        (pendingAxes idx).length == r && idleConsistent es
+  | _ :: es => idleConsistent es
+
+theorem idle_ranks_and_nesting : idleConsistent schedule = true := by decide
+
+theorem top_level_is_ambient : (List.range 64).all (inLevel 9) = true := by decide
+
+theorem pending_child1 : pendingAxes 1 = List.range' 15 7 := by decide
+theorem pending_child2 : pendingAxes 2 = List.range' 1 28 := by decide
+
+/-- Idle child hosting a role tag. -/
+def child (t : SourceOwnership.Tag) : Nat := SourceOwnership.lookup SourceOwnership.tagChild t.val
+
+def derivedPendingTag (t : SourceOwnership.Tag) (i : SourceOwnership.Axis) : Bool :=
+  (pendingAxes (child t)).contains i.val
+
+def derivedTarget (t : SourceOwnership.Tag) (i : SourceOwnership.Axis) : Bool :=
+  (((pendingAxes (child t)).drop (SourceOwnership.lookup SourceOwnership.tagOffset t.val)).take
+    (SourceOwnership.lookup SourceOwnership.tagWidth t.val)).contains i.val
+
+theorem hosted_windows : ∀ t : SourceOwnership.Tag,
+    selectedStage ∈ window (child t) ∧
+      (idleData (child t)).map (·.1) ≠ some selectedPair ∧
+      SourceOwnership.lookup SourceOwnership.tagOffset t.val +
+          SourceOwnership.lookup SourceOwnership.tagWidth t.val ≤ (pendingAxes (child t)).length := by
+  decide
+
+/-- The extracted target masks are exactly slices of the derived pending axes. -/
+theorem target_derived : ∀ (t : SourceOwnership.Tag) (i : SourceOwnership.Axis),
+    SourceOwnership.targetMask t i = derivedTarget t i := by
+  decide +kernel
+
+theorem target_in_derived_pending : ∀ (t : SourceOwnership.Tag) (i : SourceOwnership.Axis),
+    SourceOwnership.targetMask t i = true → derivedPendingTag t i = true := by
+  decide +kernel
+
+end PendingDerivation
+
+#print axioms PendingDerivation.idle_ranks_and_nesting
+#print axioms PendingDerivation.hosted_windows
+#print axioms PendingDerivation.target_derived
+#print axioms PendingDerivation.target_in_derived_pending

research/lean-pending-derivation/PendingScheduleData.lean

@@ -0,0 +1,65 @@
+import Std
+
+/-! Literal PR442 hosted bit schedule and PR434 exterior route blocks.
+Generated by generate_pending_schedule.py from ../lean-multi-host-source/inputs/hosted-template.json.gz
+(uncompressed sha256 dd7833dcaff8c84b258847f4c4d65b6402c702700ae37d2c464083ee37b24126) and inputs/geometry.json.gz
+(uncompressed sha256 fc7b29b16ee754ca9717973b745d6322bbf8351a5e35e3fc9e0fbf7a88dc0317). The extractor is not kernel verified; every
+port's routes agree on the exterior blocks. Idle levels are shifted by one.
+Apache-2.0. Douglas Colkitt, with Claude (Anthropic) assistance. -/
+namespace PendingSchedule
+
+inductive Event where
+  | local (stage pair : Nat)
+  | bridge (dst src : Nat)
+  /-- `idle idx pair rank (sourceLevel + 1) (targetLevel + 1)` -/
+  | idle (idx pair rank source target : Nat)
+  | exchange
+  deriving DecidableEq, Repr
+
+def schedule : List Event := [
+  .local 0 0,
+  .local 1 0,
+  .idle 0 1 14 0 2,
+  .bridge 0 1,
+  .local 2 0,
+  .idle 1 1 7 2 3,
+  .bridge 0 1,
+  .local 3 1,
+  .idle 2 2 28 0 4,
+  .bridge 1 2,
+  .local 4 1,
+  .idle 3 2 7 4 5,
+  .bridge 1 2,
+  .local 5 2,
+  .idle 4 3 42 0 6,
+  .bridge 2 3,
+  .local 6 2,
+  .idle 5 3 7 6 7,
+  .bridge 2 3,
+  .local 7 3,
+  .local 8 3,
+  .idle 6 0 42 3 9,
+  .idle 7 1 28 5 9,
+  .idle 8 2 14 7 9,
+  .idle 9 3 0 9 9,
+  .bridge 3 2,
+  .bridge 2 1,
+  .bridge 1 0,
+  .exchange]
+
+/-- Exterior axes of the stage-s route (s = 1..8), identical for all 120 ports. -/
+def exteriorBlocks : List (List Nat) := [
+  [8, 9, 10, 11, 12, 13, 14],
+  [15, 16, 17, 18, 19, 20, 21],
+  [22, 23, 24, 25, 26, 27, 28],
+  [29, 30, 31, 32, 33, 34, 35],
+  [36, 37, 38, 39, 40, 41, 42],
+  [43, 44, 45, 46, 47, 48, 49],
+  [50, 51, 52, 53, 54, 55, 56],
+  [57, 58, 59, 60, 61, 62, 63]]
+
+/-- The selected invocation of PR540: stage 2, replica 0, pair 0, forward. -/
+def selectedStage : Nat := 2
+def selectedPair : Nat := 0
+
+end PendingSchedule

research/lean-pending-derivation/README.md

@@ -0,0 +1,84 @@
+# PR540's pending ranges, derived in Lean
+
+**Lean companion to [#540](https://github.com/CrocSwap/integer-mult-bounds/pull/540), stacked on its head
+`acc1917034d10f464271ab115fda314fd4eee7a3`. No new κ. No PR540 file is changed.**
+
+PR540's `PhysicalSourceConnection.pendingTag` supplies the pending coordinates of the selected
+invocation (stage 2, replica 0, pair 0) by hand: `[15,22)` for idle child 1 and `[1,29)` for child 2.
+Lean checked only that they contain the target masks. [#1228](https://github.com/CrocSwap/integer-mult-bounds/pull/1228)
+derived them in Python. This package moves that derivation into Lean 4.21 and binds it to PR540's
+actual definition.
+
+## What is proved
+
+From the literal PR442 schedule and route blocks (`PendingScheduleData.lean`), `PendingDerivation.lean` defines:
+
+- **Levels:** `L₋₁ = {0}` and `L_ℓ = [0,8) ∪ E₁ ∪ … ∪ E_ℓ`, with `E_s` the exterior axes of the
+  stage-s route.
+- **Pending axes:** `pendingAxes idx = L_target \ L_source`, ascending.
+- **Windows:** the stages strictly after the pair's last local or bridge touch.
+
+The following are proved by `decide`, using only `propext` and `Quot.sound` (or no axioms):
+
+| Theorem | Statement |
+|---|---|
+| `idle_ranks_and_nesting` | All 10 idle events: levels nest and `|pendingAxes idx| = rank` |
+| `pending_child1`, `pending_child2` | `pendingAxes 1 = [15..21]`, `pendingAxes 2 = [1..28]` |
+| `hosted_windows` | For all 16 tags: stage 2 is in the child's window, the host pair is not pair 0, and `offset+width ≤ |pending|` |
+| `target_derived` | For all tags and axes, `targetMask t i` is the `[offset, offset+width)` slice of the derived pending axes |
+| `PendingBinding.pendingTag_derived` | PR540's `pendingTag t i = derivedPendingTag t i` for all tags and axes |
+| `PendingBinding.pending_eq_derived` | `PhysicalSourceConnection.pending = derivedPending` |
+| `PendingBinding.selected_invocation_completion_derived` | PR540's completion theorem, stated with the derived mask |
+
+As a result, the hand-written ranges and the extractor's hard-coded bases 15 and 1 are no longer
+unchecked premises. Both are equal to schedule-derived definitions inside Lean.
+
+Six mutations each fail because `decide` refutes the mutated statement:
+
+- L₋₁ empty;
+- L₋₁ set to the whole local block;
+- exterior blocks off by one stage;
+- the first two exterior blocks swapped;
+- child 1 advanced before the selected call;
+- child 1 claimed on the previous block.
+
+## Remaining trust boundary
+
+- **Literal data.** `PendingScheduleData.lean` is a Python extraction from the pinned template and
+  geometry, the same boundary as PR540's other literal data. `generate_pending_schedule.py --check`
+  regenerates it byte for byte.
+- **Level model.** The model is a definition. Its agreement with the PR386 frames (in particular
+  L₋₁ = span(q) in the `B_port ⊕ I₅₆` chart) is not proved here. The checks above pin it down only
+  through ranks, nesting and the extracted target masks.
+- **Axis order.** The ascending axis order within a child is the offset convention shared with
+  PR540's extractor.
+- **Scope.** One invocation only. No cover sweep, cost, all-size or κ claim.
+
+## Reproduce
+
+```sh
+cd research/lean-multi-host-source && lake exe cache get Mathlib.Data.Matrix.Mul \
+  Mathlib.Algebra.BigOperators.Fin Mathlib.Tactic.FieldSimp Mathlib.Tactic.Ring Mathlib.Tactic.NormNum
+lake build PhysicalSourceConnection          # PR540's own build; 3.5 min measured with the Mathlib cache
+cd ../.. && python3 research/lean-pending-derivation/verify.py
+```
+
+Building the three new modules takes seconds, and the controls about 15 s. `verify.py` runs the
+generator check, compiles the modules against PR540's build through `lake env`, audits the axioms
+of all seven theorems and runs the controls.
+
+## Open next questions
+
+- **Can the level model be proved from the PR386 frames?** Proving `L_ℓ` from the route identity
+  ρ_(s,q): (P_q, E_s) → (I₈, E_(s−1)) and PR540's port charts would remove the last modelling
+  premise. A first step is to state the route identity for port 0 over PR540's `Address` type. The
+  blocker is that the geometry's rational route matrices are not yet Lean data.
+- **Does this generalise to a second invocation?** `PendingDerivation` is parametric in the tag's
+  child. A second selected call needs its own ownership literals from PR540's extractor.
+
+## Credit
+
+The Lean formalization, ownership literals and identification of this gap are cheesegrader's #540.
+The construction and hosting rule are #434/#442, and the bit geometry is PR386. The Python
+predecessor is #1228. Prepared by Douglas Colkitt with substantial Claude (Anthropic) assistance.
+Apache-2.0.