import SilverSight.Receipt

namespace SilverSight

open Semantics.FixedPoint
open Semantics.FixedPoint.Q16_16

-- ═══════════════════════════════════════════════════════════════════════════
-- §1  Receipt composition (bind)
-- ═══════════════════════════════════════════════════════════════════════════

/-- Compose two receipts into a single receipt.
    The resulting receipt:
    - has gateType = .compose
    - has cost = left.cost + right.cost (additive)
    - has invariant = left.invariant ++ " ∧ " ++ right.invariant (conjunction)
    - has timestamp = max(left.timestamp, right.timestamp) (latest)
    - is well-formed iff both inputs are well-formed

    This is the fundamental composition primitive for the SilverSight receipt ledger. -/
def bindReceipt (left right : Receipt) : Receipt :=
  { gateType   := .compose
    cost       := add left.cost right.cost
    invariant  := left.invariant ++ " ∧ " ++ right.invariant
    timestamp  := max left.timestamp right.timestamp
    wellFormed := left.wellFormed && right.wellFormed }

-- ═══════════════════════════════════════════════════════════════════════════
-- §2  Well-formedness preservation
-- ═══════════════════════════════════════════════════════════════════════════

/-- bind preserves well-formedness: if both inputs are well-formed,
    the result is well-formed. -/
theorem bind_preservesWellFormed (left right : Receipt)
    (hl : left.wellFormed = true) (hr : right.wellFormed = true) :
    (bindReceipt left right).wellFormed = true := by
  simp [bindReceipt, hl, hr]

/-- bind preserves well-formedness (forward direction): if the result
    is well-formed, both inputs must be well-formed. -/
theorem bind_wellFormed_implies_inputs (left right : Receipt)
    (h : (bindReceipt left right).wellFormed = true) :
    left.wellFormed = true ∧ right.wellFormed = true := by
  simp only [bindReceipt] at h
  exact Bool.and_eq_true_iff.mp h

-- ═══════════════════════════════════════════════════════════════════════════
-- §3  Cost properties
-- ═══════════════════════════════════════════════════════════════════════════

/-- bind cost is the sum of the component costs. -/
theorem bind_cost_additive (left right : Receipt) :
    (bindReceipt left right).cost = add left.cost right.cost := by
  rfl

-- ═══════════════════════════════════════════════════════════════════════════
-- §4  Timestamp properties
-- ═══════════════════════════════════════════════════════════════════════════

/-- bind timestamp is the maximum of the component timestamps. -/
theorem bind_timestamp_max (left right : Receipt) :
    (bindReceipt left right).timestamp = max left.timestamp right.timestamp := by
  rfl

/-- bind timestamp is commutative. -/
theorem bind_timestamp_comm (left right : Receipt) :
    (bindReceipt left right).timestamp = (bindReceipt right left).timestamp := by
  simp [bindReceipt, Nat.max_comm]

-- ═══════════════════════════════════════════════════════════════════════════
-- §5  Associativity (well-formedness only)
-- ═══════════════════════════════════════════════════════════════════════════

/-- bind is associative on well-formedness. -/
theorem bind_wellFormed_assoc (a b c : Receipt) :
    (bindReceipt (bindReceipt a b) c).wellFormed =
    (bindReceipt a (bindReceipt b c)).wellFormed := by
  simp [bindReceipt, Bool.and_assoc]

-- ═══════════════════════════════════════════════════════════════════════════
-- §6  Invariant properties
-- ═══════════════════════════════════════════════════════════════════════════

/-- bind invariant is the conjunction of the component invariants. -/
theorem bind_invariant_conjunction (left right : Receipt) :
    (bindReceipt left right).invariant = left.invariant ++ " ∧ " ++ right.invariant := by
  rfl

-- ═══════════════════════════════════════════════════════════════════════════
-- §7  Gate type properties
-- ═══════════════════════════════════════════════════════════════════════════

/-- bind always produces a compose gate. -/
theorem bind_gateType (left right : Receipt) :
    (bindReceipt left right).gateType = .compose := by
  rfl

-- ═══════════════════════════════════════════════════════════════════════════
-- §8  #eval witnesses
-- ═══════════════════════════════════════════════════════════════════════════

def r1 := mkReceipt .encode (Q16_16.ofInt 50) "schema:UInt8" 1
def r2 := mkReceipt .decode (Q16_16.ofInt 30) "schema:Bool" 2
def r3 := mkReceipt .validate (Q16_16.ofInt 20) "wellformed" 3

#eval (bindReceipt r1 r2).gateType    -- expected: GateType.compose
#eval (bindReceipt r1 r2).wellFormed  -- expected: true
#eval (bindReceipt r1 r2).invariant   -- expected: "schema:UInt8 ∧ schema:Bool"
#eval (bindReceipt r1 r2).timestamp   -- expected: 2
#eval (bindReceipt (bindReceipt r1 r2) r3).invariant  -- expected: "schema:UInt8 ∧ schema:Bool ∧ wellformed"
#eval (bindReceipt r1 r2).cost        -- expected: 5242880 (Q16_16 of 80)
#eval (bindReceipt r1 r2).wellFormed  -- expected: true

end SilverSight