From 41a42c57c6c4a5956eda0b70c25a1c96a318baaf Mon Sep 17 00:00:00 2001 From: RealAdii <153971735+RealAdii@users.noreply.github.com> Date: Tue, 10 Nov 2026 20:10:09 +0530 Subject: [PATCH] refactor(varint): read a varint at an offset through Varint.decodeAt? codec/proto and codec/multiformats each cut a window of Varint.maxBytes bytes before they call Varint.decodeB?. The window now lives in codec/varint as decodeAt?, which answers the value and the position after the varint. Both readVarintAt helpers call it and map its error into their own. The varint suite pins decodeAt? to decode? over the tail from every offset of the generated inputs. Closes #66 --- Tests/Varint.lean | 24 +++++++++++++++++++ .../codec/multiformats/Multiformats/Wire.lean | 9 ++++--- packages/codec/proto/Proto/Bytes.lean | 9 ++++--- packages/codec/varint/Varint/Bytes.lean | 22 +++++++++++++++++ packages/codec/varint/docs/ARCHITECTURE.md | 10 +++++++- 5 files changed, 63 insertions(+), 11 deletions(-) diff --git a/Tests/Varint.lean b/Tests/Varint.lean index 2fda6886..e3ab1f25 100644 --- a/Tests/Varint.lean +++ b/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]]) diff --git a/packages/codec/multiformats/Multiformats/Wire.lean b/packages/codec/multiformats/Multiformats/Wire.lean index 1dcf9540..3a564745 100644 --- a/packages/codec/multiformats/Multiformats/Wire.lean +++ b/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) : diff --git a/packages/codec/proto/Proto/Bytes.lean b/packages/codec/proto/Proto/Bytes.lean index bb702756..5f4ce608 100644 --- a/packages/codec/proto/Proto/Bytes.lean +++ b/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) : diff --git a/packages/codec/varint/Varint/Bytes.lean b/packages/codec/varint/Varint/Bytes.lean index 9a9f7b0c..430187ed 100644 --- a/packages/codec/varint/Varint/Bytes.lean +++ b/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 diff --git a/packages/codec/varint/docs/ARCHITECTURE.md b/packages/codec/varint/docs/ARCHITECTURE.md index f01b170b..6b2b6a34 100644 --- a/packages/codec/varint/docs/ARCHITECTURE.md +++ b/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