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.