{-# OPTIONS --safe --cubical #-}

module Spartan6.Benchmarks.Counters where

open import Spartan6.Prelude

-- An executable, instrumentation-independent vocabulary for comparing work.
-- A readiness check is one scheduler attempt.  A handler execution includes
-- its decode path.  Dependency processing counts semantic net-dependency
-- occurrences.  Binding lookups count raw-ID comparisons performed by
-- Generic.lookupNet across handler, register-finalization, and top-output
-- resolution; validation's separate list searches are not included.  Node
-- construction excludes aliases.

record Counters : Type₀ where
  constructor counters
  field
    decodingCount             : ℕ
    readinessCheckCount       : ℕ
    handlerExecutionCount     : ℕ
    dependencyProcessingCount : ℕ
    bindingLookupCount        : ℕ
    nodeConstructionCount     : ℕ

open Counters public

zeroCounters : Counters
zeroCounters = counters      

infixl  _+ᶜ_

_+ᶜ_ : Counters -> Counters -> Counters
counters d₁ r₁ h₁ e₁ b₁ n₁ +ᶜ counters d₂ r₂ h₂ e₂ b₂ n₂ =
  counters
    (d₁ + d₂) (r₁ + r₂) (h₁ + h₂)
    (e₁ + e₂) (b₁ + b₂) (n₁ + n₂)

triangular : ℕ -> ℕ
triangular zero = zero
triangular (suc count) = suc count + triangular count

square : ℕ -> ℕ
square count = count · count

double : ℕ -> ℕ
double zero = zero
double (suc count) = suc (suc (double count))

eightfold : ℕ -> ℕ
eightfold zero = zero
eightfold (suc count) =  + eightfold count

reverseBindingLookups : ℕ -> ℕ
reverseBindingLookups zero = zero
reverseBindingLookups (suc count) =
  suc (triangular count) + reverseBindingLookups count

mixedBindingLookups : ℕ -> ℕ
mixedBindingLookups zero = zero
mixedBindingLookups (suc count) =
  ( · count + ) + mixedBindingLookups count

orderedChainCounters : ℕ -> Counters
orderedChainCounters count =
  counters count count count count (suc count) count

-- The retained first-buildable scheduler replays every blocked suffix head.
-- A reverse chain therefore performs 1 + ... + n complete attempts.
reverseChainCounters : ℕ -> Counters
reverseChainCounters count =
  counters
    (triangular count)
    (triangular count)
    (triangular count)
    count
    (suc (reverseBindingLookups count))
    count

-- Every fan-out consumer is ready, but each previous output binding precedes
-- the common input in the current list environment.
fanOutCounters : ℕ -> Counters
fanOutCounters count =
  counters count count count count
    (triangular count + triangular count) count

-- In source order, earlier outputs and earlier input bindings together make
-- the independent lookup total n squared.
independentCounters : ℕ -> Counters
independentCounters count =
  counters count count count count
    (square count + triangular count) count

-- Each OBUFDS occurrence produces an alias and one inversion node.  Two new
-- bindings per prior occurrence yield the first n odd lookup costs.
multiOutputCounters : ℕ -> Counters
multiOutputCounters count =
  counters count count count count
    (square count + triangular (double count)) count

predecessors : ℕ -> ℕ
predecessors zero = zero
predecessors (suc count) = count

-- Constants do not consult bindings.  Every CARRY4 after the first resolves
-- one preceding CO bit, and every occurrence constructs eight checked nodes.
carry4ChainCounters : ℕ -> Counters
carry4ChainCounters count =
  counters count count count (predecessors count)
    (triangular (eightfold count) + predecessors count)
    (eightfold count)

-- Each mixed-register lane has one decoded register and one decoded LUT.
-- Scheduling executes only the LUT; its Q dependency, the register's D
-- dependency, and the shared clock dependency remain separately counted.
mixedRegisterCounters : ℕ -> Counters
mixedRegisterCounters count =
  counters
    (doubleCount count)
    count
    count
    (tripleCount count)
    (mixedBindingLookups count)
    (tripleCount count)
  where
  doubleCount : ℕ -> ℕ
  doubleCount zero = zero
  doubleCount (suc remaining) = suc (suc (doubleCount remaining))

  tripleCount : ℕ -> ℕ
  tripleCount zero = zero
  tripleCount (suc remaining) =
    suc (suc (suc (tripleCount remaining)))

ordered-four-cost :
  orderedChainCounters  ≡ counters      
ordered-four-cost = refl

reverse-four-cost :
  reverseChainCounters  ≡ counters      
reverse-four-cost = refl

fan-out-four-cost :
  fanOutCounters  ≡ counters      
fan-out-four-cost = refl

independent-four-cost :
  independentCounters  ≡ counters      
independent-four-cost = refl

multi-output-three-cost :
  multiOutputCounters  ≡ counters      
multi-output-three-cost = refl

carry4-three-cost :
  carry4ChainCounters  ≡ counters      
carry4-three-cost = refl

mixed-register-three-cost :
  mixedRegisterCounters  ≡ counters      
mixed-register-three-cost = refl