/-
SilverSight.Semantics.ProductWireFormat

Certified row-major wire formats for product types (α × β), using Core
WireFormat and ProductSchema.
-/
import SilverSight.Semantics.WireFormat
import SilverSight.ProductSchema

namespace SilverSight.Semantics

-- ═══════════════════════════════════════════════════════════════════════════
-- §1  Row-major wire format for (UInt8 × Bool)
-- ═══════════════════════════════════════════════════════════════════════════

def uint8BoolRowMajor : WireFormat (UInt8 × Bool) rowMajor where
  encode := fun (a, b) => ByteArray.mk #[a, if b then 1 else 0]
  decode := fun bs =>
    match bs.data.toList with
    | [a, b] => some (a, b != 0)
    | _ => none
  encode_size := by intro (a, b); rfl
  roundTrip := by
    intro (a, b)
    simp
    cases b <;> decide

#eval uint8BoolRowMajor.encode (42, true)
#eval uint8BoolRowMajor.decode (uint8BoolRowMajor.encode (42, true))

-- ═══════════════════════════════════════════════════════════════════════════
-- §2  Row-major wire format for (UInt8 × UInt8)
-- ═══════════════════════════════════════════════════════════════════════════

def uint8PairRowMajor : WireFormat (UInt8 × UInt8) rowMajor where
  encode := fun (a, b) => ByteArray.mk #[a, b]
  decode := fun bs =>
    match bs.data.toList with
    | [a, b] => some (a, b)
    | _ => none
  encode_size := by intro (a, b); rfl
  roundTrip := by
    intro (a, b)
    simp

#eval uint8PairRowMajor.encode (42, 7)
#eval uint8PairRowMajor.decode (uint8PairRowMajor.encode (42, 7))

-- ═══════════════════════════════════════════════════════════════════════════
-- §3  Row-major wire format for (Bool × Bool)
-- ═══════════════════════════════════════════════════════════════════════════

def boolPairRowMajor : WireFormat (Bool × Bool) rowMajor where
  encode := fun (a, b) => ByteArray.mk #[if a then 1 else 0, if b then 1 else 0]
  decode := fun bs =>
    match bs.data.toList with
    | [a, b] => some (a != 0, b != 0)
    | _ => none
  encode_size := by intro (a, b); rfl
  roundTrip := by
    intro (a, b)
    simp
    cases a <;> cases b <;> decide

#eval boolPairRowMajor.encode (true, false)
#eval boolPairRowMajor.decode (boolPairRowMajor.encode (true, false))

end SilverSight.Semantics
