Properties.lean

import tasks.mul.Spec

/-!
# Task `mul`: 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.Mul.Properties

open SvGolf LeanModels.Sv

/-- The widths the statement covers: every `N` with `1 ≤ N < 2^30` (so that the output width `2N`,
an `int` expression of the module, stays below `2^31`, the values an `int` holds). -/
def ParamsInRange (N : Nat) : Prop :=
  1 ≤ N ∧ N < 2 ^ 30

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

/-- 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` and `b` with known values ends
with `p` holding their full product, on `2N` bits. -/
def ComputesProduct (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),
        HoldAll inputs [("a", N), ("b", N)] (a, b, ()) →
        HoldAll st [("p", 2 * N)] (BitVec.ofNat (2 * N) (a.toNat * b.toNat), ())

/-- **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) ∧
        ComputesProduct 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 hv
    exact hc σ stim tr hr c inputs st hs hst (a, b, ()) 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, ⟨⟩⟩ := v
    exact hc σ stim tr hr c inputs st hs hst a b hv

end SvGolf.Tasks.Mul.Properties