Circuits as streams in Coq: Verification of a sequential multiplier

Abstract

This paper presents the proof of correctness of a multiplier circuit formalized in the Calculus of Inductive Constructions. It uses a representation of the circuit as a function from the stream of inputs to the stream of outputs. We analyze the computational aspect of the impredicative encoding of coinductive types and show how it can be used to represent sequential circuits. We identify general proof principles that can be used to justify the correctness of such a circuit. The example and the principles have been formalized in the COQ proof assistant.