Circuits as streams in COQ: verification of a sequential multiplier.

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 synchronous 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.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 synchronous 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.Cet article présente la preuve formalisée dans le calcul des constructions inductives de la correction d'un circuit réalisant la multiplication sur les entiers. Le circuit est représenté par une fonction transformant la suite infinie d'entrées en une suite infinie de sorties. Nous analysons l'aspect calculatoire de la représentation imprédicative des définitions co-inductives et montrons comment cette représentation peut servir à coder un circuit synchrone. Nous identifions des principes de preuve généraux pour justifier de tels circuits. Les exemples et les principes ont été formalisés dans l'assistant à la démonstration Coq