refactor(varint): read a varint at an offset through Varint.decodeAt?

Tests/Varint.lean

@@ -63,6 +63,16 @@ private def seededInputs : List ByteArray :=
       let x := (s * 73 + j * 151 + j * j * 17) % 384
       if x < 256 then x else x - 128
 
+/-- The offset reader agrees with the model over the tail from `pos`:
+the same value or error, and a position `pos + k` where the model
+consumed `k` bytes. -/
+private def offsetPin (b : ByteArray) (pos : Nat) : Bool :=
+  let tail := (toNatList b).drop pos
+  match decodeAt? b pos, decode? tail with
+  | .ok (v, next), .ok (w, rest) => v.val == w.val && next == pos + (tail.length - rest.length)
+  | .error e, .error f => e == f
+  | _, _ => false
+
 def Varint.run (r : Runner) : IO Unit := do
   r.section "varint" "multiformats/unsigned-varint README.md"
 
@@ -124,6 +134,20 @@ def Varint.run (r : Runner) : IO Unit := do
     (checkModelPins production (values.map encodeB))
   let inputs := shortInputs ++ prefixInputs ++ seededInputs
   r.check s!"harness model pin over {inputs.length} inputs" (checkModelPins production inputs)
+  -- The offset reader: every offset of every input, one past the end
+  -- included, and a varint behind a long run of bytes, which the
+  -- 9-byte window must not read.
+  let offsetCases := (prefixInputs ++ seededInputs).flatMap fun b =>
+    (List.range (b.size + 2)).map fun pos => (b, pos)
+  r.check s!"decodeAt? agrees with decode? at {offsetCases.length} offsets"
+    (offsetCases.all fun (b, pos) => offsetPin b pos)
+  let long := ofNatList (List.replicate 100 0xFF ++ [0xAC, 0x02] ++ List.replicate 100 0x80)
+  r.check "decodeAt? reads 300 at offset 100 of a 202-byte buffer"
+    (match decodeAt? long 100 with
+      | .ok (v, next) => v.val == 300 && next == 102
+      | .error _ => false)
+  r.check "decodeAt? of a continuation run that passes the budget is malformed"
+    (failsWith .malformed (decodeAt? long 102))
   r.check "the model pin reports a wrong decoder"
     (!checkModelPins (α := UVarint) (fun _ => .error .malformed) [ofNatList [0x01]])
 

packages/codec/multiformats/Multiformats/Wire.lean

@@ -83,12 +83,11 @@ theorem takeBytesOk (cap count : Nat) (input payload rest : List Nat)
         omega
     · cases h
 
-/-- The production dependency sees a budget-sized window instead of the whole tail. -/
+/-- The varint at `position`, through the offset reader of
+`codec/varint`, with its error mapped into the multiformats error. -/
 def readVarintAt (input : ByteArray) (position : Nat) :
-    Except Error (Varint.UVarint × Nat) := do
-  let window := input.extract position (min input.size (position + Varint.maxBytes))
-  let (value, used) ← (Varint.decodeB? window).mapError Error.framing
-  .ok (value, position + used)
+    Except Error (Varint.UVarint × Nat) :=
+  (Varint.decodeAt? input position).mapError Error.framing
 
 /-- The available size is checked before a variable-length extraction. -/
 def takeBytesAt (input : ByteArray) (position count cap : Nat) :

packages/codec/proto/Proto/Bytes.lean

@@ -21,12 +21,11 @@ theorem encodeFieldsBModel (fs : Fields) :
     Bytes.toNatList (encodeFieldsB fs) = encodeFields fs :=
   Bytes.toNatListOfNatListOfLt (encodeFields fs) (encodeFieldsBytes fs)
 
-/-- A budget-sized window avoids copying the remaining message for each varint. -/
+/-- The varint at `pos`, through the offset reader of `codec/varint`,
+with its error mapped into the protobuf error. -/
 private def readVarintAt (bs : ByteArray) (pos : Nat) :
-    Except Error (Varint.UVarint × Nat) := do
-  let window := bs.extract pos (min bs.size (pos + Varint.maxBytes))
-  let (v, used) ← (Varint.decodeB? window).mapError Error.framing
-  .ok (v, pos + used)
+    Except Error (Varint.UVarint × Nat) :=
+  (Varint.decodeAt? bs pos).mapError Error.framing
 
 /-- Check the length before extracting a fixed-width or variable payload. -/
 private def takeBytesAt (bs : ByteArray) (pos count : Nat) :

packages/codec/varint/Varint/Bytes.lean

@@ -42,4 +42,26 @@ where
     else .error .truncated
   termination_by maxBytes - i
 
+/-- One varint at byte `pos` of `b`, and the position after it.
+
+A protobuf field, a multihash, or a frame header holds its varints
+inside a larger buffer. `decodeB?` reads from the front of its input,
+so a caller at an offset would have to cut the input first. A cut of
+the whole tail copies the rest of the message for each varint. A
+varint never takes more than `maxBytes` bytes, so this reader cuts a
+window of `maxBytes` bytes at most. The window answers as the whole
+tail would, and the copy stays at 9 bytes for any buffer size.
+
+The errors are the errors of `decodeB?`. A `pos` at or past the end
+of `b` gives an empty window, which is `truncated`. -/
+def decodeAt? (b : ByteArray) (pos : Nat) : Except DecodeError (UVarint × Nat) :=
+  let window := b.extract pos (min b.size (pos + maxBytes))
+  (decodeB? window).map fun (v, used) => (v, pos + used)
+
+-- `decodeAt?` reads at the offset and answers the position after the
+-- varint, here 300 = `0xAC 0x02` at offset 1, so the next byte is at 3.
+#guard match decodeAt? (Bytes.ofNatList [0xFF, 0xAC, 0x02, 0x07]) 1 with
+  | .ok (v, next) => v.val == 300 && next == 3
+  | .error _ => false
+
 end Varint

packages/codec/varint/docs/ARCHITECTURE.md

@@ -15,7 +15,7 @@ error boundary" below.
 | `Varint.lean` | the root module; one import line per public submodule |
 | `Varint/UVarint.lean` | the newtype `structure UVarint where val : Nat` with its proof field, the model core `encode` and `decode?`, and the `Codec UVarint` / `LawfulCodec UVarint` instances; the instances live with the type (ARCHITECTURE §3.2). The 9-byte budget constant `maxBytes` and the value bound `limit` live here, their one home (PRINCIPLES 1.5). The suffix form `decodeEncodeSuffix` and the budget lemma `lengthEncodeLe` live here too, because the proof of the instance law uses them |
 | `Varint/Theorems.lean` | the theorems over the model beyond the instance law (ARCHITECTURE §6): the accepted-input split `encodeDecode`, `encodeNonempty`, and `encodeBytes`, with the spec examples as `example` blocks |
-| `Varint/Bytes.lean` | the production `ByteArray` path, `encodeB` and `decodeB?`; it imports the 9-byte budget constant from `Varint/UVarint.lean` |
+| `Varint/Bytes.lean` | the production `ByteArray` path, `encodeB`, `decodeB?`, and the offset reader `decodeAt?`; it imports the 9-byte budget constant from `Varint/UVarint.lean` |
 
 All declarations live in the `Varint` namespace. The root module
 re-exports the public submodules.
@@ -42,6 +42,12 @@ mechanisms of §3:
   DecodeError (UVarint × Nat)` are the production forms. The `Nat`
   counts the consumed bytes, so a framing layer knows where its
   payload starts.
+- `decodeAt? : ByteArray → Nat → Except DecodeError (UVarint × Nat)`
+  reads the varint at an offset and returns the position after it.
+  It cuts a window of `maxBytes` bytes at most, so a decoder that
+  walks a buffer by position copies 9 bytes per varint. `codec/proto`
+  and `codec/multiformats` read their varints through it and map its
+  error into their own.
 - `Codec UVarint` and `LawfulCodec UVarint` are the instances of
   §3.2. One instance per type, on the wrapped type alone.
 
@@ -133,6 +139,8 @@ The `ByteArray` decoder carries no theorem of its own. The generic
 harness of `base/bytes` pins it to the model over generated inputs, in
 the `decodeB? b = decode? (toNatList b)` shape (ARCHITECTURE §4.2,
 §6; `base/bytes` docs, owned contracts 1 and 2).
+The suite pins `decodeAt? b pos` to `decode?` over the tail of `b`
+from `pos`, at every offset of the generated inputs.
 
 ## What the package must not depend on