Library Sem_Var


Semantics of local variable operations

@author Patryk Czarnik

Require Import List.
Require Import Common.
Require Import Program.
Require Import ProgramStructures.
Require Import RuntimeStructures.
Require Import ValuesNTypes.
Require Import ArithOps.
Require Import Arithmetic.
Require Import AllStructures.

Module of this type provides detailed semantics of local variable instructions TVarInstr.
Module Type SEM_VAR.

Included modules

  Declare Module M_AllStructures : ALL_STRUCTURES.

  Import M_AllStructures.
  Import M_Program.M_ProgramStructures.M_ValuesAndTypes.
  Import M_Program.M_ProgramStructures.
  Import M_Program.
  Import M_RuntimeStructures.M_Heap.
  Import M_RuntimeStructures.
  Import M_Arithmetics.
  Import ArithmeticOperators.

  Import List.ListNotations.
  Open Local Scope type_scope.

Var operation constraints

Load and store instructions asymmetrically support kinds of values. Original astore instruction is allowed to store reference and returnAddress values, while the aload instruction is allowed to load only reference values (a returnAddress is not allowed). This specific constraint is described in more general definitions below.

Dynamic semantics

The dynamic semantics of stack operations, provided as a relation on the top of the stack (before and after) represented as a list of values and variable array before and after intruction.
  Inductive semVar: TVarInstr → (list TValue × TVars) → (list TValue × TVars) → Prop :=
  | SemVar_load_1: vik var vars v vv,
    isLoadable vik (kindOfValue v) →
    ValVarMapping v (One vv) →
    varsGet var vars = Some vv
    semVar (VI_Load vik var) ([], vars) ([v], vars)

  | SemVar_load_2: vik var vars v vv1 vv2,
    isLoadable vik (kindOfValue v) →
    ValVarMapping v (Two vv1 vv2) →
    varsGet var vars = Some vv1
    varsGet (nextVar var) vars = Some vv2
    semVar (VI_Load vik var) ([], vars) ([v], vars)

  | SemVar_store_1: vik var vars v vv vars',
    isStorable vik (kindOfValue v) →
    ValVarMapping v (One vv) →
    vars' = varsSet var vv vars
    semVar (VI_Store vik var) ([v], vars) ([], vars')

  | SemVar_store_2: vik var vars v vv1 vv2 vars'',
    isStorable vik (kindOfValue v) →
    ValVarMapping v (Two vv1 vv2) →
    let vars' := varsSet var vv1 vars in
    vars'' = varsSet (nextVar var) vv2 vars'
    semVar (VI_Store vik var) ([v], vars) ([], vars'')

  | SemVar_iinc: var c x vars x' vars',
    varsGet var vars = Some (VVInt x) →
    x' = M_Numeric_Int.add x c
    vars' = varsSet var (VVInt x') vars
    semVar (VI_Inc var c) ([], vars) ([], vars').

Static semantics

The static (kind-level) semantics of variable operations, provided as a relation on the top of the stack projected to a list of kinds and variable array "shadows" (kind-level abstractions).
  Inductive staticSemVar: TVarInstr → (list TKind × TVarsKShadow) → (list TKind × TVarsKShadow) → Prop :=
  | StaticSemVar_load_1: vik k vk var kvars,
    isLoadable vik k
    ValVarKindMapping k (One vk) →
    varsGet var kvars = Some vk
    staticSemVar (VI_Load vik var) ([], kvars) ([k], kvars)

  | StaticSemVar_load_2: vik k vk1 vk2 var kvars,
    isLoadable vik k
    ValVarKindMapping k (Two vk1 vk2) →
    varsGet var kvars = Some vk1
    varsGet (nextVar var) kvars = Some vk2
    staticSemVar (VI_Load vik var) ([], kvars) ([k], kvars)

  | StaticSemVar_store_1: vik k vk var kvars kvars',
    isStorable vik k
    ValVarKindMapping k (One vk) →
    kvars' = varsSet var vk kvars
    staticSemVar (VI_Store vik var) ([k], kvars) ([], kvars')

  | StaticSemVar_store_2: vik k vk1 vk2 var kvars kvars'',
    isStorable vik k
    ValVarKindMapping k (Two vk1 vk2) →
    let kvars' := varsSet var vk1 kvars in
    kvars'' = varsSet (nextVar var) vk2 kvars'
    staticSemVar (VI_Store vik var) ([k], kvars) ([], kvars'')

  | StaticSemVar_iinc: var c kvars,
    varsGet var kvars = Some VKInt

    staticSemVar (VI_Inc var c) ([], kvars) ([], kvars).

Correctness

We need the following fact about variable arrays.
Ulimately, it seems to require using equivalence relation expressing extensional equality instead of "phusical equality" of variable arrays in the semantics.
Setting the same value as previous does not change a variables array.
  Axiom PVarsSetSame:
     (t:Set) (vars: TVarsGeneric t) var v1 v2,
      varsGet var vars = Some v1
      v1 = v2
      (varsSet var v2 vars) = vars.

  Lemma PvarsKAbstractionSetSame:
     vars var v1 v2,
      varsGet var vars = Some v1
      kindOfVarValue v1 = kindOfVarValue v2
      varsKAbstraction (varsSet var v2 vars) = varsKAbstraction vars.
  Proof.
    intros.
    rewrite PvarsKAbstractionConsistentSet.
    eapply PVarsSetSame.
    apply PvarsKAbstractionConsistentSome.
    eassumption.
    assumption.
  Qed.

Guarantees that every step in the dynamic semantics is covered by the static semantics.
  Lemma staticSemVarConsistent: (vi: TVarInstr) (vs vs': list TValue) (vars vars': TVars),
      semVar vi (vs, vars) (vs', vars')
      staticSemVar vi (kindOfValues vs, varsKAbstraction vars) (kindOfValues vs', varsKAbstraction vars').
  Proof.
    intros.
    inversion H; subst; clear H.

SemVar_load_1
    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_load_1.
    assumption.
    eassumption.
    apply PvarsKAbstractionConsistentSome.
    assumption.

SemVar_load_2
    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_load_2.
    assumption.
    eassumption.
    apply PvarsKAbstractionConsistentSome.
    assumption.
    apply PvarsKAbstractionConsistentSome.
    assumption.

SemVar_store_1
    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_store_1.
    assumption.
    eassumption.
    apply PvarsKAbstractionConsistentSet.

SemVar_store_2
    apply PValVarMappingConsistent in H6; simpl in H6.
    eapply StaticSemVar_store_2.
    assumption.
    eassumption.
    unfold vars'0.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKAbstractionConsistentSet.
    reflexivity.

SemVar_iinc
    rewrite (PvarsKAbstractionSetSame vars var (VVInt x) (VVInt (M_Numeric_Int.add x c))).
    constructor.
    rewrite PvarsKAbstractionConsistent.
    rewrite H5.
    simpl.
    reflexivity.
    assumption.
    simpl.
    reflexivity.
  Qed.

Guarantees that every step in the static semantics is motivated by a corresponding step in the dynamic semantics.
  Lemma staticSemVarComplete: (vi: TVarInstr) (ks ks': list TKind) (kvars kvars': TVarsKShadow),
      staticSemVar vi (ks, kvars) (ks', kvars')
       vs vs' vars vars',
           kindOfValues vs = ks
         kindOfValues vs' = ks'
         varsKAbstraction vars = kvars
         varsKAbstraction vars' = kvars'
         semVar vi (vs, vars) (vs', vars').
  Proof.
    intros.
    inversion H; subst; clear H.

StaticSemVar_load_1
    destruct (PvarsKConcretisationConsistentSome _ _ _ H7) as [vv H]; clear H7.
    decompose [and] H; clear H.
    subst vk.
    destruct (PValVarMappingConsistentInv_AVar_EVal k (One vv) H6) as [v H];
      clear H6.
    decompose [and] H; clear H; subst.
     [].
     [v].
     (varsKConcretisation kvars').
     (varsKConcretisation kvars').
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    apply PvarsKConcretisationAbstraction.
    eapply SemVar_load_1.
    assumption.
    eassumption.
    assumption.

StaticSemVar_load_2
    destruct (PvarsKConcretisationConsistentSome _ _ _ H7) as [vv1 H]; clear H7.
    decompose [and] H; clear H.
    destruct (PvarsKConcretisationConsistentSome _ _ _ H8) as [vv2 H]; clear H8.
    decompose [and] H; clear H.
    subst vk1 vk2.
    destruct (PValVarMappingConsistentInv_AVar_EVal k (Two vv1 vv2) H6) as [v H];
      clear H6.
    decompose [and] H; clear H; subst.
     [].
     [v].
     (varsKConcretisation kvars').
     (varsKConcretisation kvars').
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    apply PvarsKConcretisationAbstraction.
    eapply SemVar_load_2.
    assumption.
    eassumption.
    assumption.
    assumption.

StaticSemVar_store_1
    destruct (PValVarMappingConsistentInv_EVal_EVar _ _ H6) as [v H_];
      clear H6.
    destruct H_ as [vv12 H].
    decompose [and] H; clear H; subst.
    destruct vv12 as [vv | vv1 vv2]; simpl in H2.

    injection H2; clear H2; intros; subst.
     [v].
     [].
     (varsKConcretisation kvars).
     (varsSet var vv (varsKConcretisation kvars)).
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKConcretisationAbstraction.
    reflexivity.
    eapply SemVar_store_1.
    assumption.
    eassumption.
    reflexivity.

    discriminate H2.

StaticSemVar_store_2
    unfold kvars'0 in ×.
    destruct (PValVarMappingConsistentInv_EVal_EVar _ _ H6) as [v H_];
      clear H6.
    destruct H_ as [vv12 H].
    decompose [and] H; clear H; subst.
    destruct vv12 as [vv | vv1 vv2]; simpl in H2.

    discriminate H2.

    injection H2; clear H2; intros; subst.
     [v].
     [].
     (varsKConcretisation kvars).
     (varsSet (nextVar var) vv2 (varsSet var vv1 (varsKConcretisation kvars))).
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKConcretisationAbstraction.
    reflexivity.
    eapply SemVar_store_2.
    assumption.
    eassumption.
    reflexivity.

StaticSemVar_iinc
    destruct (PvarsKConcretisationConsistentSome _ _ _ H2) as [v H].
    decompose [and] H; clear H.
    destruct v; simpl in H0; simplify_eq H0; clear H0.
     [].
     [].
     (varsKConcretisation kvars').
     (varsSet var (VVInt (M_Numeric_Int.add ival c)) ((varsKConcretisation kvars'))).
    repeat (try split).
    apply PvarsKConcretisationAbstraction.
    rewrite PvarsKAbstractionConsistentSet.
    rewrite PvarsKConcretisationAbstraction.
    eapply PVarsSetSame.     eassumption.
    reflexivity.
    econstructor.
    eassumption.
    reflexivity.
    reflexivity.
  Qed.

  Lemma PSemVarInversion_load_1:
     vik var vs vs' vars vars',
    isCatVIK cat1 vik
    semVar (VI_Load vik var) (vs, vars) (vs', vars')
       v vv,
      isLoadable vik (kindOfValue v)
    ValVarMapping v (One vv)
    vs = []
    vs' = [v]
    vars = vars'
    varsGet var vars = Some vv.
  Proof.
    intros.
    inversion H; clear H; subst;
      (inversion H0; clear H0; subst;
       [ v; vv; tauto
       | inversion H7; clear H7; subst; inversion H6]).
  Qed.

  Lemma PSemVarInversion_store_1:
     vik var vs vars vs' vars',
    isCatVIK cat1 vik
    semVar (VI_Store vik var) (vs, vars) (vs', vars')
       v vv,
      isStorable vik (kindOfValue v)
    ValVarMapping v (One vv)
    vs = [v]
    vs' = []
    vars' = varsSet var vv vars.
  Proof.
    intros.
    inversion H; clear H; subst;
      (inversion H0; clear H0; subst;
       [ v; vv; tauto
       | unfold vars'0 in *; inversion H7; clear H7; subst v;
         inversion H5]).
  Qed.
End SEM_VAR.