/-
SilverSight.Semantics.Schema

A Schema is the logical shape of a type. It is the source of truth;
layouts and wire formats are derived from it.

Core schemas are fixed-size. Variable-length containers (lists, maps,
streams) are represented by pointing to a separately-scoped buffer and
are a library extension, not part of the invariant core.
-/

import SilverSight.FixedPoint

namespace SilverSight.Semantics

open SilverSight.FixedPoint

/-- Core schema: fixed byte size on the wire plus a well-formedness check.

    `byteSize` is the canonical encoded length. `wellFormed` is the
    minimal structural predicate the decoder may assume/verify. It is
    a `Bool`, not a `Prop`, so that decoders can use it directly at
    runtime without requiring a `Decidable` instance. -/
class Schema (α : Type) where
  byteSize   : Nat
  wellFormed : α → Bool

export Schema (byteSize wellFormed)

/-- Shorthand for the canonical encoded size of a type. -/
def encodedSize (α : Type) [Schema α] : Nat := byteSize α

/-- A value is schema-admissible if it is well-formed. -/
def SchemaAdmissible {α : Type} [Schema α] (a : α) : Prop := wellFormed a = true

/-- The empty schema is admissible for unit-like values. -/
instance : Schema Unit where
  byteSize   := 0
  wellFormed := fun _ => true

/-- Booleans occupy one byte on the wire. -/
instance : Schema Bool where
  byteSize   := 1
  wellFormed := fun _ => true

@[simp] theorem bool_byteSize : byteSize Bool = 1 := rfl

/-- 8-bit unsigned integers occupy one byte. -/
instance : Schema UInt8 where
  byteSize   := 1
  wellFormed := fun _ => true

@[simp] theorem uint8_byteSize : byteSize UInt8 = 1 := rfl

/-- 32-bit unsigned integers occupy four bytes in row-major layout. -/
instance : Schema UInt32 where
  byteSize   := 4
  wellFormed := fun _ => true

@[simp] theorem uint32_byteSize : byteSize UInt32 = 4 := rfl

/-- 64-bit unsigned integers occupy eight bytes. -/
instance : Schema UInt64 where
  byteSize   := 8
  wellFormed := fun _ => true

@[simp] theorem uint64_byteSize : byteSize UInt64 = 8 := rfl

/-- Q16_16 fixed-point (32-bit signed scaled by 2^16) occupies four bytes.
    Q16_16 is used where values may exceed [-1,1] or require hardware-register
    width; Q0_16 is the default for dimensionless scalars. -/
instance : Schema Q16_16 where
  byteSize   := 4
  wellFormed := fun _ => true

@[simp] theorem q16_16_byteSize : byteSize Q16_16 = 4 := rfl

/-- Q0_16 fixed-point (16-bit signed fraction in [-1,1]) occupies two bytes.
    Default scalar type for dimensionless quantities. -/
instance : Schema Q0_16 where
  byteSize   := 2
  wellFormed := fun _ => true

@[simp] theorem q0_16_byteSize : byteSize Q0_16 = 2 := rfl

end SilverSight.Semantics
