interval: budget canonical-table gcd work

HexInterval/Experiment/RationalTable.lean

@@ -288,12 +288,15 @@ structure Cost where
   denominatorBits : Nat
   deriving DecidableEq, Repr
 
-/-- Caller-owned limits for the first raw-table boundary.  Arithmetic temporary
-work and wire bytes belong to later phases and are not guessed here. -/
+/-- Caller-owned limits for the first raw-table boundary.  GCD input size and
+aggregate GCD work are independent of retained endpoint size.  Arithmetic
+temporary work and wire bytes belong to later phases and are not guessed here. -/
 structure Limit where
   maxEntries : Nat
   maxNumeratorBits : Nat
   maxDenominatorBits : Nat
+  maxGcdInputBits : Nat
+  maxGcdWork : Nat
   deriving DecidableEq, Repr
 
 /-- Semantic canonicality required of an admitted raw endpoint. -/
@@ -305,6 +308,15 @@ def cost (q : RawRat) : Cost :=
   { numeratorBits := EndpointCost.natBits q.num.natAbs
     denominatorBits := EndpointCost.natBits q.den }
 
+/-- Largest bit width presented to the canonicality GCD. -/
+def Cost.gcdInputBits (size : Cost) : Nat :=
+  max size.numeratorBits size.denominatorBits
+
+/-- Conservative nonzero work charged for one canonicality GCD.  Giving zero
+a one-unit cost ensures that every `Nat.gcd` invocation consumes budget. -/
+def Cost.gcdWork (size : Cost) : Nat :=
+  max 1 size.numeratorBits * max 1 size.denominatorBits
+
 /-- Logical malformed-entry reasons. -/
 inductive Invalid where
   | zeroDenominator
@@ -316,6 +328,8 @@ inductive Resource where
   | entries
   | numeratorBits
   | denominatorBits
+  | gcdInputBits
+  | gcdWork
   deriving DecidableEq, Repr
 
 /-- Result of validating one entry. -/
@@ -325,13 +339,18 @@ inductive EntryResult where
   | resourceLimit (reason : Resource)
   deriving DecidableEq, Repr
 
-/-- Validate retained size first, then positivity and reduced form. -/
-def check (limit : Limit) (q : RawRat) : EntryResult :=
+/-- Validate retained size and GCD resources before positivity and reduced
+form.  `remainingGcdWork` is owned and threaded by the whole-table checker. -/
+def check (limit : Limit) (remainingGcdWork : Nat) (q : RawRat) : EntryResult :=
   let size := q.cost
   if size.numeratorBits > limit.maxNumeratorBits then
     .resourceLimit .numeratorBits
   else if size.denominatorBits > limit.maxDenominatorBits then
     .resourceLimit .denominatorBits
+  else if size.gcdInputBits > limit.maxGcdInputBits then
+    .resourceLimit .gcdInputBits
+  else if size.gcdWork > remainingGcdWork then
+    .resourceLimit .gcdWork
   else if q.den = 0 then
     .malformed .zeroDenominator
   else if q.num.natAbs.gcd q.den = 1 then
@@ -340,22 +359,25 @@ def check (limit : Limit) (q : RawRat) : EntryResult :=
     .malformed .notReduced
 
 /-- A ready entry has a positive, coprime denominator. -/
-theorem canonical_of_check {limit : Limit} {q : RawRat}
-    (h : q.check limit = .ready) : q.Canonical := by
+theorem canonical_of_check {limit : Limit} {remainingGcdWork : Nat} {q : RawRat}
+    (h : q.check limit remainingGcdWork = .ready) : q.Canonical := by
   unfold check at h
   dsimp only at h
   split at h <;> try contradiction
   split at h <;> try contradiction
   split at h <;> try contradiction
+  split at h <;> try contradiction
+  split at h <;> try contradiction
   rename_i hden
   split at h <;> try contradiction
   rename_i hcop
   exact ⟨hden, hcop⟩
 
 /-- A ready raw endpoint interprets to the same canonical numerator and
 denominator that were checked. -/
-theorem value_fields {limit : Limit} {q : RawRat}
-    (h : q.check limit = .ready) : q.value.num = q.num ∧ q.value.den = q.den := by
+theorem value_fields {limit : Limit} {remainingGcdWork : Nat} {q : RawRat}
+    (h : q.check limit remainingGcdWork = .ready) :
+    q.value.num = q.num ∧ q.value.den = q.den := by
   have hc := canonical_of_check h
   have hvalue : q.value = Rat.mk' q.num q.den hc.1 hc.2 := by
     exact (Rat.mk_eq_mkRat q.num q.den hc.1 hc.2).symm
@@ -374,32 +396,35 @@ inductive Result where
   | resourceLimit (index : Option Nat) (reason : RawRat.Resource)
   deriving DecidableEq, Repr
 
-/-- Validate every entry in order after bounded collection preflight. -/
-def checkFrom (limit : RawRat.Limit) : Nat → List RawRat → Result
-  | _, [] => .ready
-  | index, entry :: tail =>
-      match entry.check limit with
-      | .ready => checkFrom limit (index + 1) tail
+/-- Validate every entry in order after bounded collection preflight, consuming
+the caller-owned aggregate GCD budget only after each successful entry. -/
+def checkFrom (limit : RawRat.Limit) : Nat → Nat → List RawRat → Result
+  | _, _, [] => .ready
+  | index, remainingGcdWork, entry :: tail =>
+      match entry.check limit remainingGcdWork with
+      | .ready =>
+          checkFrom limit (index + 1) (remainingGcdWork - entry.cost.gcdWork) tail
       | .malformed reason => .malformed index reason
       | .resourceLimit reason => .resourceLimit (some index) reason
 
 /-- Validate an untrusted table under caller-owned entry and endpoint limits.
 The bounded length check precedes the whole-table scan. -/
 def check (limit : RawRat.Limit) (entries : List RawRat) : Result :=
   if lengthWithin limit.maxEntries entries then
-    checkFrom limit 0 entries
+    checkFrom limit 0 limit.maxGcdWork entries
   else
     .resourceLimit none .entries
 
 /-- A ready suffix scan contains only canonical raw endpoints. -/
 theorem canonical_of_checkFrom {limit : RawRat.Limit} {entries : List RawRat}
-    {index : Nat} (h : checkFrom limit index entries = .ready) :
+    {index remainingGcdWork : Nat}
+    (h : checkFrom limit index remainingGcdWork entries = .ready) :
     ∀ q ∈ entries, q.Canonical := by
-  induction entries generalizing index with
+  induction entries generalizing index remainingGcdWork with
   | nil => simp
   | cons head tail ih =>
       simp only [checkFrom] at h
-      cases hhead : head.check limit with
+      cases hhead : head.check limit remainingGcdWork with
       | ready =>
           simp only [hhead] at h
           intro q hq
@@ -429,7 +454,9 @@ end Table
 def fixtureTableLimit : RawRat.Limit :=
   { maxEntries := 5
     maxNumeratorBits := 8
-    maxDenominatorBits := 8 }
+    maxDenominatorBits := 8
+    maxGcdInputBits := 8
+    maxGcdWork := 64 }
 
 /-- An accepted table including canonical zero, negative, and non-dyadic
 values. -/
@@ -456,7 +483,14 @@ def checksTable : Bool :=
       [⟨2, 6⟩, ⟨256, 1⟩] == .malformed 0 .notReduced &&
     Table.check { fixtureTableLimit with maxDenominatorBits := 8 }
       (fixtureTable ++ [⟨1, 256⟩]) ==
-        .resourceLimit (some 4) .denominatorBits
+        .resourceLimit (some 4) .denominatorBits &&
+    Table.check { fixtureTableLimit with maxGcdInputBits := 7 } [⟨1, 255⟩] ==
+      .resourceLimit (some 0) .gcdInputBits &&
+    Table.check { fixtureTableLimit with maxGcdWork := 5 }
+      [⟨0, 1⟩, ⟨1, 2⟩, ⟨1, 3⟩] == .ready &&
+    Table.check { fixtureTableLimit with maxGcdWork := 4 }
+      [⟨0, 1⟩, ⟨1, 2⟩, ⟨1, 3⟩] ==
+        .resourceLimit (some 2) .gcdWork
 
 /-- Ordinary-kernel canary for canonical whole-table validation. -/
 theorem checksTable_eq_true : checksTable = true := by

HexInterval/SPEC/hex-interval.md

@@ -378,10 +378,15 @@ telemetry contract, not a claim about GMP or kernel wall time.
 Whole-table canonicality has its own `maxGcdInputBits` and `maxGcdWork` caps.
 Input-size and work preflight occur before calling `Nat.gcd` for every entry,
 including an unused tail. The first conservative gcd work unit may be the
-product of numerator and denominator bit lengths; alternative Euclidean-step
-models are benchmark candidates. Retained table bits, per-edge peak temporary
-bits, aggregate arithmetic work, and representation-level lookup work are
-distinct limits.
+product `max(1, numeratorBits) * max(1, denominatorBits)`, so canonical zero
+and every other gcd invocation consume nonzero work. The reference checker
+requires each input width to fit `maxGcdInputBits`, then requires this cost to
+fit the remaining caller-owned aggregate budget before invoking `Nat.gcd`.
+After a ready entry it subtracts the cost and proceeds in table order;
+`maxGcdWork` exhaustion therefore reports the first entry whose gcd cannot be
+run. Alternative Euclidean-step models are benchmark candidates. Retained
+table bits, per-edge peak temporary bits, aggregate arithmetic work, and
+representation-level lookup work are distinct limits.
 
 Every *endpoint-table* traversal is accounted for. The transparent `List`
 reference checker charges exact forward distance for literal and finite-cut
@@ -431,14 +436,15 @@ later entry. The target pipeline uses these phases:
    edge.
 
 The current `RationalTable.Table.check` experiment implements the collection
-cap and the per-entry numerator/denominator/canonicality portion of phases 2
-and 3. It intentionally does not yet expose an independent encoded-byte or gcd
-work cap. `RationalCertificate.Certificate.check` adds canonical-table,
-endpoint-reference, caller-boundary, structural, and exact endpoint-lookup
-validation from phases 2 and 4. Arithmetic edges and projection implement the
-remaining preflight/replay pieces in separate experimental modules before
-they are composed. Thus declared limits below describe the composed target;
-they are not a claim that the first table module already exposes every field.
+cap and the per-entry numerator/denominator/gcd/canonicality portions of phases
+2 and 3, including caller-owned gcd input and aggregate work caps. It does not
+yet expose an independent encoded-byte cap. `RationalCertificate.Certificate.check`
+adds canonical-table, endpoint-reference, caller-boundary, structural, and
+exact endpoint-lookup validation from phases 2 and 4. Arithmetic edges and
+projection implement the remaining preflight/replay pieces in separate
+experimental modules before they are composed. Thus declared limits below
+describe the composed target; they are not a claim that the first table module
+already exposes every field.
 
 Failures distinguish resource limits from malformed certificates. Resource
 reasons include collection entries, encoded bytes, numerator/denominator bits,

conformance/HexInterval/RationalTableConformance.lean

@@ -128,10 +128,42 @@ example : checksErasure = true := by
 #guard Table.check { fixtureTableLimit with maxDenominatorBits := 8 }
   (fixtureTable ++ [⟨1, 256⟩]) == .resourceLimit (some 4) .denominatorBits
 
+-- The GCD input cap is separate from retained endpoint caps and is exact.
+#guard Table.check { fixtureTableLimit with maxGcdInputBits := 8 } [⟨1, 255⟩] ==
+  .ready
+#guard Table.check { fixtureTableLimit with maxGcdInputBits := 7 } [⟨1, 255⟩] ==
+  .resourceLimit (some 0) .gcdInputBits
+
+-- Every GCD consumes nonzero work, including canonical zero.  The aggregate
+-- budget is consumed in table order and reports the first entry it cannot run.
+#guard Table.check { fixtureTableLimit with maxGcdWork := 1 } [⟨0, 1⟩] == .ready
+#guard Table.check { fixtureTableLimit with maxGcdWork := 0 } [⟨0, 1⟩] ==
+  .resourceLimit (some 0) .gcdWork
+#guard Table.check { fixtureTableLimit with maxGcdWork := 5 }
+  [⟨0, 1⟩, ⟨1, 2⟩, ⟨1, 3⟩] == .ready
+#guard Table.check { fixtureTableLimit with maxGcdWork := 4 }
+  [⟨0, 1⟩, ⟨1, 2⟩, ⟨1, 3⟩] ==
+    .resourceLimit (some 2) .gcdWork
+
+-- Complete traversal charges an otherwise unused tail.  Its exact input fits,
+-- but one-short aggregate work fails at that tail's index.
+#guard Table.check { fixtureTableLimit with maxGcdWork := 9 }
+  [⟨1, 1⟩, ⟨1, 255⟩] == .ready
+#guard Table.check { fixtureTableLimit with maxGcdWork := 8 }
+  [⟨1, 1⟩, ⟨1, 255⟩] == .resourceLimit (some 1) .gcdWork
+
+-- GCD resource preflight precedes logical validation within one entry, while
+-- a bounded logical failure at an earlier entry still wins over later work.
+#guard Table.check { fixtureTableLimit with maxGcdWork := 0 } [⟨0, 0⟩] ==
+  .resourceLimit (some 0) .gcdWork
+#guard Table.check { fixtureTableLimit with maxGcdWork := 6 }
+  [⟨2, 6⟩, ⟨1, 255⟩] == .malformed 0 .notReduced
+
 -- Successful validation reconstructs exactly the checked Core numerator and
 -- denominator; it does not silently replace the raw encoding.
 example : (RawRat.value ⟨-1, 3⟩).num = -1 ∧ (RawRat.value ⟨-1, 3⟩).den = 3 := by
-  exact RawRat.value_fields (limit := fixtureTableLimit) (by decide +kernel)
+  exact RawRat.value_fields (limit := fixtureTableLimit)
+    (remainingGcdWork := fixtureTableLimit.maxGcdWork) (by decide +kernel)
 
 example : checksTable = true := by
   decide +kernel

progress/20260727T111936Z.md

@@ -0,0 +1,32 @@
+# Accomplished
+
+- Added independent caller-owned GCD input-width and aggregate-work limits to
+  the canonical raw rational table boundary.
+- Made each entry preflight retained sizes, both GCD input widths, and its
+  remaining nonzero GCD work charge before either logical validation or
+  `Nat.gcd`; table traversal now consumes that budget deterministically in
+  entry order.
+- Preserved the first-failing-index result and canonicality/value theorems
+  across the budget-threading API change.
+- Added exact and one-short conformance for GCD input, single-entry and
+  aggregate work, canonical zero, zero denominator ordering, and an otherwise
+  unused tail.
+- Updated the rational cost model in the SPEC and verified the focused table,
+  certificate, experiment, and downstream conformance targets. Forbidden-token
+  and whitespace checks pass.
+
+# Current frontier
+
+The raw table now accounts for every canonicality GCD under a conservative
+nonzero work proxy. Encoded-byte decoding limits and arithmetic-edge GCDs are
+separate later boundaries.
+
+# Next step
+
+Stack this commit under the rational planner/edge/projection branches and
+update their table-limit literals for the two new fields while resolving any
+expected API conflicts around `RawRat.check`.
+
+# Blockers
+
+None.