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

module Spartan6.Validation.CycleSoundness where

open import Spartan6.Prelude

import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Raw as Validation

open import Cubical.Data.Nat using (_≡ᵇ_)
open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty

private
  variable
    ℓ : Level

infix  _∈_

data _∈_ {A : Type ℓ} (item : A) : List A → Type ℓ where
  here  : ∀ {items} → item ∈ (item ∷ᴸ items)
  there : ∀ {other items} → item ∈ items → item ∈ (other ∷ᴸ items)

or-true-sound : ∀ {left right}
  → left or right ≡ true
  → (left ≡ true) ⊎ (right ≡ true)
or-true-sound {false} {false} result =
  Empty.rec (false≢true result)
or-true-sound {false} {true} result = inr refl
or-true-sound {true} {false} result = inl refl
or-true-sound {true} {true} result = inl refl

or-true-left : ∀ {left right}
  → left ≡ true
  → left or right ≡ true
or-true-left {left} {right} result =
  cong (λ value → value or right) result

or-true-right : ∀ {left right}
  → right ≡ true
  → left or right ≡ true
or-true-right {false} result = result
or-true-right {true} result = refl

nat-equality-reflexive : ∀ number → (number ≡ᵇ number) ≡ true
nat-equality-reflexive zero = refl
nat-equality-reflexive (suc number) = nat-equality-reflexive number

nat-equality-sound : ∀ {left right}
  → (left ≡ᵇ right) ≡ true
  → left ≡ right
nat-equality-sound {zero} {zero} result = refl
nat-equality-sound {zero} {suc right} result =
  Empty.rec (false≢true result)
nat-equality-sound {suc left} {zero} result =
  Empty.rec (false≢true result)
nat-equality-sound {suc left} {suc right} result =
  cong suc (nat-equality-sound result)

nat-equality-complete : ∀ {left right}
  → left ≡ right
  → (left ≡ᵇ right) ≡ true
nat-equality-complete {left} equality =
  subst (λ right → (left ≡ᵇ right) ≡ true)
        equality
        (nat-equality-reflexive left)

-- A propositional edge witness records an actual entry in the dependency
-- list.  Endpoint paths account for the Boolean source comparison performed
-- by targetsFrom.

data DependencyEdge
  (source target : Raw.NetId)
  : List Validation.Dependency → Type₀ where
  edgeHere : ∀ {edge edges}
    → source ≡ Validation.Dependency.dependencySource edge
    → target ≡ Validation.Dependency.dependencyTarget edge
    → DependencyEdge source target (edge ∷ᴸ edges)
  edgeThere : ∀ {edge edges}
    → DependencyEdge source target edges
    → DependencyEdge source target (edge ∷ᴸ edges)

targetsFrom-sound : ∀ {source target edges}
  → target ∈ Validation.targetsFrom source edges
  → DependencyEdge source target edges
targetsFrom-sound {edges = []ᴸ} ()
targetsFrom-sound
  {source} {target} {edge ∷ᴸ edges} membership
  with source ≡ᵇ Validation.Dependency.dependencySource edge UsingEq
... | false , comparison =
  edgeThere
    (targetsFrom-sound
      (subst
        (λ equal-source →
          target ∈
            (if equal-source
             then Validation.Dependency.dependencyTarget edge
                  ∷ᴸ Validation.targetsFrom source edges
             else Validation.targetsFrom source edges))
        comparison
        membership))
... | true , comparison
  with subst
    (λ equal-source →
      target ∈
        (if equal-source
         then Validation.Dependency.dependencyTarget edge
              ∷ᴸ Validation.targetsFrom source edges
         else Validation.targetsFrom source edges))
    comparison
    membership
...   | here = edgeHere (nat-equality-sound comparison) refl
...   | there rest = edgeThere (targetsFrom-sound rest)

targetsFrom-complete : ∀ {source target edges}
  → DependencyEdge source target edges
  → target ∈ Validation.targetsFrom source edges
targetsFrom-complete {edges = []ᴸ} ()
targetsFrom-complete
  {source} {target} {edge ∷ᴸ edges}
  (edgeHere source-path target-path) =
    subst
      (λ equal-source →
        target ∈
          (if equal-source
           then Validation.Dependency.dependencyTarget edge
                ∷ᴸ Validation.targetsFrom source edges
           else Validation.targetsFrom source edges))
      (sym (nat-equality-complete source-path))
      (subst
        (λ candidate →
          candidate
          ∈ (Validation.Dependency.dependencyTarget edge
             ∷ᴸ Validation.targetsFrom source edges))
        (sym target-path)
        here)
targetsFrom-complete
  {source} {target} {edge ∷ᴸ edges}
  (edgeThere rest)
  with source ≡ᵇ Validation.Dependency.dependencySource edge
... | false = targetsFrom-complete rest
... | true = there (targetsFrom-complete rest)

-- ReachableWithin is the graph-theoretic meaning of the detector's fuel.
-- It contains only endpoint equality and actual dependency edges.

data ReachableWithin
  (edges : List Validation.Dependency)
  (target : Raw.NetId)
  : ℕ → Raw.NetId → Type₀ where
  atTarget : ∀ {fuel current}
    → current ≡ target
    → ReachableWithin edges target fuel current
  followEdge : ∀ {fuel current next}
    → DependencyEdge current next edges
    → ReachableWithin edges target fuel next
    → ReachableWithin edges target (suc fuel) current

mutual
  reachable-sound : ∀ {fuel target current edges}
    → Validation.reachable fuel target current edges ≡ true
    → ReachableWithin edges target fuel current
  reachable-sound {fuel = zero} result =
    atTarget (nat-equality-sound result)
  reachable-sound {fuel = suc fuel} result
    with or-true-sound result
  ... | inl current-is-target =
    atTarget (nat-equality-sound current-is-target)
  ... | inr explored with explore-sound explored
  ...   | next , membership , path =
    followEdge (targetsFrom-sound membership) path

  explore-sound : ∀ {fuel target nexts edges}
    → Validation.explore fuel target nexts edges ≡ true
    → Σ Raw.NetId λ next
      → (next ∈ nexts) × ReachableWithin edges target fuel next
  explore-sound {nexts = []ᴸ} result =
    Empty.rec (false≢true result)
  explore-sound {nexts = next ∷ᴸ nexts} result
    with or-true-sound result
  ... | inl found = next , here , reachable-sound found
  ... | inr found-later with explore-sound found-later
  ...   | later-next , membership , path =
    later-next , there membership , path

mutual
  reachable-complete : ∀ {fuel target current edges}
    → ReachableWithin edges target fuel current
    → Validation.reachable fuel target current edges ≡ true
  reachable-complete {fuel = zero} (atTarget equality) =
    nat-equality-complete equality
  reachable-complete {fuel = suc fuel} (atTarget equality) =
    or-true-left (nat-equality-complete equality)
  reachable-complete {fuel = suc fuel} (followEdge edge path) =
    or-true-right
      (explore-complete (targetsFrom-complete edge) path)

  explore-complete : ∀ {fuel target next nexts edges}
    → next ∈ nexts
    → ReachableWithin edges target fuel next
    → Validation.explore fuel target nexts edges ≡ true
  explore-complete here path =
    or-true-left (reachable-complete path)
  explore-complete (there membership) path =
    or-true-right (explore-complete membership path)

CycleWithin : ℕ
            → List Validation.Dependency
            → List Validation.Dependency
            → Type₀
CycleWithin fuel all-edges candidate-edges =
  Σ Validation.Dependency λ edge
    → (edge ∈ candidate-edges)
    × ReachableWithin
        all-edges
        (Validation.Dependency.dependencySource edge)
        fuel
        (Validation.Dependency.dependencyTarget edge)

someDependencyCycles-sound : ∀ {fuel all-edges candidate-edges}
  → Validation.someDependencyCycles fuel all-edges candidate-edges ≡ true
  → CycleWithin fuel all-edges candidate-edges
someDependencyCycles-sound {candidate-edges = []ᴸ} result =
  Empty.rec (false≢true result)
someDependencyCycles-sound
  {fuel} {all-edges} {edge ∷ᴸ edges} result
  with or-true-sound result
... | inl return-path =
  edge , here , reachable-sound return-path
... | inr later-cycle with someDependencyCycles-sound later-cycle
...   | found-edge , membership , return-path =
  found-edge , there membership , return-path

someDependencyCycles-complete : ∀ {fuel all-edges candidate-edges}
  → CycleWithin fuel all-edges candidate-edges
  → Validation.someDependencyCycles fuel all-edges candidate-edges ≡ true
someDependencyCycles-complete {candidate-edges = []ᴸ}
  (edge , () , return-path)
someDependencyCycles-complete {candidate-edges = edge ∷ᴸ edges}
  (.edge , here , return-path) =
    or-true-left (reachable-complete return-path)
someDependencyCycles-complete {candidate-edges = edge ∷ᴸ edges}
  (found-edge , there membership , return-path) =
    or-true-right
      (someDependencyCycles-complete
        (found-edge , membership , return-path))

CombinationalCycle : Raw.RawDesign → Type₀
CombinationalCycle design =
  CycleWithin
    (suc (lengthList (Validation.designDependencies design)))
    (Validation.designDependencies design)
    (Validation.designDependencies design)

combinationalCycle?-sound : ∀ design
  → Validation.combinationalCycle? design ≡ true
  → CombinationalCycle design
combinationalCycle?-sound design result =
  someDependencyCycles-sound result

combinationalCycle?-complete : ∀ design
  → CombinationalCycle design
  → Validation.combinationalCycle? design ≡ true
combinationalCycle?-complete design cycle =
  someDependencyCycles-complete cycle

-- Completeness above is exact for the fuel chosen by combinationalCycle?.
-- Turning it into an unbounded finite-graph theorem would additionally require
-- a normalization result that removes repeated vertices or edges from walks;
-- Validation.Raw currently defines neither such walks nor a finite vertex set.