Library OracleLanguages.OracleLanguage

Basic definitions about correlating oracles.

A correlating oracle is a program that realizes a relation between reduction traces in such a way that the verification that this relation holds between the reduction traces of two programs is reduced to the proof of a program, more precisely to the proof that an invariant holds during the evaluation of a Coq program.

We are interested in defining languages of correlating oracles, each oracle language corresponding to a specific class of relations. For instance, the oracle language of "renaming"s contains all the oracles that relate pair of reduction traces (tr₁, tr₂) where the configurations of tr₁ can be obtained by a renaming of the configurations of tr₂.

An oracle language is characterized by a class of invariants that is fulfilled by its inhabitants. The purpose of this invariant is twofold: first, it represents the static property that holds between the program configurations related by the oracle; second, it is a sufficient condition for the oracle to effectively realize a trace relation (i.e. the oracle must be “productive” and it must relate actual program configurations).

Require Import Common.
Require Import ProgrammingLanguage.
Require Import ReductionTrace.
Require Import ReductionTracesRelation.

As with programming languages, we specify a record signature for oracle languages. This signature is parameterized by two programming languages, as an oracle relates a pair of programs written in two potentially different programming languages.

Oracle languages are very similar to programming languages, except they are not required to provide a decidable equality on their states.

Furthermore, oracle languages are equipped with projection functions to recover left and right program states (left_state and right_state) from an oracle state, as well as as left and right global environments (left_genv and right_genv) from global oracle environments.

Oracle languages also provide a class of invariants invariant as well as several proofs: 1. Proof invariant_1 that the invariant holds 2. Proof prediction_soundness that if an oracle configuration for which invariant holds relates two program configurations, the oracle's reduction function oracle_step is defined on this oracle state and leads to an oracle state relating two program configurations reachable from the previous ones.

Record oracle_language (L₁ L₂ : language) :=
  {

    oracle_state : Type;
    oracle_genv : Type;
    oracle_step : oracle_genv → oracle_state → option oracle_state;

    left_state :
      oracle_state → state L₁;
    right_state :
      oracle_state → state L₂;
    left_genv :
      oracle_genv → genv_type L₁;
    right_genv :
      oracle_genv → genv_type L₂;


    invariant :
      oracle_genv → oracle_state → Prop ;


    invariant_1 :
      ∀ genv os os',
        invariant genv os →
        oracle_step genv os = Some os' →
        invariant genv os';


    prediction_soundness :
      ∀ genv os os',
        invariant genv os →
        oracle_step genv os = Some os' →
        ∃ n₁ n₂,
          opt_state_eq (nsteps (left_genv genv) n₁ (left_state os))
                       (Some (left_state os'))
        ∧ opt_state_eq (nsteps (right_genv genv) n₂ (right_state os))
                       (Some (right_state os'))

        ∧ n₁ + n₂ > 0;




    prediction_completeness :
      ∀ genv os,
        invariant genv os →
        oracle_step genv os = None →
        step L₁ (left_genv genv) (left_state os) = None
        ∧ step L₂ (right_genv genv) (right_state os) = None;

  }.

An oracle realizes a specific trace relation. This trace relation relates the execution traces of two specific programs.

By contrast, an oracle language defines a trace relation relating every pair of traces for which an instance exists.

In general, a trace T₁ is related to a trace T₂ by an oracle O if:

A. T₁ starts with a configuration C₁ and T₂ starts with a configuration C₂ that are related by O.

B. Once initialized, the oracle can be executed and at each step of its execution the state of the oracle can be projected as configurations appearing in order in T₁ and T₂.

If the invariant of O holds on the initial configurations of T₁ and T₂ then A and B holds. This is guaranteed by prediction_soundness and invariant_1.

Definition oracle_correlation_relation
  {L₁ L₂ : language} (OT : oracle_language L₁ L₂)
  (genv : oracle_genv OT) (state : oracle_state OT)
: trace_relation L₁ L₂ :=
  λ tr₁ tr₂,
    let '(genv₁, S₁) := first tr₁ in
    let '(genv₂, S₂) := first tr₂ in
    trace L₁ (genv₁, S₁) tr₁ ∧ trace L₂ (genv₂, S₂) tr₂
    ∧ genv_eq L₁ (left_genv OT genv) genv₁
    ∧ genv_eq L₂ (right_genv OT genv) genv₂
    ∧ state_eq L₁ (left_state OT state) S₁
    ∧ state_eq L₂ (right_state OT state) S₂
    ∧ invariant OT genv state.

Definition correlation_relation
  {L1 L2 : language} (OT : oracle_language L1 L2)
: trace_relation L1 L2 :=
  λ tr₁ tr₂,
    ∃ genv os, oracle_correlation_relation OT genv os tr₁ tr₂.

An oracle realizes a relation between configurations of two languages.

CoFixpoint correlation_trace_from
  {L₁ L₂ : language} (OT : oracle_language L₁ L₂)
  (genv : oracle_genv OT)
  (state : oracle_state OT)
  : coplist (configuration L₁ × configuration L₂) :=
  let c₁ := (left_genv OT genv , left_state OT state ) in
  let c₂ := (right_genv OT genv , right_state OT state ) in
  match oracle_step OT genv state with
  | Some next_state ⇒
    CCons _ (c₁ , c₂ ) (correlation_trace_from OT genv next_state)
  | None ⇒

    CSingle _ (c₁ , c₂ )
  end.

Definition left_trace {L1 L2 : language}
           (cotrace : coplist (configuration L1 × configuration L2))
:= Common.map fst cotrace.

Definition right_trace {L1 L2 : language}
           (cotrace : coplist (configuration L1 × configuration L2))
:= Common.map snd cotrace.

If two traces are related by an oracle, then the oracle realizes a relation between the configurations of these two traces.

Theorem oracle_relates_configurations_of_programs
  {L₁ L₂ : language} (OT : oracle_language L₁ L₂) :
  ∀ (genv : oracle_genv OT) (state : oracle_state OT) tr₁ tr₂,
    oracle_correlation_relation OT genv state tr₁ tr₂ →
    let correlation_trace := correlation_trace_from OT genv state in
    let subtr₁ := left_trace correlation_trace in
    let subtr₂ := right_trace correlation_trace in
    included_subtrace subtr₁ tr₁ ∧ included_subtrace subtr₂ tr₂.

The definition oracle_correlation_relation defined previously only depends on the initial states of those traces, and exploiting them may rely on oracle-specific knowledge.

Fortunately, every pair of traces related by an oracle are also related by a slightly more general γ-correlation trace relation that abstracts away a few of the oracle details.

Definition γ_from_oracle {L₁ L₂ : language}
           (OT : oracle_language L₁ L₂) (genv : oracle_genv OT)
  : configuration L₁ → configuration L₂ → Prop :=
  λ c₁ c₂,
  ∃ os,
      configuration_eq c₁ (left_genv OT genv , left_state OT os )
      ∧ configuration_eq c₂ (right_genv OT genv , right_state OT os )
      ∧ invariant OT genv os.

Theorem oracle_gamma_correlated
        {L₁ L₂ : language} (OT : oracle_language L₁ L₂) :
  ∀ (genv : oracle_genv OT) (state : oracle_state OT) tr₁ tr₂,
    oracle_correlation_relation OT genv state tr₁ tr₂ →
    gamma_correlated (γ_from_oracle OT genv) tr₁ tr₂.

CoInductive oracle_eq {L₁ L₂ : language}
            (OT₁ OT₂ : oracle_language L₁ L₂)
            (genv₁ : oracle_genv OT₁) (genv₂ : oracle_genv OT₂) :
  oracle_state OT₁ → oracle_state OT₂ → Prop :=
| OracleStuckEquality :
    ∀ os₁ os₂,
      state_eq L₁ (left_state OT₁ os₁) (left_state OT₂ os₂) →
      state_eq L₂ (right_state OT₁ os₁) (right_state OT₂ os₂) →
      oracle_step OT₁ genv₁ os₁ = None →
      oracle_step OT₂ genv₂ os₂ = None →
      oracle_eq OT₁ OT₂ genv₁ genv₂ os₁ os₂
| OracleStepEquality :
    ∀ os₁ os₂ os₁' os₂',
      state_eq L₁ (left_state OT₁ os₁) (left_state OT₂ os₂) →
      state_eq L₂ (right_state OT₁ os₁) (right_state OT₂ os₂) →
      oracle_step OT₁ genv₁ os₁ = Some os₁' →
      oracle_step OT₂ genv₂ os₂ = Some os₂' →
      oracle_eq OT₁ OT₂ genv₁ genv₂ os₁' os₂' →
      oracle_eq OT₁ OT₂ genv₁ genv₂ os₁ os₂.

Lemma oracle_eq_refl:
  ∀ {L₁ L₂ : language} {OT : oracle_language L₁ L₂}
    (genv : oracle_genv OT) (os : oracle_state OT ),
    oracle_eq OT OT genv genv os os.

Lemma oracle_eq_sym:
  ∀ {L₁ L₂ : language}
    {OT₁ OT₂ : oracle_language L₁ L₂}
    (genv₁ : oracle_genv OT₁) (genv₂ : oracle_genv OT₂)
    (os₁ : oracle_state OT₁) (os₂ : oracle_state OT₂ ),
    oracle_eq OT₁ OT₂ genv₁ genv₂ os₁ os₂ →
    oracle_eq OT₂ OT₁ genv₂ genv₁ os₂ os₁.

Lemma oracle_eq_trans:
  ∀ {L₁ L₂ : language}
    {OT₁ OT₂ OT₃ : oracle_language L₁ L₂}
    (genv₁ : oracle_genv OT₁) (genv₂ : oracle_genv OT₂) (genv₃ : oracle_genv OT₃)
    (os₁ : oracle_state OT₁) (os₂ : oracle_state OT₂) (os₃ : oracle_state OT₃ ),
    oracle_eq OT₁ OT₂ genv₁ genv₂ os₁ os₂ →
    oracle_eq OT₂ OT₃ genv₂ genv₃ os₂ os₃ →
    oracle_eq OT₁ OT₃ genv₁ genv₃ os₁ os₃.

Definition oracle_nsteps {L₁ L₂} {OT : oracle_language L₁ L₂}
         (genv : oracle_genv OT)
         (n : nat) (os : oracle_state OT) :
  option (oracle_state OT) := napply (oracle_step OT genv) n os.

Definition oracle_nsteps' {L₁ L₂} {OT : oracle_language L₁ L₂}
         (genv : oracle_genv OT)
         (n : nat)
         (os : oracle_state OT) :
  oracle_state OT × nat := napply' (oracle_step OT genv) n os.

Lemma oracle_nsteps_left:
  ∀ {L₁ L₂} {OT : oracle_language L₁ L₂} genv n os os',
    invariant OT genv os →
    oracle_nsteps genv n os = Some os' →
    ∃ n',
      opt_state_eq (nsteps (left_genv OT genv) n' (left_state OT os))
                   (Some (left_state OT os')).

Lemma oracle_nsteps_right:
  ∀ {L₁ L₂} {OT : oracle_language L₁ L₂} genv n os os',
    invariant OT genv os →
    oracle_nsteps genv n os = Some os' →
    ∃ n',
      opt_state_eq (nsteps (right_genv OT genv) n' (right_state OT os))
                   (Some (right_state OT os')).

Require Import Omega.

Given a pair of programs related by an oracle, if neither those programs diverges, the oracle reaches those two programs' final states in a finite number of iterations.

Lemma oracle_nsteps_termination:
  ∀ {L₁ L₂} {OT : oracle_language L₁ L₂}
    (genv : oracle_genv OT)
    (n n' n₁ n₂ : nat) (os os' : oracle_state OT)
    S₁'' S₂'',
    let S₁ := left_state OT os in
    let S₂ := right_state OT os in
    invariant OT genv os →
    opt_state_eq (nsteps (left_genv OT genv) n₁ S₁) (Some S₁'') →
    opt_state_eq (nsteps (right_genv OT genv) n₂ S₂) (Some S₂'') →
    step L₁ (left_genv OT genv) S₁'' = None →
    step L₂ (right_genv OT genv) S₂'' = None →
    oracle_nsteps' genv n os = (os', n') →
    n ≥ n₁ + n₂ →
    let S₁' := left_state OT os' in
    let S₂' := right_state OT os' in
    state_eq L₁ S₁' S₁'' ∧ state_eq L₂ S₂' S₂'' ∧ invariant OT genv os'.

Lemma oracle_nsteps_termination'':
  ∀ {L₁ L₂} {OT : oracle_language L₁ L₂}
    (genv : oracle_genv OT)
    (os : oracle_state OT ),
    let S₁ := left_state OT os in
    let S₂ := right_state OT os in
    invariant OT genv os →
    terminates (left_genv OT genv) S₁ →
    terminates (right_genv OT genv) S₂ →
    ∃ n os',
      oracle_nsteps genv n os = Some os'
      ∧ invariant OT genv os'
      ∧ let S₁' := left_state OT os' in
        let S₂' := right_state OT os' in
          step L₁ (left_genv OT genv) S₁' = None
        ∧ step L₂ (right_genv OT genv) S₂' = None.