Library OracleLanguages.Paper
Verifiable Semantic Difference Languages
1. Introduction
In our paper, we present a general language-agnostic definition
of what a difference language for a deterministic programming
language is, an interpretation domain based on correlating oracles,
as well as several examples of such correlating oracles on a toy
imperative language, including encodings of several Relational Hoare
Logic variants, used to prove those logics' soundness.
Throughout the paper, we work on deterministic programming languages,
as defined in the ProgrammingLanguage module.
A programming language is defined by a record of type language
defining its abstract syntax prog, the set genv_type of its global
environments, the set state of its dynamic states, a return type
return_type to extract results from final states using the state_final function,
a function initial_state returning a configuration from an abstract syntax tree,
a reduction function step, decidable equality on genv_type and state as well as
a few other properties.
All our examples will be instantiated on the toy imperative language imp_language.
1.1. Programming languages
Inductive varid :=
| x | y | z | n | a | b | c | d | s | count | pow.
Lemma varid_eq_dec :
∀ x y : varid, { x = y } + {x ≠ y}.
Module Var <: MiniDecidableType.
Definition t := varid.
Definition eq_dec := varid_eq_dec.
End Var.
Module Var_as_DT := Make_UDT Var.
Require Import ProgrammingLanguage.
Require Import Imp.Lang.
Module Imp := Imp.Lang.Make Var_as_DT.
Import Imp.
Before going further in the paper, let us go through a few small
examples on imp_language, demonstrating its syntax, or how to
compute multiple reduction steps using nsteps'.
Import Imp.SmallStep.Syntax.Notations.
Example ex₁ : prog Imp.imp_language :=
{
x ← Int (-41);
IF Var x ≤ Int 0 THEN {
x ← Var x + Int 42;
y ← Var x × Int 42
} ELSE
y ← Var x × Int 10
}%AST.
Example ex₁_initial_configuration : configuration imp_language :=
initial_state imp_language ex₁.
Example ex₁_genv : genv_type imp_language :=
fst ex₁_initial_configuration.
Example ex₁_initial_state :=
snd ex₁_initial_configuration.
Example ex₁_final_state :=
fst (nsteps' ex₁_genv 10 ex₁_initial_state).
Example ex₁_final_state_is_final:
state_final ex₁_final_state ≠ None.
1.2 Reduction traces
Require Import ReductionTrace.
Example ex₁_trace : coplist (configuration imp_language) :=
program_trace imp_language ex₁.
Example ex₁_trace_actually_trace:
trace' imp_language ex₁_trace.
Example ex₁_trace_converges:
nsteps_converging_trace 10 ex₁_trace.
Amongst trace relations, we are particularly interested in “γ-correlations”,
because we will see that several interesting differences are naturally
specified by this kind of relations.
Those traces are specified in our Coq development by the gamma_correlated
predicate.
As a simple example, we define ex₂ to be the γ-correlation implied by
configuration_eq, that is, the identity relation between program traces.
Require Import ReductionTracesRelation.
Example ex₂ : trace_relation imp_language imp_language :=
gamma_correlated (configuration_eq).
Example ex₂_refl:
∀ T₁, trace' imp_language T₁ → ex₂ T₁ T₁.
2. Overview
Import ZArith.
Example P₀ (v : nat) : prog imp_language :=
{
x ← Int (Z.of_nat (S v));
a ← Int 0;
d ← Var x;
WHILE Int 0 ≤ Var d DO {
IF (Var x) % (Var d) == Int 0 THEN
a ← Var a + Var d
ELSE Skip;
d ← Var d - Int 1
};
WHILE Int 0 ≤ Var a DO
d ← Var d + Int 1
}%AST.
Example P₂ (v : nat) : prog imp_language :=
{
x ← Int (Z.of_nat (S v));
s ← Int 0;
d ← Var x;
WHILE Int 0 < Var d DO {
IF (Var x) % (Var d) == Int 0 THEN
s ← Var s + Var d
ELSE Skip;
d ← Var d - Int 1
};
WHILE Int 0 ≤ Var s DO
d ← Var d + Int 1
}%AST.
Notice that the execution of P₀ crashes during the last iteration
of its first While loop because of a division by zero, while the
execution of P₂ diverges without crashing.
Lemma P₀_crashes:
∀ v, ∃ n, nsteps_crashing_trace n (program_trace imp_language (P₀ v)).
Lemma P₂_does_not_crash:
∀ v, ¬ (∃ n, nsteps_crashing_trace n (program_trace imp_language (P₂ v))).
What could be a relevant semantic difference between P₀ and P₃?
Using the difference language for imp_language presented in the paper,
a possible difference δ between P₀ and P₃ could be written as follows:
Require Imp.ImpDifferenceLanguage.
Module ImpDifferenceLanguage := Imp.ImpDifferenceLanguage.Make Var_as_DT Imp.
Import ImpDifferenceLanguage.
Definition φ (var : varid) : varid :=
match var with
| a ⇒ s
| s ⇒ a
| var ⇒ var
end.
Program Definition φ' : Renaming.bijection varid varid :=
exist _ φ _.
Example renaming := Renaming φ'.
Definition P₁_loop_ctx v :=
CtxSeqR (x ← Int (Z.of_nat (S v)))%AST
(CtxSeqR (s ← Int 0)%AST
(CtxSeqR (d ← Var x)%AST
(CtxSeqL CtxHole
(Seq (WHILE Int 0 ≤ Var s DO d ← Var d + Int 1) Skip)%AST))).
Example P₁_loop_body := {
IF (Var x) % (Var d) == Int 0 THEN
s ← Var s + Var d
ELSE
Skip;
d ← Var d - Int 1
}%AST.
Lemma P₁_loop_body_crashes:
∀ s,
eval_exp s (Var d) = Some 0%Z →
∀ k',
nsteps υ 3 (P₁_loop_body::k', s) = None.
Example crash_fix v :=
let 'exp := (Var d) in
let 'f := (λ _, 3) in
CrashFixWhile (P₁_loop_ctx v)
P₁_loop_body
exp 0 f P₁_loop_body_crashes.
Example δ v : ImpDifferenceLanguage.t :=
Superpose
(Compare FixCrash)
(Compose
(Compare renaming)
(Compare (crash_fix v))).
In the above example, δ is a conjunction of two differences:
A difference is said to be sound (sound_program_difference) with regards
to two programs if the reduction traces of the programs are related by
its interpretation interpret.
- FixCrash, a high-level difference description stating that the first program crashes while the second does not
- The composition of two more low-level differences, stating that there exists an intermediate program P₁ such that renaming relates P₀ to P₁, and crash_fix relates P₁ to P₂
Require Import DifferenceLanguage.
Example P₁ (v : nat) : prog imp_language :=
Renaming.rename_cmd φ (P₀ v).
Lemma δ_sound:
∀ v, sound_program_difference _ _ imp_difference_language (δ v) (P₀ v) (P₂ v).
Correlating oracles provide generic relational reasoning principles.
Indeed, they reduce the proof that a relation holds between two programs'
reduction traces to a proof that an invariant holds between the initial
configurations of these programs. In this section, we give general definitions
about correlating oracles and we present a collection of correlating oracle
languages on imp_language.
Roughly speaking, a correlating oracle is a Coq program which simulates a
specific parallel execution of two compared programs in such a way that it
highlights a stream of pairs of configurations which verify a given relation.
These pairs of configurations are retrieved from the oracle state of type oracle_state
using projections functions left_genv, right_genv, left_state and right_state.
Oracles are expressed in oracle languages, which are inhabitants of the record type
oracle_language. Each oracle_language defines:
3.1. General definitions
- a type oracle_state for dynamic states,
- a type oracle_genv for global environments,
- a step function oracle_step : oracle_genv → oracle_state → option oracle_state,
- left_genv, right_genv, left_state and right_state projection functions,
- a property invariant : oracle_genv → oracle_state → Prop,
- a proof invariant_1 that this property is preserved by oracle_step
- a proof prediction_soundness that any oracle state obtained by oracle_step from a state satsifying invariant projects to left and right states that are reachable from the respective projections of the original oracle state
Import ProgrammingLanguage.
Consider as an example this simple definition of an identity_oracle language
relating pairs of identical programs of a given language:
Definition id_step {L : language} (genv : genv_type L) (os : state L) :=
ProgrammingLanguage.step L genv os.
Lemma id_step_soundness {L : language}:
∀ (genv : genv_type L) (os os' : state L),
Logic.True →
id_step genv os = Some os' →
∃ n₁ n₂,
opt_state_eq (nsteps (id genv) n₁ (id os))
(Some (id os'))
∧ opt_state_eq (nsteps (id genv) n₂ (id os))
(Some (id os'))
∧ n₁ + n₂ > 0.
Lemma id_step_completeness {L : language}:
∀ (genv : genv_type L) (os : state L),
Logic.True →
id_step genv os = None →
ProgrammingLanguage.step L genv os = None
∧ ProgrammingLanguage.step L genv os = None.
Definition identity_oracle {L : language} : oracle_language L L :=
{|
oracle_genv := genv_type L;
oracle_state := state L;
oracle_step := id_step;
left_state := id;
right_state := id;
left_genv := id;
right_genv := id;
invariant := λ genv os, Logic.True;
invariant_1 := λ genv os os' Hinv Hstep, I;
prediction_soundness := id_step_soundness;
prediction_completeness := id_step_completeness;
|}.
Notice that while genv_type identity_oracle and oracle_state identity_oracle
are defined to be the underlying language's genv_type and state,
oracle_step identiy_oracle is a custom function id_step.
This is because the definition of prediction_soundness forbids the oracle
from getting stuck. Instead, if the state is a stuck state in the underlying
semantics, we work around this restriction by not making progress.
The invariant is always satisfied as we are interested in all pairs of
identical states, and all left and right projections are identical by design.
Example ex₁_as_id_oracle : oracle_state identity_oracle :=
ex₁_initial_state.
Example ex₁_as_id_oracle_projections:
left_state identity_oracle ex₁_as_id_oracle = ex₁_initial_state
∧ right_state identity_oracle ex₁_as_id_oracle = ex₁_initial_state.
Example ex₁_as_id_oracle_step:
step imp_language tt ex₁_initial_state
= oracle_step (identity_oracle (L := imp_language)) tt ex₁_as_id_oracle.
Finite traces of programs related by an oracle are covered by that oracle,
meaning that a finite number of steps of the oracle is sufficient to get to
an oracle state which projects to the final states of both programs.
This is proved by oracle_nsteps_termination.
One can build a γ-correlation out of an oracle language.
Indeed, given an oracle language definition and a global oracle environment,
the function γ_from_oracle builds a relation between program states for which
there exists an oracle state projecting back to them while satisfying the oracle's
invariant.
By using oracle_step and the related proofs prediction_soundness and invariant_1,
oracle_gamma_correlated computes a γ-correlation relating two program traces out
of an oracle state satisfying the oracle's invariant.
Example ex₁_γ_correlation : trace_relation imp_language imp_language :=
gamma_correlated (γ_from_oracle (identity_oracle (L := imp_language)) tt).
Example ex₁_γ_correlation_1:
ex₁_γ_correlation ex₁_trace ex₁_trace.
3.2. Correlating oracle languages on imp_language
Import ImpDifferenceLanguage.OracleHelpers.
Import Renaming.
Import CrashFixWhile.
While the generic identity_oracle language can be used on imp_language, it
is not specific to that programming language, nor is it very informative.
We wrote a few oracle languages specific to imp_language that attempt to
capture some common difference classes. We already have used some of them when
defining the semantics for δ: the interpretation of renaming and crash_fix
relies on oracles of renaming_oracle and crashfixwhile_oracle respectively.
Let us go through those oracle languages.
The oracle language renaming_oracle is one of
the simplest of our oracle languages: its global environment is bijection from
variable identifiers to variable identifiers, while its dynamic state is simply
a pair of imp_language states. Its invariant asserts the pair of dynamic states
is indeed related by the bijection, and its step function execute the left and
right programs in lock-step.
We have already defined a bijection earlier with φ'.
3.2.1. Renaming
Example renaming_ex₁ v : oracle_genv renaming_oracle × oracle_state renaming_oracle :=
let '(_, S₁) := initial_state imp_language (P₀ v) in
let '(_, S₂) := initial_state imp_language (P₁ v) in
(φ', Renaming.State S₁ S₂).
Example renaming_ex₁_1 v:
invariant renaming_oracle (fst (renaming_ex₁ v)) (snd (renaming_ex₁ v)).
Import SwapAssign.
The oracle language swapassign_oracle of independent assignment
swapping describes programs that behave the
same way and only differ by swapped syntactically independent assignments.
Its definition is rather simple, but makes use of OracleLanguages.Imp.Oracles.OracleHelpers which defines a structure cont_mod and helper functions to step in both left and
right programs while keeping track of where they differ.
The global environment holds no information, while the dynamic oracle state is
a pair of left and right dynamic states and (if the left and right states are not
stuck) an OracleHelpers.cont_mod structure to dynamically keep track of the
swapped assignments in the continuations. Each step of the oracle corresponds
to exactly one step of each program unless the next statements on the continuation
are swapped assignments, in which case both assignments are evaluated in one oracle
step.
Example swap_example : cmd :=
{
a ← Int 10;
x ← Int 2;
(WHILE Int 0 ≤ Var a DO
Seq (x ← Int 42 × Var x)
(a ← (Var a - Int 1)))
}%AST.
Example swap_example' : cmd :=
{
a ← Int 10;
x ← Int 2;
(WHILE Int 0 ≤ Var a DO
Seq (a ← (Var a - Int 1))
(x ← Int 42 × Var x))
}%AST.
Example swap_assign_or : oracle_genv swapassign_oracle × oracle_state swapassign_oracle :=
let '(_, S₁) := initial_state imp_language swap_example in
let '(_, S₂) := initial_state imp_language swap_example' in
(tt, State S₁ S₂ [OracleHelpers.CmdMod
(RecMod Id (RecMod Id (RecMod (RecMod (LeafMod Swap) Id) Id)))]).
Lemma swap_assign_or_1:
invariant swapassign_oracle (fst swap_assign_or) (snd swap_assign_or).
In the definitions above, the RecMod Id (RecMod Id (RecMod (RecMod (LeafMod Swap) Id) Id)) part is a cmd_mod structure representing the syntactic change between swap_example
and swap_example': RecMod means the root AST node is the same in both trees, Id
means two subtrees are identical, and LeafMod represents a language-specific change.
In this case, RecMod Id (RecMod Id (RecMod _ Id) Id) selects the While loop of
both programs, with identical contexts. The RecMod (LeafMod Swap) Id in the hole
selects the Seq under the loops' bodies and assert there is a Swap difference
between them. This difference simply states that the two assignments are independent
(see assign_indep) and swapped.
3.2.2b. Branches swapping
Import SwapBranches.
The oracle language swapbranches_oracle of independent branches swapping describes
programs indentical except for ITE statements in which the condition has been
syntactically negated and both branches swapped (thus being semantically equivalent).
Its global static environment does not hold information, while its dynamic state
is a triple of the left and right states and a cont_mod structure.
It always performs exactly one step in each of the left and right programs and its
invariant asserts the two states' memories to be equal.
Example swap_ite_example : cmd :=
{
a ← Int 10;
IF Var a ≤ Int 42 THEN
a ← Var a + Int 12
ELSE
a ← Var a - Int 12
}%AST.
Example swap_ite_example' : cmd :=
{
a ← Int 10;
IF ¬ Var a ≤ Int 42 THEN
a ← Var a - Int 12
ELSE
a ← Var a + Int 12
}%AST.
Example swap_ite_or
: oracle_genv swapbranches_oracle × oracle_state swapbranches_oracle :=
let '(_, S₁) := initial_state imp_language swap_ite_example in
let '(_, S₂) := initial_state imp_language swap_ite_example' in
(tt, State S₁ S₂ [OracleHelpers.CmdMod
(RecMod Id (RecMod (LeafMod Negate) Id))]).
Lemma swap_ite_or_1:
invariant swapbranches_oracle (fst swap_ite_or) (snd swap_ite_or).
Import ValueChange.
Given a list of modified variables, an oracle of the oracle language valuechange_oracle describes a specific class of pair of programs which have identical control flow and only
differ in the values of the listed variables.
The global environment of such oracles are lists of potentially modified variables, and their dynamic state is simply a pair of the left and right dynamic states.
The oracle step function simply performs exactly one step in each program, while its invariants states that:
For simplicity's sake, this last condition is actually much stronger than needed, and
formally defined by same_control_cont.
- The memory of the left and right programs are equal on all variables not listed in the global environment, and
- The continuations have the same shape, with potentially modified variables not affecting conditional or loop expressions
Example valuechange_example : cmd := {
x ← Int 42;
count ← Int 5;
pow ← Int 1;
WHILE Int 0 < Var count DO {
count ← Var count - Int 1;
pow ← Var pow × Var x
}
}%AST.
Example valuechange_example' : cmd := {
x ← Int 10;
count ← Int 5;
pow ← Int 1;
WHILE Int 0 < Var count DO {
count ← Var count - Int 1;
pow ← Var pow × Var x
}
}%AST.
Example valuechange_or
: oracle_genv valuechange_oracle × oracle_state valuechange_oracle :=
let '(_, S₁) := initial_state imp_language valuechange_example in
let '(_, S₂) := initial_state imp_language valuechange_example' in
([x; pow], State S₁ S₂).
Lemma valuechange_or_1:
invariant valuechange_oracle (fst valuechange_or) (snd valuechange_or).
Import CrashFix.
Given a source code location where a crash provably occurs in a finite
number of steps whenever a given boolean expression evaluates to false
or fails to evaluate, oracles of the crashfix_oracle language describe
the addition of a defensive ITE statement to guard at the given source
code location to avoid such a crash.
As with many of the previously-described oracle languages, crashfix_oracle
makes use of a cont_mod structure and associated helpers to keep track
of the execution point at which the two programs differ.
The global environment of oracles of this language hold no information, while
their state can either be:
- A pair of program states when the left one is stuck
- A triple of the two program states and a cont_mod structure otherwise
Example crashfix_example v : cmd :=
{
x ← Int v;
y ← Int 42 % (Var x);
z ← Var x + Var y
}%AST.
Example crashfix_example' v : cmd :=
{
x ← Int v;
IF ¬ (Var x == Int 0) THEN
y ← Int 42 % (Var x)
ELSE
y ← Int 0;
z ← Var x + Var y
}%AST.
Example crash_proof:
∀ s, eval_bexp s (¬ (Var x == Int 0))%AST ≠ Some true →
∀ k',
nsteps υ ((λ _, 1) s) ((y ← Int 42 % (Var x))%AST::k', s) = None.
Example crashfix_or v
: oracle_genv crashfix_oracle × oracle_state crashfix_oracle :=
let '(_, S₁) := initial_state imp_language (crashfix_example v) in
let '(_, S₂) := initial_state imp_language (crashfix_example' v) in
let cfix := {|
condition := (¬ (Var x == Int 0))%AST;
c_then := (y ← Int 42 % (Var x))%AST;
c_else := (y ← Int 0)%AST;
crash_bound := λ s, 1;
crash_avoided_1 := crash_proof |}
in
(tt, State S₁ S₂
[OracleHelpers.CmdMod
(RecMod Id (RecMod (LeafMod cfix) Id))]).
Lemma crashfix_or_1:
∀ v, invariant crashfix_oracle (fst (crashfix_or v)) (snd (crashfix_or v)).
Notice the RecMod Id (RecMod (LeafMod cfix) Id) part in crashfix_or:
it builds a cmd_mod structure in a similar way to what we have seen
with swapassign_or, but with the concrete local difference being
represented by a record cfix containing the proof crash_proof that
the guarded statement indeed crashes when ¬ (Var x == Int 0) does not
evaluate to true.
3.2.4b. Fix off-by-one-induced crash
Import CrashFixWhile.
A common programming error is to perform one time too many iterations of
a loop. This is the kind of situations the crashfixwhile_oracle language
attempts to address.
It is similar to the crashfix_oracle except it doesn't add a new ITE
statement but changes a LE comparison to a LT comparison, effectively
guarding from a crashing iteration.
We have already used this oracle in the overview with the interpretation
of the crash_fix difference, but let us explicitly build an oracle
for the difference between P₁ and P₂.
Example crashfixwhile_or v
: oracle_genv crashfixwhile_oracle × oracle_state crashfixwhile_oracle :=
let '(_, S₁) := initial_state imp_language (P₁ v) in
let '(_, S₂) := initial_state imp_language (P₂ v) in
let cfix := {|
expression := Var d;
bound := 0%Z;
body := P₁_loop_body;
crash_bound := λ _, 3;
crash_avoided_1 := P₁_loop_body_crashes |}
in
(tt, State S₁ S₂
[OracleHelpers.CmdMod
(RecMod Id
(RecMod Id
(RecMod Id
(RecMod (LeafMod cfix) Id))))]).
Lemma crashfixwhile_or_1:
∀ v, invariant crashfixwhile_oracle (fst (crashfixwhile_or v)) (snd (crashfixwhile_or v)).
Notice that most of the work for this oracle has already been done in
the overview.
Import AbstractEquiv.
A more abstract oracle language is the abstract_equiv_oracle language,
which describes the difference between a pair of programs where sub-programs
have been replaced by provably equivalent (terminating) ones in an otherwise
syntactically equal context.
Again, this oracle language makes use of a cont_mod structure and associated
helpers, it's global environments hold no information, whereas its dynamic states
are either pairs of stuck states, or triples of left and right states and a cont_mod
structure.
Its step function performs lock-step execution of the syntactically-equal parts
of the two programs, and executes both equivalent subprograms in one single oracle
step. Thus, the left and right stores are equivalent at all times.
Example abstractequiv_example (v : Z) : prog imp_language := {
Seq (y ← Int 1) (x ← Int 0);
n ← Int 0;
WHILE (Var n < Int v) DO {
n ← Var n + Int 1;
z ← Var x + Var y;
y ← Var z;
x ← Var z - Var x
}
}%AST.
Example abstractequiv_example' (v : Z) : prog imp_language := {
Seq (x ← Int 0) (y ← Int 1);
n ← Int 0;
WHILE (Var n < Int v) DO {
n ← Var n + Int 1;
z ← Var x + Var y;
x ← Var y;
y ← Var z
}
}%AST.
Definition nsteps_helper n c s :=
match nsteps υ n ([c], s) with
| Some ([], s') ⇒ Left s'
| _ ⇒ Right n
end.
Lemma nsteps_helper_1 n c:
∀ s s',
nsteps_helper n c s = Left s' →
∃ n', nsteps υ n' ([c], s) = Some ([], s').
Program Example abstract_equiv_or v
: oracle_genv abstract_equiv_oracle × oracle_state abstract_equiv_oracle :=
let '(_, S₁) := initial_state imp_language (abstractequiv_example v) in
let '(_, S₂) := initial_state imp_language (abstractequiv_example' v) in
let c_left₁ := (Seq (y ← Int 1) (x ← Int 0))%AST in
let c_right₁ := (Seq (x ← Int 0) (y ← Int 1))%AST in
let c_left₂ := {
n ← Var n + Int 1;
z ← Var x + Var y;
y ← Var z;
x ← Var z - Var x
}%AST in
let c_right₂ := {
n ← Var n + Int 1;
z ← Var x + Var y;
x ← Var y;
y ← Var z
}%AST in
let mod₁ := {|
c_left := c_left₁;
c_right := c_right₁;
left_fun := nsteps_helper 3 c_left₁;
left_fun_spec_1 := nsteps_helper_1 3 c_left₁;
right_fun := nsteps_helper 3 c_right₁;
right_fun_spec_1 := nsteps_helper_1 3 c_right₁ |}
in
let mod₂ := {|
c_left := c_left₂;
c_right := c_right₂;
left_fun := nsteps_helper 9 c_left₂;
left_fun_spec_1 := nsteps_helper_1 9 c_left₂;
right_fun := nsteps_helper 9 c_right₂;
right_fun_spec_1 := nsteps_helper_1 9 c_right₂ |}
in
(tt, State S₁ S₂
[OracleHelpers.CmdMod
(RecMod (LeafMod mod₁)
(RecMod Id
(RecMod
(RecMod (LeafMod mod₂) Id) Id)))]).
Lemma abstract_equiv_or_1:
∀ v, invariant abstract_equiv_oracle
(fst (abstract_equiv_or v)) (snd (abstract_equiv_or v)).
The above example is a bit more involved that most of those we have seen so far.
There are two reasons for that: first, abstract_equiv_oracle, much like
crashfix_oracle and crashfixwhile_oracle, requires the user to provide proofs.
The second reason is that this example actually describes two independent local
changes, mod₁ and mod₂. This ability to describe multiple independent local
changes is shared amongst all oracle languages using cont_mod structures.
3.2.6. Minimal Relational Hoare Logic
Minimal Relational Hoare Logic is a program logic enabling deductive reasoning on
pairs of programs sharing the same structure and executing in lock-step.
Minimal RHL proofs have type minimal_rhl_proof P c₁ c₂ Q and are proofs that
the (disjoint) programs c₁ and c₂ executed with a store satisfying a
precondition P do not crash, and that, if they converge, result in a state
satisfying the postcondition Q.
The minimal_rhl_oracle language relates such programs. The global environment of
such an oracle is the postcondition that should be satisfied by the execution of
the two related programs. Its state is a 5-uple of:
The invariant ensures the store is indeed the disjoint union of the two underlying
stores, that it satisfies the current precondition, that the list of proof terms
match the left and right continuations, and that each element's post-condition
implies the following element's pre-condition.
The oracle_step function performs exactly one step in each program, and
maintains the list of proof terms accordingly. In a sense, this oracle language
provides a small-step semantics to Minimal RHL proofs.
Finally, correctness of the Minimal Relational Hoare Logic is not assumed,
but instead proved from minimal_rhl_oracle's soundness in the minimal_rhl_soundness
theorem.
- The left program state
- The right program state
- A disjoint union of that of both programs' states
- The current precondition
- A list of Minimal RHL proof terms