Parallel keyed-record circuit families -- proof internals #
theorem
Complexity.Circuit.eval_parallelKeyedRecordFamily_internal
{B : Basis}
{inputWidth keyWidth payloadWidth : ℕ}
[NeZero inputWidth]
[NeZero keyWidth]
(count : ℕ)
(circuits : Fin (count + 1) → (internalGates : ℕ) × Circuit B inputWidth (keyWidth + payloadWidth) internalGates)
(input : BitString inputWidth)
(keys : Fin (count + 1) → BitString keyWidth)
(payloads : Fin (count + 1) → BitString payloadWidth)
(heval : ∀ (index : Fin (count + 1)), (circuits index).snd.eval input = Fin.append (keys index) (payloads index))
:
(parallelKeyedRecordFamily count circuits).snd.eval input = BitString.packKeyedRecords count keys payloads