/-
SilverSight.Semantics.WireFormat

A WireFormat is a certified encoder/decoder pair for a fixed-size Schema
under a specific Layout. The `roundTrip` field is a Lean proof that decoding
an encoded value reproduces the original value.

Core WireFormats are intentionally simple. Complex layout-specific encodings
(columnar stripping, compact packing, mmap views) are library extensions that
must provide their own `roundTrip` proofs against this interface.
-/

import SilverSight.Semantics.Schema
import SilverSight.Semantics.Layout

namespace SilverSight.Semantics

/-- Certified wire format: encode, decode, and a proof that they round-trip.

    The `encode_size` field guarantees that every encoding consumes exactly
    `Schema.byteSize α` bytes, matching the schema contract. -/
structure WireFormat (α : Type) [Schema α] (layout : Layout) where
  encode      : α → ByteArray
  decode      : ByteArray → Option α
  encode_size : ∀ a, (encode a).size = byteSize α
  roundTrip   : ∀ a, decode (encode a) = some a

namespace WireFormat

/-- The trivial wire format for `Unit`: zero bytes round-trip. -/
def unitRowMajor : WireFormat Unit rowMajor where
  encode      := fun _ => ByteArray.empty
  decode      := fun _ => some ()
  encode_size := fun _ => rfl
  roundTrip   := fun _ => rfl

/-- Row-major wire format for `Bool`: one byte, 1 = true, 0 = false. -/
def boolRowMajor : WireFormat Bool rowMajor where
  encode := fun b => ByteArray.mk #[if b then (1 : UInt8) else (0 : UInt8)]
  decode := fun bs =>
    if h : bs.size = 1 then
      let idx : Fin bs.size := ⟨0, by rw [h]; decide⟩
      match bs.get idx with
      | 1 => some true
      | 0 => some false
      | _ => none
    else none
  encode_size := by
    intro _
    rfl
  roundTrip := by
    intro b
    cases b <;> simp [ByteArray.get, ByteArray.size]

/-- Row-major wire format for `UInt8`: one byte, identity. -/
def uint8RowMajor : WireFormat UInt8 rowMajor where
  encode := fun u => ByteArray.mk #[u]
  decode := fun bs =>
    if h : bs.size = 1 then
      let idx : Fin bs.size := ⟨0, by rw [h]; decide⟩
      some (bs.get idx)
    else
      none
  encode_size := by
    intro _
    rfl
  roundTrip := by
    intro u
    simp [ByteArray.get, ByteArray.size]

end WireFormat

end SilverSight.Semantics
