[RealAdii]

Summary

codec/varint gains Varint.decodeAt?, the varint reader at an offset of a ByteArray. codec/proto and codec/multiformats read their varints through it. The window of Varint.maxBytes bytes now has one home (PRINCIPLES 1.5).

Closes #66

What changed

• codec/varint: decodeAt? : ByteArray → Nat → Except DecodeError (UVarint × Nat) in Varint/Bytes.lean. It cuts a window of 9 bytes at most and answers the value and the position after the varint. A #guard checks one read at an offset.
• codec/proto: Pb.readVarintAt calls Varint.decodeAt? and maps the error into Error.framing.
• codec/multiformats: Wire.readVarintAt does the same. Its callers in ComponentWire, Multihash, and Cid do not change.
• Tests/Varint.lean: the suite pins decodeAt? b pos to decode? over the tail from pos. It runs every offset of the prefix and seeded inputs, one past the end included. Two more checks read a varint behind 100 bytes and refuse a continuation run past the budget.
• packages/codec/varint/docs/ARCHITECTURE.md: the public surface lists decodeAt?, and the harness paragraph names the offset pin.

Streams.Framing.read stays as it is. It reads from a BufReader through r.peek Varint.maxBytes, and the peek already holds the window. It has no ByteArray offset for decodeAt? to take.

Test plan

• lake build (every package, on the pinned toolchain) is green.
• lake test passes, and passes again under +RTS -N1.
• The import-rule lint is green (ARCHITECTURE.md §2).
• A new codec or framing layer comes with its round-trip theorem or
  property test, and with a test for its length cap.
• If this touches wire behavior: the captured vectors still pass,
  and the description names the spec section the change follows.
• If this touches the go interop path: the interop matrix
  (PLAN W5.9) is green.

Risk / trust footprint

none

Notes for reviewers

decodeAt? returns the position after the varint, as the two readVarintAt callers used it, and decodeB? keeps the consumed count. The proto and multiformats suites pin both decoders to their models, so they cover the swap.

LICENSE (LGPL version 3)

• I have read and accepted LICENSE (LGPL version 3), NOTICE and CLA in the root of this project.

🤖 Generated with Claude Code

[IvanAnishchuk]

Good work. This is what #66 asked for: Varint.decodeAt? with the signature and home the issue named, both by-hand window cuts gone (Proto/Bytes.lean and Multiformats/Wire.lean), the behaviour unchanged, and the offset pin at every position of the generated inputs. Leaving Streams.Framing as it is makes sense, since its window comes from BufReader.peek.

One line still describes the old shape. packages/codec/proto/docs/ARCHITECTURE.md, line 184, says the production decoder "gives the varint dependency a window bounded by that dependency's byte budget". After this change codec/varint cuts the window, and proto reads each varint through Varint.decodeAt?. The sentence should say that, in this PR.