/-
SilverSight.Semantics.LayoutBridge

A LayoutBridge converts between two wire formats of the same schema and
preserves meaning. The `correct` field is a Lean proof that converting the
encoding in layout L1 yields exactly the encoding in layout L2.

The Core only provides the bridge interface and identity bridges. Concrete
bridges (row-major ↔ columnar, compact expansion, mmap view wrapping) are
library extensions that must each supply a `correct` proof.
-/

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

namespace SilverSight.Semantics

/-- A certified conversion between two wire formats of the same schema. -/
structure LayoutBridge (α : Type) [Schema α] (L1 L2 : Layout) where
  wf1     : WireFormat α L1
  wf2     : WireFormat α L2
  convert : ByteArray → ByteArray
  correct : ∀ a, convert (wf1.encode a) = wf2.encode a

namespace LayoutBridge

/-- The identity bridge: encoding in L is already the encoding in L. -/
def identity {α : Type} {L : Layout} [Schema α] (wf : WireFormat α L) :
    LayoutBridge α L L where
  wf1     := wf
  wf2     := wf
  convert := id
  correct := by simp

/-- Identity bridge for `Bool` row-major. -/
def boolRowMajor : LayoutBridge Bool rowMajor rowMajor :=
  identity WireFormat.boolRowMajor

/-- Identity bridge for `UInt8` row-major. -/
def uint8RowMajor : LayoutBridge UInt8 rowMajor rowMajor :=
  identity WireFormat.uint8RowMajor

end LayoutBridge

end SilverSight.Semantics
