/-
SilverSight.Semantics.View

A View is a structured value read from a byte range without copying the
underlying buffer. The Core defines the address-arithmetic contract; the
zero-copy property is a theorem about offsets and schema sizes.

Only fixed-size Core schemas have built-in accessors. Variable-length views
are a library extension that must preserve the same address-arithmetic
invariant.
-/

import SilverSight.Semantics.Schema

namespace SilverSight.Semantics

/-- A zero-copy view of a fixed-size schema value inside a byte buffer.

    `valid` is the address-arithmetic invariant: the schema's byte range
    fits entirely inside the buffer starting at `offset`. -/
structure View (α : Type) [Schema α] where
  base   : ByteArray
  offset : Nat
  valid  : offset + byteSize α ≤ base.size

namespace View

/-- Read a UInt8 through a one-byte view. The result is the byte at the
    view's offset; no copy of the underlying buffer occurs. -/
def readUInt8 (v : View UInt8) : UInt8 :=
  v.base.get v.offset (by
    have h : byteSize UInt8 = 1 := rfl
    have hv := v.valid
    omega
  )

/-- Reading a UInt8 view returns exactly the byte at the stored offset. -/
@[simp]
theorem readUInt8_eq_get (v : View UInt8) :
    readUInt8 v = v.base.get v.offset (by
      have h : byteSize UInt8 = 1 := rfl
      have hv := v.valid
      omega
    ) := rfl

end View

end SilverSight.Semantics
