import tasks.add.Spec

/-!
# Task `add`: the statement as named properties (proved, not trusted)

`Spec.lean`'s `Statement` is one formula. This file gives each part of it a name, one definition
per thing a design must satisfy, and proves `statement_iff_properties`: the statement holds
exactly when, at every `N` in range, every property holds. The theorem is checked by Lean's
kernel, so the properties cover the whole statement and nothing else; this file adds nothing to
the trusted base. `properties.json` explains each property in plain words.
-/

namespace SvGolf.Tasks.Add.Properties

open SvGolf LeanModels.Sv

/-- The widths the statement covers: every `N` with `1 ≤ N < 2^31` (the values an `int` parameter
holds). -/
def ParamsInRange (N : Nat) : Prop :=
  1 ≤ N ∧ N < 2 ^ 31

/-- Exactly these ports, in this order, with these widths. -/
def Interface (N : Nat) (d : Design2) : Prop :=
  inputPorts d = [("a", N), ("b", N), ("cin", 1)] ∧ outputPorts d = [("s", N), ("cout", 1)]

/-- No process runs at a clock edge (no `always_ff`, no `always @(posedge …)`). -/
def Unclocked (d : Design2) : Prop :=
  ∀ p ∈ d.processes.toList, p.isEdgePhase = false

/-- No combinational loop: the design lowers to continuous assigns (`Design2.lowerComb`) that are
ranked (`Acyclic`): each reads only what lower-ranked ones write. -/
def LoopFree (d : Design2) : Prop :=
  ∃ d', d.lowerComb = some d' ∧ Acyclic d'

/-- Under every schedule and every stimulus, the run completes. -/
def Terminates (d : Design2) : Prop :=
  ∀ (σ : ScheduleOracle) (stim : List SvState), ∃ tr, Runs2 d σ stim tr

/-- In every completed run, every cycle whose stimulus drives `a`, `b`, `cin` with known values
ends with `s` and `cout` holding the low `N` bits and the carry of `a + b + cin`. -/
def ComputesSum (N : Nat) (d : Design2) : Prop :=
  d ⊨₂ spec2 fun stim tr =>
    ∀ (c : Nat) (inputs st : SvState), stim[c]? = some inputs → tr[c]? = some st →
      ∀ (a b : BitVec N) (cin : BitVec 1),
        HoldAll inputs [("a", N), ("b", N), ("cin", 1)] (a, b, cin, ()) →
        HoldAll st [("s", N), ("cout", 1)]
          (BitVec.ofNat N (a.toNat + b.toNat + cin.toNat),
           BitVec.ofNat 1 ((a.toNat + b.toNat + cin.toNat) / 2 ^ N), ())

/-- **The statement is exactly the properties.** -/
theorem statement_iff_properties (sem : Nat → Design2) :
    Statement sem ↔ ∀ N, ParamsInRange N →
      Interface N (sem N) ∧ Unclocked (sem N) ∧ LoopFree (sem N) ∧ Terminates (sem N) ∧ ComputesSum N (sem N) := by
  constructor
  · intro h N hN
    obtain ⟨hi, ⟨hu, hl, ht⟩, hc⟩ := h N hN
    refine ⟨hi, hu, hl, ht, ?_⟩
    intro σ stim tr hr c inputs st hs hst a b cin hv
    exact hc σ stim tr hr c inputs st hs hst (a, b, cin, ()) hv
  · intro h N hN
    obtain ⟨hi, hu, hl, ht, hc⟩ := h N hN
    refine ⟨hi, ⟨hu, hl, ht⟩, ?_⟩
    intro σ stim tr hr c inputs st hs hst v hv
    obtain ⟨a, b, cin, ⟨⟩⟩ := v
    exact hc σ stim tr hr c inputs st hs hst a b cin hv

end SvGolf.Tasks.Add.Properties