Library soundness

Require Export operationalSemantics.
Require Export evidence.

Inductive twoSatisfies(s1 s2:State): TwoAssn -> Prop :=
|TwoSatisfies: forall (phi :BExpr) (E :Expr), (BEval phi s1 = Some true ->
         BEval phi s2 = Some true ->
         (Eval E s1 = Eval E s2)) ->
         twoSatisfies s1 s2 (phi, E).

Interpretation over a list

Definition twoAssnsInteprpetation (s1 s2: State) (a:TwoAssns) : Prop :=
Forall (twoSatisfies s1 s2) a.

Fixpoint twoAssnsInterpretation (s1 s2: State) (a:TwoAssns) : Prop :=
  match a with
  | h::t => (twoSatisfies s1 s2 h) /\ twoAssnsInterpretation s1 s2 t
  | [] => True
end.

Interpretation of a triple. "Valid Hoare Triple" from the paper We use X to allow us to guarantee certain expressions evaluate in the states referred to in the interpretation

Fixpoint tripleInterp (X: list SkalVar) C (asns: assns): Prop :=
match asns with
| Assns pre post =>
      (forall s s' t t',
        (forall x, In x X -> exists v1, lookup s x = Some v1 /\ exists v2, lookup s' x = Some v2) ->
        (twoAssnsInterpretation s s' pre) -> Opsem s C t -> Opsem s' C t' ->
        (twoAssnsInterpretation t t' post))
| Aforall F =>
      forall a ,
         allVarsIn (AFv a ) X =true ->
         IntersectionNull (AFv a) (Mods C) = true ->
        tripleInterp X C (F a) end.

Fixpoint backSat (X: list SkalVar ) C (asns : assns) : Prop :=
match asns with
| Assns pre post =>
     forall s t, Opsem s C t -> forall phi' x', In (phi', x') post ->
       (forall x, In x X -> exists v, lookup s x = Some v) ->
       BEval phi' t = Some true -> (exists phi, exists x, In (phi, x) pre /\
       BEval phi s = Some true)
| Aforall F =>
     (forall a,
        allVarsIn (AFv a) X = true ->
        IntersectionNull (AFv a) (Mods C) = true ->
        backSat X C (F a)) end.

Definition soundness:= forall X {C asns}, TEvid X C asns ->
(tripleInterp X C asns /\ backSat X C asns ).

Soundness statement for two implication evidence

Definition twoAImp Theta Theta' s s' := twoAssnsInterpretation s s' Theta ->
twoAssnsInterpretation s s' Theta'.

Statement for backsat in twoImplications

Definition twoIBack (Theta Theta' :TwoAssns) s := forall phi' e', BEval phi' s =Some true ->
In (phi', e') Theta' -> (exists phi, exists e, In (phi, e) Theta /\ BEval phi s = Some true).

Definition twoISoundness:= forall Theta Theta' X s s',
TIEvid X Theta Theta' -> (forall x, In x X -> (exists v, lookup s x = Some v) /\ (exists v2, lookup s' x = Some v2)) ->
twoAImp Theta Theta' s s' /\ twoIBack Theta Theta' s.

One implication soundness

Definition OISoundness := forall X b1 b2, OIEvid X b1 b2 ->
  (forall s, (forall x, In x X -> exists v, lookup s x = Some v) ->
       (BEval b1 s) = Some true ->
       (BEval b2 s) = Some true).

Definition EQSoundness := forall X e1 e2, EQEvid X e1 e2 ->
  (forall s, (forall x, In x X -> exists v, lookup s x = Some v) -> Eval e1 s = Eval e2 s).

Definition NPCsoundness := forall phi phi' s s' C X, NPCEvid X phi C phi' -> Opsem s C s' ->
BEval phi' s' = Some true -> BEval phi s = Some true.