[ls-python] expose range values at boundary

Author: thomasahle

CHANGELOG.md

@@ -36,6 +36,13 @@ change is listed here under **Changed** or **Removed**.
   differential suite now has **2,664 / 3,025 rows = 88.1% matched**, or
   **88.1% complete**, with **100% agreement among decided rows**.
 
+- `range` values now cross the public call boundary as structural
+  `Val.range` snapshots. The boundary preserves each constructor field's
+  integer-or-Boolean form while the runner compares CPython's normalized
+  integer attributes. The differential suite now has **2,665 / 3,025 rows =
+  88.1% matched**, or **88.1% complete** (proof interpreter: **2,592 / 3,025
+  = 85.7%**), with **100% agreement among decided rows**.
+
 ## [0.1.9] — 2026-10-11
 
 ### Added

Examples/python/seq_lab/seq_lab.py

@@ -2,8 +2,8 @@
 
 Tuple/namedtuple slices, tuple repetition, sum(it[, start]), tuple(it),
 and range as an immediate value (materialize-per-use). Range equality now
-compares sequences without materialization; the remaining loud frontier is
-pinned by refusal probes: boundary and list slices. String repetition now
+compares sequences without materialization; range values cross the public
+boundary, while list slices remain pinned by a refusal probe. String repetition now
 has its own acceptance tier.
 """
 

Examples/python/seq_lab/spec.lean

@@ -8,9 +8,9 @@ repetition, `sum(it[, start])` (the element fold IS `evalBinOp .add`; a
 str start is CPython's special-cased `TypeError`), `tuple(it)`, and
 `range` as the immediate `RVal.rangeV` — materialize-per-use, which is
 what makes RE-ITERATION exact (`range_reiter`). Range equality compares the
-integer sequence without materializing it. The remaining loud frontier is
-pinned below: range indexing/membership/unpacking/boundary, list slices —
-every one `unsupported`, never a guessed value
+integer sequence without materializing it. Range values also cross the public
+boundary as `Val.range`; list slices remain pinned below as `unsupported`,
+never a guessed value
 and never a fake `TypeError`.
 -/
 
@@ -93,10 +93,10 @@ load_program seq_lab from "Examples/python/seq_lab/seq_lab.json"
 #py_check seq_lab.range_in_float() = true
 #py_check seq_lab.range_in_fraction() = false
 
-/-! ### the remaining loud range frontier (unsupported, never guessed) -/
+/-! ### range values at the public boundary -/
 
-#guard (match callFunction seq_lab "range_boundary" #[.int 3] 4096 with
-  | .unsupported _ => true | _ => false)
+#guard callFunction seq_lab "range_boundary" #[.int 3] 4096 ==
+  .ok (.range (.int 0) (.int 3) (.int 1))
 #py_check seq_lab.range_unpack() = 0
 #py_check seq_lab.range_unpack_step() = 5
 #py_check seq_lab.range_unpack_bad() raises

LeanModels/Python/Ast.lean

@@ -421,6 +421,19 @@ def benignImportBinds : String → Option (String × Bool)
 
 /-! ## Core value / result types (DESIGN.md, normative) -/
 
+/-- The integer object retained by a public `range` value, including bool
+subclasses.  Runtime range values use the same representation, so freezing
+and thawing preserve the constructor fields exactly. -/
+inductive RangeBound where
+  | int (value : Int)
+  | bool (value : Bool)
+deriving Repr, Inhabited, BEq
+
+/-- The numerical interpretation used by range consumers. -/
+def RangeBound.toInt : RangeBound → Int
+  | .int value => value
+  | .bool value => if value then 1 else 0
+
 /-- Runtime values. -/
 inductive Val where
   | none
@@ -429,6 +442,8 @@ inductive Val where
   | int (n : Int)
   | float (value : Float64)
   | str (s : String)
+  /-- A Python `range` value at the public call boundary. -/
+  | range (lo hi step : RangeBound)
   | list (xs : Array Val)
   | tuple (xs : Array Val)
 deriving Repr, Inhabited, BEq

LeanModels/Python/Runtime.lean

@@ -27,17 +27,6 @@ namespace LeanModels.Python
 /-- A heap address (the index into the heap array). -/
 abbrev Addr := Nat
 
-/-- The integer object retained by a range constructor, including bool subclasses. -/
-inductive RangeBound where
-  | int (value : Int)
-  | bool (value : Bool)
-deriving Repr, Inhabited, BEq
-
-/-- The numerical interpretation used by range consumers. -/
-def RangeBound.toInt : RangeBound → Int
-  | .int value => value
-  | .bool value => if value then 1 else 0
-
 /-- Runtime values (docs/memory-model.md v2). -/
 inductive RVal where
   | none
@@ -622,6 +611,7 @@ mutual
     | .int n => .int n
     | .float value => .float value
     | .str s => .str s
+    | .range lo hi step => .rangeV lo hi step
     | .list xs => .listV (RVal.thawList xs.toList).toArray
     | .tuple xs => .tuple (RVal.thawList xs.toList).toArray
 
@@ -646,6 +636,7 @@ mutual
     | .int n => .ok (.int n)
     | .float value => .ok (.float value)
     | .str s => .ok (.str s)
+    | .rangeV lo hi step => .ok (.range lo hi step)
     | .listV xs => do
         let vs ← RVal.freezeList xs.toList
         return .list vs.toArray
@@ -654,8 +645,6 @@ mutual
         return .tuple vs.toArray
     | .ntuple _ _ _ =>
         .unsupported "returning a namedtuple through the call boundary is outside the tier (no namedtuple observation form in `Val`; a tuple snapshot would silently forget the class — docs/memory-model.md §class semantics)"
-    | .rangeV .. =>
-        .unsupported "returning a range through the call boundary is outside the tier (no range observation form in `Val`; docs/memory-model.md §module-init execution)"
     | .ref _ =>
         .unsupported "returning a heap object through the call boundary is outside the tier (H1-proper freeze, docs/memory-model.md)"
 
@@ -684,6 +673,7 @@ mutual
     | .int _ => rfl
     | .float _ => rfl
     | .str _ => rfl
+    | .range _ _ _ => rfl
     | .list xs => by
         simp [RVal.thaw, RVal.freeze, RVal.freezeList_thawList xs.toList]
     | .tuple xs => by
@@ -716,6 +706,8 @@ mutual
         cases (Res.ok.inj h); rfl
     | .str _, v, h => by
         cases (Res.ok.inj h); rfl
+    | .rangeV lo hi step, v, h => by
+        cases (Res.ok.inj h); rfl
     | .listV xs, v, h => by
         simp only [RVal.freeze, Res.bind_eq_ok, Res.pure_eq] at h
         obtain ⟨vs, hl, hv⟩ := h
@@ -865,7 +857,7 @@ mutual
   recursively). On this fragment thawing is pure — the bridge every
   pre-H2 boundary statement rides. Kernel-computable (list-structural). -/
   def Val.listFree : Val → Bool
-    | .none | .ellipsis | .bool _ | .int _ | .float _ | .str _ => true
+    | .none | .ellipsis | .bool _ | .int _ | .float _ | .str _ | .range _ _ _ => true
     | .list _ => false
     | .tuple xs => Val.listFreeList xs.toList
 
@@ -893,6 +885,7 @@ mutual
     | .int n => (h, .int n)
     | .float value => (h, .float value)
     | .str s => (h, .str s)
+    | .range lo hi step => (h, .rangeV lo hi step)
     | .tuple xs =>
       match RVal.thawListH h xs.toList with
       | (h, vs) => (h, .tuple vs.toArray)
@@ -928,6 +921,7 @@ mutual
     | .int _, _, h => rfl
     | .float _, _, h => rfl
     | .str _, _, h => rfl
+    | .range _ _ _, _, h => rfl
     | .tuple xs, hf, h => by
         simp only [RVal.thawH, RVal.thaw,
           RVal.thawListH_of_listFree xs.toList (by simpa [Val.listFree] using hf) h]
@@ -1002,8 +996,7 @@ mutual
             return .tuple vs.toArray
         | .ntuple _ _ _ =>
             .unsupported "returning a namedtuple through the call boundary is outside the tier (no namedtuple observation form in `Val`; a tuple snapshot would silently forget the class — docs/memory-model.md §class semantics)"
-        | .rangeV .. =>
-            .unsupported "returning a range through the call boundary is outside the tier (no range observation form in `Val`; docs/memory-model.md §module-init execution)"
+        | .rangeV lo hi step => .ok (.range lo hi step)
         | .ref a =>
           if path.contains a then
             .unsupported "returning a CYCLIC heap object through the call boundary is outside the tier (no cyclic observation form in `Val`; docs/memory-model.md §call layering)"
@@ -1065,8 +1058,7 @@ mutual
         return .tuple vs.toArray
     | .ntuple _ _ _ =>
         .unsupported "returning a namedtuple through the call boundary is outside the tier (no namedtuple observation form in `Val`; a tuple snapshot would silently forget the class — docs/memory-model.md §class semantics)"
-    | .rangeV .. =>
-        .unsupported "returning a range through the call boundary is outside the tier (no range observation form in `Val`; docs/memory-model.md §module-init execution)"
+    | .rangeV lo hi step => .ok (.range lo hi step)
     | .ref a => RVal.freezeH h fuel [] (.ref a)
 
   /-- Elementwise `freezeB`, first refusal wins. -/
@@ -1092,6 +1084,7 @@ mutual
     | .int _ => rfl
     | .float _ => rfl
     | .str _ => rfl
+    | .range _ _ _ => rfl
     | .list xs => by
         simp only [RVal.thaw, RVal.freezeB,
           RVal.freezeListB_thawList h fuel xs.toList, Res.ok_bind, Res.pure_eq]
@@ -1146,6 +1139,7 @@ mutual
     | .int _ => rfl
     | .float _ => rfl
     | .str _ => rfl
+    | .range _ _ _ => rfl
     | .list xs => by
         simpa [RVal.thaw, RVal.refFree] using
           RVal.refFreeList_thawList xs.toList
@@ -1334,7 +1328,10 @@ theorem RVal.eq_thaw_of_freezeH_pair (h : Heap) (fuel : Nat) :
       | int n => simp only [RVal.freezeH] at hc; cases (Res.ok.inj hc); rfl
       | float value => simp only [RVal.freezeH] at hc; cases (Res.ok.inj hc); rfl
       | str s => simp only [RVal.freezeH] at hc; cases (Res.ok.inj hc); rfl
-      | rangeV lo hi step => simp [RVal.freezeH] at hc
+      | rangeV lo hi step =>
+        simp only [RVal.freezeH] at hc
+        cases (Res.ok.inj hc)
+        rfl
       | listV xs =>
         -- the snapshot is a `.list` — excluded by `hlf`
         simp only [RVal.freezeH, Res.bind_eq_ok, Res.pure_eq] at hc
@@ -1401,6 +1398,7 @@ mutual
     | .int _, v, hc, _ => by cases (Res.ok.inj hc); rfl
     | .float _, v, hc, _ => by cases (Res.ok.inj hc); rfl
     | .str _, v, hc, _ => by cases (Res.ok.inj hc); rfl
+    | .rangeV lo hi step, v, hc, _ => by cases (Res.ok.inj hc); rfl
     | .listV xs, v, hc, hlf => by
         simp only [RVal.freezeB, Res.bind_eq_ok, Res.pure_eq] at hc
         obtain ⟨vs, _, hv⟩ := hc

LeanModels/Python/Semantics.lean

@@ -98,6 +98,7 @@ def Val.typeName : Val → String
   | .int _ => "int"
   | .float _ => "float"
   | .str _ => "str"
+  | .range _ _ _ => "range"
   | .list _ => "list"
   | .tuple _ => "tuple"
 

Main.lean

@@ -228,6 +228,10 @@ partial def valJson : Val → String
   | .int n => "{\"t\":\"int\",\"v\":" ++ jsonStr (toString n) ++ "}"
   | .float value => "{\"t\":\"float\",\"bits\":" ++ jsonStr (toString value.bits.toNat) ++ "}"
   | .str s => "{\"t\":\"str\",\"v\":" ++ jsonStr s ++ "}"
+  | .range lo hi step =>
+      "{\"t\":\"range\",\"lo\":" ++ jsonStr (toString lo.toInt) ++
+        ",\"hi\":" ++ jsonStr (toString hi.toInt) ++
+        ",\"step\":" ++ jsonStr (toString step.toInt) ++ "}"
   | .list xs => "{\"t\":\"list\",\"v\":[" ++ ",".intercalate (xs.toList.map valJson) ++ "]}"
   | .tuple xs => "{\"t\":\"tuple\",\"v\":[" ++ ",".intercalate (xs.toList.map valJson) ++ "]}"
 

docs/memory-model.md

@@ -3105,8 +3105,9 @@ each construct differential, refusals loud):
   scalar renderer; numerical consumers use `RangeBound.toInt`. Thus
   `range(False, True)` renders those Boolean names but yields integer `0`.
   A retained Boolean `True` step is numerically one and omitted from rendering;
-  `False` still fails construction. Attribute access, slicing,
-  range-valued `%` conversions, and the public boundary are not newly admitted.
+  `False` still fails construction. Attribute access, slicing, and
+  range-valued `%` conversions remain loud; ranges now cross the public
+  boundary as a structural `Val.range` snapshot.
 
 **What stays out, loudly:** `.items()` outside the init shell;
 `dict.keys/.values`; the call-mutation gap where an attempt was REFUSED

docs/python-coverage.md

@@ -10,17 +10,17 @@ What the Lean model of Python runs, measured. Everything outside the modelled ti
 
 | rows | agree with CPython | disagree | recorded refusals |
 |---:|---:|---:|---:|
-| 3025 | 2664 | 0 | 361 |
+| 3025 | 2665 | 0 | 360 |
 
-Of the 2664 rows the model decides, 2664 agree with CPython (100.0%). A *recorded refusal* is a row kept in the suite to pin a known gap: the model must refuse it, and the suite fails if it ever answers instead.
+Of the 2665 rows the model decides, 2665 agree with CPython (100.0%). A *recorded refusal* is a row kept in the suite to pin a known gap: the model must refuse it, and the suite fails if it ever answers instead.
 
 ### What the theorems can see
 
 The rows above run through the runner's interpreter (`LeanModels/Python/Monadic/`). Theorems are stated about a second definition, `LeanModels/Python/Semantics.lean`, whose tier is narrower ([python-architecture.md](python-architecture.md)). `diff_test.py --proof-interpreter` runs the same rows through it; a refusal there is allowed, a wrong answer is not.
 
 | rows | agree with CPython | disagree | refused |
 |---:|---:|---:|---:|
-| 3025 | 2591 | 0 | 434 |
+| 3025 | 2592 | 0 | 433 |
 
 ## Grammar
 

harness/cases.json

@@ -408,7 +408,7 @@
   {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_in_step", "args": [[]], "expect": "match"},
   {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_in_float", "args": [[]], "expect": "match"},
   {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_in_fraction", "args": [[]], "expect": "match"},
-  {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_boundary", "args": [[3]], "expect": "unsupported"},
+  {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_boundary", "args": [[3]], "expect": "match"},
   {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_unpack", "args": [[]], "expect": "match"},
   {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_unpack_step", "args": [[]], "expect": "match"},
   {"file": "Examples/python/seq_lab/seq_lab.py", "function": "range_unpack_bad", "args": [[]], "expect": "match"},