Module CertC

Require Import List.
Require String.
Require Import NumC.

Module Cert.
This module describes the communication between the Ocaml oracle and the Coq code. Constraints are identified by identifiers. These identifers are opaque and we only know how to test equality of two. The main motivation was to aviod yet another data conversion between Coq and Ocaml, but it is not really strong.

  Axiom id_t: Set.
  Axiom eqId: id_t -> id_t -> bool.
  Axiom shift: id_t -> id_t -> id_t.
  Axiom idPr: id_t -> String.string.

Linear combination of constraints.
  Definition frag_t
    := list (id_t * QNum.t).

Argument for proving the inclusion of a set of constraints s in the half-space described by another constraint c. Either c is a linear combination of the constraints in s, or it is an equality and the proof is a proof of inclusion for each of its two constituting inequalities. The former proof uses Direct and the latter uses SplitEq.
  Inductive cstrT: Set
    | Direct: frag_t -> cstrT
    | SplitEq: frag_t -> frag_t -> cstrT.

Argument for proving the inclusion of a set of constraints cs in another set cs'. This can be done either by proving that each constraint of cs' is implied by cs, or by proving that cs defines an empty subspace. The former method uses Implies, the latter uses Empty.
  Inductive finalT: Set
    | Implies: list (id_t * cstrT) -> finalT
    | Empty: frag_t -> finalT.

This is the top-level definition for inclusion certificates. It makes it possible to derive intermediate constraints and thus factorize proof arguments.
  Inductive t: Type
    | Bind: id_t -> cstrT -> t -> t
    | Final: finalT -> t.

The proof argument for one constraint of the result of a join.
  Record joinEltT: Set
    := mk {
           id: id_t;
           arg1: cstrT;
           arg2: cstrT

The proof argument for the result of a join.
  Definition joinT: Set := list joinEltT.

The proof argument which justifies an assignment. AsgInv contains the necessary information for the case of an invertible operation (x := f(x)), while AsgNInv containts inversion for a non-invertible operation (e.g. x := 3).
  Inductive asgT: Set
    | AsgInv: list (id_t * t) -> t -> asgT
    | AsgNInv: t -> list (id_t * t) -> asgT.

The proof argument for the result of meet. meetCert is a regular inclusion certificate. There is need to uniquely identify constraints for specifying linear constraints. sh specifies the shift to apply to the second argument of the meet operator so that every constraint gets a unique identifier.
  Record meetT : Set
    := mkMeet {
           sh: id_t;
           meetCert: t

End Cert.