/-
SilverSight.Semantics.ProductSchema

Extends SilverSight.Semantics.Schema with instances for product types (α × β).
-/
import SilverSight.Semantics.Schema

namespace SilverSight.Semantics

-- ═══════════════════════════════════════════════════════════════════════════
-- §1  Product Schema instance
-- ═══════════════════════════════════════════════════════════════════════════

/-- Schema instance for fixed-size product types (α × β).
    byteSize is the sum of component sizes.
    wellFormed requires both components to be well-formed. -/
instance [Schema α] [Schema β] : Schema (α × β) where
  byteSize   := byteSize α + byteSize β
  wellFormed := fun (a, b) => wellFormed a && wellFormed b

@[simp] theorem prod_byteSize [Schema α] [Schema β] :
    byteSize (α × β) = byteSize α + byteSize β := rfl

theorem prod_wellFormed [Schema α] [Schema β] (a : α) (b : β) :
    wellFormed (a, b) = (wellFormed a && wellFormed b) := rfl

-- ═══════════════════════════════════════════════════════════════════════════
-- §2  Nested product schemas
-- ═══════════════════════════════════════════════════════════════════════════

@[simp] theorem prod3_byteSize [Schema α] [Schema β] [Schema γ] :
    byteSize ((α × β) × γ) = byteSize α + byteSize β + byteSize γ := by
  simp [prod_byteSize, Nat.add_assoc]

@[simp] theorem prod3_byteSize' [Schema α] [Schema β] [Schema γ] :
    byteSize (α × β × γ) = byteSize α + byteSize β + byteSize γ := by
  simp [prod_byteSize, Nat.add_assoc]

-- ═══════════════════════════════════════════════════════════════════════════
-- §3  #eval witnesses
-- ═══════════════════════════════════════════════════════════════════════════

#eval byteSize (UInt8 × UInt8)              -- expected: 2
#eval byteSize (UInt8 × Bool)               -- expected: 2
#eval byteSize (UInt32 × UInt32)            -- expected: 8
#eval byteSize (Q16_16 × Q16_16)           -- expected: 8
#eval byteSize (UInt8 × UInt32)             -- expected: 5
#eval byteSize ((UInt8 × UInt8) × UInt32)  -- expected: 6
#eval byteSize (UInt8 × UInt8 × UInt32)    -- expected: 6

end SilverSight.Semantics
