Spartan6.Netlist.Carry4BuilderSoundness

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

module Spartan6.Netlist.Carry4BuilderSoundness where

open import Spartan6.Prelude

import Spartan6.Netlist.Carry4Builder as Builder
import Spartan6.Netlist.BuilderCore as Generic
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Expression as Expression
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.Carry4 as Carry

-- Evaluate a checked wire against the locals already compiled by a node
-- spine.  This covers external inputs, stored state, earlier local nodes, and
-- literals uniformly.

evaluateWire : ∀ {inputCount registerCount localCount}
  → Checked.Nodes inputCount registerCount localCount
  → Vec Bit inputCount
  → Vec Bit registerCount
  → Checked.Wire inputCount registerCount localCount
  → Bit
evaluateWire nodes external state wire =
  Expression.eval external state
    (Checked.compileWire (Checked.compileNodes nodes) wire)

evaluateWires : ∀ {inputCount registerCount localCount count}
  → Checked.Nodes inputCount registerCount localCount
  → Vec Bit inputCount
  → Vec Bit registerCount
  → Vec (Checked.Wire inputCount registerCount localCount) count
  → Vec Bit count
evaluateWires nodes external state [] = []
evaluateWires nodes external state (wire ∷ wires) =
  evaluateWire nodes external state wire
  ∷ evaluateWires nodes external state wires

evaluateBuilderWire : ∀ {inputCount registerCount}
  → (current : Generic.Builder inputCount registerCount)
  → Vec Bit inputCount
  → Vec Bit registerCount
  → Checked.Wire
      inputCount registerCount (Generic.builderLocalCount current)
  → Bit
evaluateBuilderWire current = evaluateWire (Generic.builderNodes current)

evaluateBuilderWires : ∀ {inputCount registerCount count}
  → (current : Generic.Builder inputCount registerCount)
  → Vec Bit inputCount
  → Vec Bit registerCount
  → Vec
      (Checked.Wire
        inputCount registerCount (Generic.builderLocalCount current))
      count
  → Vec Bit count
evaluateBuilderWires current = evaluateWires (Generic.builderNodes current)

compile-liftLocalWire :
  ∀ {inputCount registerCount localCount}
    (nodes : Checked.Nodes inputCount registerCount localCount)
    (node : Checked.Node inputCount registerCount localCount)
    (wire : Checked.Wire inputCount registerCount localCount)
  → Checked.compileWire
      (Checked.compileNodes (nodes Checked.▻ node))
      (Generic.liftLocalWire wire)
    ≡ Checked.compileWire (Checked.compileNodes nodes) wire
compile-liftLocalWire nodes node (Checked.externalWire index) = refl
compile-liftLocalWire nodes node (Checked.storedWire index) = refl
compile-liftLocalWire nodes node (Checked.localWire index) = refl
compile-liftLocalWire nodes node (Checked.literalWire bit) = refl

addCarryStage-preserves-wire :
  ∀ {inputCount registerCount}
    (current : Generic.Builder inputCount registerCount)
    incoming di select o-net co-net external state
    (wire :
      Checked.Wire inputCount registerCount
        (Generic.builderLocalCount current))
  → evaluateBuilderWire
      (Builder.addCarryStage
        current incoming di select o-net co-net)
      external state
      (Builder.liftLocalTwice wire)
    ≡ evaluateBuilderWire current external state wire
addCarryStage-preserves-wire
  (Generic.builder local-count nodes bindings)
  incoming di select o-net co-net external state wire =
  cong (Expression.eval external state)
    (compile-liftLocalWire
      (nodes Checked.▻ Checked.xorNode select incoming)
      (Checked.muxNode
        (Generic.liftLocalWire select)
        (Generic.liftLocalWire di)
        (Generic.liftLocalWire incoming))
      (Generic.liftLocalWire wire)
    ∙ compile-liftLocalWire
        nodes (Checked.xorNode select incoming) wire)

addCarryStage-o-value :
  ∀ {inputCount registerCount}
    (current : Generic.Builder inputCount registerCount)
    incoming di select o-net co-net external state
  → evaluateBuilderWire
      (Builder.addCarryStage
        current incoming di select o-net co-net)
      external state
      (Checked.localWire (fsuc fzero))
    ≡ Carry.xorCY
        (evaluateBuilderWire current external state select)
        (evaluateBuilderWire current external state incoming)
addCarryStage-o-value
  (Generic.builder local-count nodes bindings)
  incoming di select o-net co-net external state = refl

addCarryStage-co-value :
  ∀ {inputCount registerCount}
    (current : Generic.Builder inputCount registerCount)
    incoming di select o-net co-net external state
  → evaluateBuilderWire
      (Builder.addCarryStage
        current incoming di select o-net co-net)
      external state
      (Checked.localWire fzero)
    ≡ Carry.muxCY
        (evaluateBuilderWire current external state select)
        (evaluateBuilderWire current external state di)
        (evaluateBuilderWire current external state incoming)
addCarryStage-co-value
  (Generic.builder local-count nodes bindings)
  incoming di select o-net co-net external state =
  cong (Expression.eval external state)
    (cong₃ Expression.select
      (compile-liftLocalWire
        nodes (Checked.xorNode select incoming) select)
      (compile-liftLocalWire
        nodes (Checked.xorNode select incoming) di)
      (compile-liftLocalWire
        nodes (Checked.xorNode select incoming) incoming))

-- buildCarry4 appends XOR then MUX for bits 0,1,2,3.  Because local index zero
-- denotes the newest node, the final O wires occupy 7,5,3,1 and CO occupies
-- 6,4,2,0.  The dependent result below records those exact wires at the
-- builder's computed final local bound.

builtOutputWires :
  ∀ {inputCount registerCount}
  → (current : Generic.Builder inputCount registerCount)
  → (entry :
      Checked.Wire
        inputCount registerCount (Generic.builderLocalCount current))
  → (di select :
      Vec
        (Checked.Wire
          inputCount registerCount (Generic.builderLocalCount current))
        4)
  → (o-nets co-nets : Vec Raw.NetId 4)
  → Vec
      (Checked.Wire inputCount registerCount
        (Generic.builderLocalCount
          (Builder.buildCarry4
            current entry di select o-nets co-nets)))
      8
builtOutputWires
  (Generic.builder local-count nodes bindings)
  entry
  (di0 ∷ di1 ∷ di2 ∷ di3 ∷ [])
  (s0 ∷ s1 ∷ s2 ∷ s3 ∷ [])
  (o0 ∷ o1 ∷ o2 ∷ o3 ∷ [])
  (co0 ∷ co1 ∷ co2 ∷ co3 ∷ []) =
  Checked.localWire
    (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))))
  ∷ Checked.localWire
      (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))
  ∷ Checked.localWire (fsuc (fsuc (fsuc fzero)))
  ∷ Checked.localWire (fsuc fzero)
  ∷ Checked.localWire
      (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero))))))
  ∷ Checked.localWire (fsuc (fsuc (fsuc (fsuc fzero))))
  ∷ Checked.localWire (fsuc (fsuc fzero))
  ∷ Checked.localWire fzero
  ∷ []

flattenCarryOutput : Carry.Carry4Output → Vec Bit 8
flattenCarryOutput
  (Carry.carry4Output
    (o0 ∷ o1 ∷ o2 ∷ o3 ∷ [])
    (co0 ∷ co1 ∷ co2 ∷ co3 ∷ [])) =
  o0 ∷ o1 ∷ o2 ∷ o3
  ∷ co0 ∷ co1 ∷ co2 ∷ co3 ∷ []

vec8-cong : ∀ {A : Type₀}
  {a0 a1 a2 a3 a4 a5 a6 a7 b0 b1 b2 b3 b4 b5 b6 b7 : A}
  → a0 ≡ b0 → a1 ≡ b1 → a2 ≡ b2 → a3 ≡ b3
  → a4 ≡ b4 → a5 ≡ b5 → a6 ≡ b6 → a7 ≡ b7
  → (a0 ∷ a1 ∷ a2 ∷ a3 ∷ a4 ∷ a5 ∷ a6 ∷ a7 ∷ [])
    ≡ (b0 ∷ b1 ∷ b2 ∷ b3 ∷ b4 ∷ b5 ∷ b6 ∷ b7 ∷ [])
vec8-cong p0 p1 p2 p3 p4 p5 p6 p7 =
  cong₂ _∷_ p0
    (cong₂ _∷_ p1
      (cong₂ _∷_ p2
        (cong₂ _∷_ p3
          (cong₂ _∷_ p4
            (cong₂ _∷_ p5
              (cong₂ _∷_ p6
                (cong₂ _∷_ p7 refl)))))))

-- Fully general checked-node correspondence.  Existing local expressions are
-- evaluated once at the incoming builder boundary; the four generated stages
-- then agree definitionally with UG615 muxCY/xorCY in Primitive.Carry4.

buildCarry4-evaluation :
  ∀ {inputCount registerCount}
    (current : Generic.Builder inputCount registerCount)
    (entry :
      Checked.Wire
        inputCount registerCount (Generic.builderLocalCount current))
    (di select :
      Vec
        (Checked.Wire
          inputCount registerCount (Generic.builderLocalCount current))
        4)
    (o-nets co-nets : Vec Raw.NetId 4)
    (external : Vec Bit inputCount)
    (state : Vec Bit registerCount)
  → evaluateBuilderWires
      (Builder.buildCarry4 current entry di select o-nets co-nets)
      external state
      (builtOutputWires current entry di select o-nets co-nets)
    ≡ flattenCarryOutput
        (Carry.evalCarry4
          (Carry.fromCI
            (evaluateBuilderWire current external state entry))
          (evaluateBuilderWires current external state di)
          (evaluateBuilderWires current external state select))
buildCarry4-evaluation
  (Generic.builder local-count nodes bindings)
  entry
  (di0 ∷ di1 ∷ di2 ∷ di3 ∷ [])
  (s0 ∷ s1 ∷ s2 ∷ s3 ∷ [])
  (o0 ∷ o1 ∷ o2 ∷ o3 ∷ [])
  (co0 ∷ co1 ∷ co2 ∷ co3 ∷ [])
  external state =
  vec8-cong
    o0-final o1-final o2-final o3-final
    co0-final co1-final co2-final co3-final
  where
  current : Generic.Builder _ _
  current = Generic.builder local-count nodes bindings

  value : Checked.Wire _ _ local-count → Bit
  value = evaluateBuilderWire current external state

  c0 d0 d1 d2 d3 s₀ s₁ s₂ s₃ : Bit
  c0 = value entry
  d0 = value di0
  d1 = value di1
  d2 = value di2
  d3 = value di3
  s₀ = value s0
  s₁ = value s1
  s₂ = value s2
  s₃ = value s3

  c1 c2 c3 c4 x0 x1 x2 x3 : Bit
  c1 = Carry.muxCY s₀ d0 c0
  c2 = Carry.muxCY s₁ d1 c1
  c3 = Carry.muxCY s₂ d2 c2
  c4 = Carry.muxCY s₃ d3 c3
  x0 = Carry.xorCY s₀ c0
  x1 = Carry.xorCY s₁ c1
  x2 = Carry.xorCY s₂ c2
  x3 = Carry.xorCY s₃ c3

  b0 b1 b2 b3 : Generic.Builder _ _
  b0 = Builder.addCarryStage current entry di0 s0 o0 co0
  b1 =
    Builder.addCarryStage b0
      (Checked.localWire fzero)
      (Builder.liftLocalTwice di1)
      (Builder.liftLocalTwice s1)
      o1 co1
  b2 =
    Builder.addCarryStage b1
      (Checked.localWire fzero)
      (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
      (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
      o2 co2
  b3 =
    Builder.addCarryStage b2
      (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3

  s1-at-b0 :
    evaluateBuilderWire b0 external state
      (Builder.liftLocalTwice s1)
    ≡ s₁
  s1-at-b0 =
    addCarryStage-preserves-wire
      current entry di0 s0 o0 co0 external state s1

  d1-at-b0 :
    evaluateBuilderWire b0 external state
      (Builder.liftLocalTwice di1)
    ≡ d1
  d1-at-b0 =
    addCarryStage-preserves-wire
      current entry di0 s0 o0 co0 external state di1

  s2-at-b1 :
    evaluateBuilderWire b1 external state
      (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
    ≡ s₂
  s2-at-b1 =
    addCarryStage-preserves-wire
      b0 (Checked.localWire fzero)
      (Builder.liftLocalTwice di1)
      (Builder.liftLocalTwice s1)
      o1 co1 external state (Builder.liftLocalTwice s2)
    ∙ addCarryStage-preserves-wire
        current entry di0 s0 o0 co0 external state s2

  d2-at-b1 :
    evaluateBuilderWire b1 external state
      (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
    ≡ d2
  d2-at-b1 =
    addCarryStage-preserves-wire
      b0 (Checked.localWire fzero)
      (Builder.liftLocalTwice di1)
      (Builder.liftLocalTwice s1)
      o1 co1 external state (Builder.liftLocalTwice di2)
    ∙ addCarryStage-preserves-wire
        current entry di0 s0 o0 co0 external state di2

  s3-at-b2 :
    evaluateBuilderWire b2 external state
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
    ≡ s₃
  s3-at-b2 =
    addCarryStage-preserves-wire
      b1 (Checked.localWire fzero)
      (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
      (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
      o2 co2 external state
      (Builder.liftLocalTwice (Builder.liftLocalTwice s3))
    ∙ addCarryStage-preserves-wire
        b0 (Checked.localWire fzero)
        (Builder.liftLocalTwice di1)
        (Builder.liftLocalTwice s1)
        o1 co1 external state (Builder.liftLocalTwice s3)
    ∙ addCarryStage-preserves-wire
        current entry di0 s0 o0 co0 external state s3

  d3-at-b2 :
    evaluateBuilderWire b2 external state
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
    ≡ d3
  d3-at-b2 =
    addCarryStage-preserves-wire
      b1 (Checked.localWire fzero)
      (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
      (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
      o2 co2 external state
      (Builder.liftLocalTwice (Builder.liftLocalTwice di3))
    ∙ addCarryStage-preserves-wire
        b0 (Checked.localWire fzero)
        (Builder.liftLocalTwice di1)
        (Builder.liftLocalTwice s1)
        o1 co1 external state (Builder.liftLocalTwice di3)
    ∙ addCarryStage-preserves-wire
        current entry di0 s0 o0 co0 external state di3

  co0-at-b0 :
    evaluateBuilderWire b0 external state
      (Checked.localWire fzero)
    ≡ c1
  co0-at-b0 =
    addCarryStage-co-value
      current entry di0 s0 o0 co0 external state

  o0-at-b0 :
    evaluateBuilderWire b0 external state
      (Checked.localWire (fsuc fzero))
    ≡ x0
  o0-at-b0 =
    addCarryStage-o-value
      current entry di0 s0 o0 co0 external state

  co1-at-b1 :
    evaluateBuilderWire b1 external state
      (Checked.localWire fzero)
    ≡ c2
  co1-at-b1 =
    addCarryStage-co-value
      b0 (Checked.localWire fzero)
      (Builder.liftLocalTwice di1)
      (Builder.liftLocalTwice s1)
      o1 co1 external state
    ∙ cong₃ Carry.muxCY s1-at-b0 d1-at-b0 co0-at-b0

  o1-at-b1 :
    evaluateBuilderWire b1 external state
      (Checked.localWire (fsuc fzero))
    ≡ x1
  o1-at-b1 =
    addCarryStage-o-value
      b0 (Checked.localWire fzero)
      (Builder.liftLocalTwice di1)
      (Builder.liftLocalTwice s1)
      o1 co1 external state
    ∙ cong₂ Carry.xorCY s1-at-b0 co0-at-b0

  co2-at-b2 :
    evaluateBuilderWire b2 external state
      (Checked.localWire fzero)
    ≡ c3
  co2-at-b2 =
    addCarryStage-co-value
      b1 (Checked.localWire fzero)
      (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
      (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
      o2 co2 external state
    ∙ cong₃ Carry.muxCY s2-at-b1 d2-at-b1 co1-at-b1

  o2-at-b2 :
    evaluateBuilderWire b2 external state
      (Checked.localWire (fsuc fzero))
    ≡ x2
  o2-at-b2 =
    addCarryStage-o-value
      b1 (Checked.localWire fzero)
      (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
      (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
      o2 co2 external state
    ∙ cong₂ Carry.xorCY s2-at-b1 co1-at-b1

  co3-at-b3 :
    evaluateBuilderWire b3 external state
      (Checked.localWire fzero)
    ≡ c4
  co3-at-b3 =
    addCarryStage-co-value
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state
    ∙ cong₃ Carry.muxCY s3-at-b2 d3-at-b2 co2-at-b2

  o3-at-b3 :
    evaluateBuilderWire b3 external state
      (Checked.localWire (fsuc fzero))
    ≡ x3
  o3-at-b3 =
    addCarryStage-o-value
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state
    ∙ cong₂ Carry.xorCY s3-at-b2 co2-at-b2

  o3-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire (fsuc fzero))
    ≡ x3
  o3-final = o3-at-b3

  co3-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire fzero)
    ≡ c4
  co3-final = co3-at-b3

  o2-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire (fsuc (fsuc (fsuc fzero))))
    ≡ x2
  o2-final =
    addCarryStage-preserves-wire
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state (Checked.localWire (fsuc fzero))
    ∙ o2-at-b2

  co2-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire (fsuc (fsuc fzero)))
    ≡ c3
  co2-final =
    addCarryStage-preserves-wire
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state (Checked.localWire fzero)
    ∙ co2-at-b2

  o1-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire
        (fsuc (fsuc (fsuc (fsuc (fsuc fzero))))))
    ≡ x1
  o1-final =
    addCarryStage-preserves-wire
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state
      (Builder.liftLocalTwice (Checked.localWire (fsuc fzero)))
    ∙ addCarryStage-preserves-wire
        b1 (Checked.localWire fzero)
        (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
        (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
        o2 co2 external state (Checked.localWire (fsuc fzero))
    ∙ o1-at-b1

  co1-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire
        (fsuc (fsuc (fsuc (fsuc fzero)))))
    ≡ c2
  co1-final =
    addCarryStage-preserves-wire
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state
      (Builder.liftLocalTwice (Checked.localWire fzero))
    ∙ addCarryStage-preserves-wire
        b1 (Checked.localWire fzero)
        (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
        (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
        o2 co2 external state (Checked.localWire fzero)
    ∙ co1-at-b1

  o0-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire
        (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero))))))))
    ≡ x0
  o0-final =
    addCarryStage-preserves-wire
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Checked.localWire (fsuc fzero))))
    ∙ addCarryStage-preserves-wire
        b1 (Checked.localWire fzero)
        (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
        (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
        o2 co2 external state
        (Builder.liftLocalTwice (Checked.localWire (fsuc fzero)))
    ∙ addCarryStage-preserves-wire
        b0 (Checked.localWire fzero)
        (Builder.liftLocalTwice di1)
        (Builder.liftLocalTwice s1)
        o1 co1 external state (Checked.localWire (fsuc fzero))
    ∙ o0-at-b0

  co0-final :
    evaluateBuilderWire b3 external state
      (Checked.localWire
        (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))))
    ≡ c1
  co0-final =
    addCarryStage-preserves-wire
      b2 (Checked.localWire fzero)
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice di3)))
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Builder.liftLocalTwice s3)))
      o3 co3 external state
      (Builder.liftLocalTwice
        (Builder.liftLocalTwice (Checked.localWire fzero)))
    ∙ addCarryStage-preserves-wire
        b1 (Checked.localWire fzero)
        (Builder.liftLocalTwice (Builder.liftLocalTwice di2))
        (Builder.liftLocalTwice (Builder.liftLocalTwice s2))
        o2 co2 external state
        (Builder.liftLocalTwice (Checked.localWire fzero))
    ∙ addCarryStage-preserves-wire
        b0 (Checked.localWire fzero)
        (Builder.liftLocalTwice di1)
        (Builder.liftLocalTwice s1)
        o1 co1 external state (Checked.localWire fzero)
    ∙ co0-at-b0

semanticEntry : Builder.CarryEntrySource → Bit → Carry.CarryEntry
semanticEntry Builder.ciSource bit = Carry.fromCI bit
semanticEntry Builder.cyinitSource bit = Carry.fromCYINIT bit

buildCarry4-evaluation-for-source :
  ∀ {inputCount registerCount}
    (source : Builder.CarryEntrySource)
    (current : Generic.Builder inputCount registerCount)
    (entry :
      Checked.Wire
        inputCount registerCount (Generic.builderLocalCount current))
    (di select :
      Vec
        (Checked.Wire
          inputCount registerCount (Generic.builderLocalCount current))
        4)
    (o-nets co-nets : Vec Raw.NetId 4)
    (external : Vec Bit inputCount)
    (state : Vec Bit registerCount)
  → evaluateBuilderWires
      (Builder.buildCarry4 current entry di select o-nets co-nets)
      external state
      (builtOutputWires current entry di select o-nets co-nets)
    ≡ flattenCarryOutput
        (Carry.evalCarry4
          (semanticEntry source
            (evaluateBuilderWire current external state entry))
          (evaluateBuilderWires current external state di)
          (evaluateBuilderWires current external state select))
buildCarry4-evaluation-for-source
  Builder.ciSource current entry di select o-nets co-nets external state =
  buildCarry4-evaluation
    current entry di select o-nets co-nets external state
buildCarry4-evaluation-for-source
  Builder.cyinitSource current entry di select o-nets co-nets external state =
  buildCarry4-evaluation
    current entry di select o-nets co-nets external state
  ∙ cong flattenCarryOutput
      (Carry.CI-CYINIT-same-value
        (evaluateBuilderWire current external state entry)
        (evaluateBuilderWires current external state di)
        (evaluateBuilderWires current external state select))

outputNetOrder : Vec Raw.NetId 4 → Vec Raw.NetId 4
               → Vec Raw.NetId 8
outputNetOrder
  (o0 ∷ o1 ∷ o2 ∷ o3 ∷ [])
  (co0 ∷ co1 ∷ co2 ∷ co3 ∷ []) =
  o0 ∷ o1 ∷ o2 ∷ o3
  ∷ co0 ∷ co1 ∷ co2 ∷ co3 ∷ []

lookupNets : ∀ {inputCount registerCount localCount count}
  → Vec Raw.NetId count
  → Generic.Bindings inputCount registerCount localCount
  → Vec
      (Maybe (Checked.Wire inputCount registerCount localCount))
      count
lookupNets [] bindings = []
lookupNets (net-id ∷ net-ids) bindings =
  Generic.lookupNet net-id bindings ∷ lookupNets net-ids bindings

-- Generic.Builder intentionally allows repeated raw net IDs.  In that case a
-- later binding shadows an earlier one, so eight distinct raw output
-- occurrences cannot all be recovered by lookup.  This explicit proposition
-- is the exact lookup/provenance premise needed by the semantic theorem; a
-- whole-design multiple-driver proof can discharge it downstream.

record OutputLookupProvenance
  {inputCount registerCount : ℕ}
  (current : Generic.Builder inputCount registerCount)
  (entry :
    Checked.Wire
      inputCount registerCount (Generic.builderLocalCount current))
  (di select :
    Vec
      (Checked.Wire
        inputCount registerCount (Generic.builderLocalCount current))
      4)
  (o-nets co-nets : Vec Raw.NetId 4)
  : Type₀ where
  field
    allOutputsBound :
      lookupNets
        (outputNetOrder o-nets co-nets)
        (Generic.builderBindings
          (Builder.buildCarry4
            current entry di select o-nets co-nets))
      ≡ map just
          (builtOutputWires current entry di select o-nets co-nets)

open OutputLookupProvenance public

record BoundCarry4Correspondence
  {inputCount registerCount : ℕ}
  (current : Generic.Builder inputCount registerCount)
  (entry :
    Checked.Wire
      inputCount registerCount (Generic.builderLocalCount current))
  (di select :
    Vec
      (Checked.Wire
        inputCount registerCount (Generic.builderLocalCount current))
      4)
  (o-nets co-nets : Vec Raw.NetId 4)
  (external : Vec Bit inputCount)
  (state : Vec Bit registerCount)
  : Type₀ where
  field
    rawOutputLookup :
      lookupNets
        (outputNetOrder o-nets co-nets)
        (Generic.builderBindings
          (Builder.buildCarry4
            current entry di select o-nets co-nets))
      ≡ map just
          (builtOutputWires current entry di select o-nets co-nets)

    outputEvaluation :
      evaluateBuilderWires
        (Builder.buildCarry4 current entry di select o-nets co-nets)
        external state
        (builtOutputWires current entry di select o-nets co-nets)
      ≡ flattenCarryOutput
          (Carry.evalCarry4
            (Carry.fromCI
              (evaluateBuilderWire current external state entry))
            (evaluateBuilderWires current external state di)
            (evaluateBuilderWires current external state select))

open BoundCarry4Correspondence public

buildCarry4-bound-correspondence :
  ∀ {inputCount registerCount current entry di select o-nets co-nets}
    external state
  → OutputLookupProvenance
      {inputCount = inputCount} {registerCount = registerCount}
      current entry di select o-nets co-nets
  → BoundCarry4Correspondence
      current entry di select o-nets co-nets external state
buildCarry4-bound-correspondence external state provenance =
  record
    { rawOutputLookup = allOutputsBound provenance
    ; outputEvaluation =
        buildCarry4-evaluation _ _ _ _ _ _ external state
    }