Verification

Generating verification conditions

From the Dcalc intermediate representation, the module Verification.Conditions provides functions to generate verification conditions for each scope definition present in the program. These verification conditions, if proven true, can assert the well-behaved execution of the scope definition: absence of empty or conflict errors.

Related modules:

• Verification.Conditions Generates verification conditions from scope definitions

Generic solver

As Catala ambitions to mix and match different proof backends to solve the verification conditions, the compiler features a functorial interface common to all backends to rationalize the inputs and outputs. More precisely, it is sufficient for a proof backend to implement Verification.Io.Backend to enjoy the normalized input/output (I/O) of Verification.Io.BackendIO through the functor Verification.Io.MakeBackendIO.

Finally, the Verification.Solver calls the I/O functions of the different backends to perform the solving of the various verification conditions.

Related modules

• Verification.Io Common code for handling the IO of all proof backends supported
• Verification.Solver Solves verification conditions using various proof backends

Z3 proof backend

One of the way to prove the Verification.Conditions.verification_conditions true is to encode them into a Z3 query. The Catala compiler features a complete encoding of the Dcalc intermediate representation into Z3, which can be used to launch Z3 queries and collect results to inform potential Dcalc program optimizations.

Related modules:

• Verification.Z3backend Interfacing with the Z3 SMT solver