Library liblayers.compat.CompatGenSem

Generic compatsem


Section SEMANTICS.
  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModel} `{Hmwd: UseMemWithData mem}.
  Context {D} `{HD: CompatData D}.
  Context `{Tsemof: Semof (cdata D)} `{Hsemof: !Semprops T}.

Using extcall_sem


  Inductive sextcall_generic_sem (f: T) (s: stencil) (WB: blockProp):
    list valmwd (cdata D) → valmwd (cdata D) → Prop :=
      extcall_generic_sem_intro l m d v :
        semof f l d v
        sextcall_generic_sem f s WB l (m, d) v (m, ).

  Ltac inv_extcall_generic :=
    match goal with
      [ H: sextcall_generic_sem _ _ _ _ _ _ _ _ |- _ ] ⇒ inversion H; subst
    end.

  Definition sextcall_generic_info (f: T) :=
    {|
      sextcall_step := sextcall_generic_sem f;
      sextcall_csig := mkcsig targs tres;
      sextcall_valid s := true
    |}.

  Local Instance extcall_generic_properties (f: T):
    ExtcallProperties (sextcall_generic_info f).
  Proof.
    split.
    × intros s WB _ _ _ _ [l m d v H].
      eapply semprops_well_typed.
      eassumption.
    × intros s WB _ _ _ _ b [l m d v H] Hb.
      exact Hb.
    × intros s WB _ _ _ _ b ofs p [l m d v H] Hvalid Hperm.
      exact Hperm.
    × intros s WB _ _ _ _ [l m d v H].
      simpl.
      eauto with mem.
    × intros s WB _ _ _ _ [m2 d2] vargs2 [vargs1 m1 d1 v H] Hm2 Hvargs2.
      lift_auto. subst.        v, (m2, ).
      repeat split.
      + eapply semprops_lessdef in Hvargs2; eauto.
        subst.
        assumption.
      + apply Val.lessdef_refl.
      + change (m2, ) with ((fun mset fst m (m1, )) m2).
        constructor.
        assumption.
      + apply Mem.unchanged_on_refl.
    × intros s WB WB´ _ _ _ _ ι [m2 d2] vargs2 [vargs1 m1 d1 v H].
      intros Hm Hvargs HWB.
      lift_auto. subst.        ι, v, (m2, ).
      repeat split.
      + eapply semprops_inject in Hvargs; eauto.
        subst.
        assumption.
      + eapply semprops_inject_neutral.
        eassumption.
      + change (m2, ) with ((fun mset fst m (m1, )) m2).
        constructor.
        assumption.
      + apply Mem.unchanged_on_refl.
      + apply Mem.unchanged_on_refl.
      + apply inject_incr_refl.
      + rewrite H0 in H1; discriminate.
      + rewrite H0 in H1; discriminate.
    × intros s WB _ _ _ _ v2 [m2 d2] [l m1 d v1 d1 Ha] H.
      simpl in H.
      inversion H as [xl xm2 xd xv1 xd2 Hb]; subst.
      edestruct semprops_determ; [apply Ha | apply Hb | ].
      subst; eauto.
    × intros s WB1 WB2 _ _ _ _ HWB [l m d v H].
      constructor.
      assumption.
    × intros s WB _ _ _ _ b chunk o [l m d v H] Hvalid Hb.
      reflexivity.
  Qed.

Preservation of the low-level and high-level invariants cannot be shown in a generic way since they involves abstract data. Instead, we expect the user to provide an instance of the following class.

  Class PreservesInvariants (f: T) :=
    {
      semprops_low_level_invariant vargs m d vres :
        semof f vargs d vres
        low_level_invariant m d
        low_level_invariant m ;
      semprops_high_level_invariant vargs d vres :
        semof f vargs d vres
        high_level_invariant d
        high_level_invariant ;
      semprops_kernel_mode vargs d vres :
        semof f vargs d vres
        kernel_mode d
        kernel_mode
    }.

  Local Instance extcall_generic_invariants f:
    PreservesInvariants f
    ExtcallInvariants (D := cdata D) (sextcall_generic_info f).
  Proof.
    intros Hf.
    split.
    × intros s WB vargs m d vres H Hd.
      inversion H; subst.
      eapply semprops_low_level_invariant;
      eassumption.
    × intros s WB vargs m d vres H Hd.
      inversion H; subst.
      eapply semprops_high_level_invariant;
      eassumption.
    × intros s WB vargs m d vres H Hd.
      inversion H; subst.
      eapply semprops_kernel_mode;
      eassumption.
    × intros s WB vargs m d vres H.
      inversion H; subst.
      reflexivity.
    × intros s WB l m d v H.
      inversion H; subst.
      intros; split.
      + eapply semprops_inject_neutral.
        eassumption.
      + assumption.
    × intros s WB _ _ _ _ [l m d v H].
      eapply semprops_well_typed.
      eassumption.
  Qed.

  Definition gensem (f: T) `{PreservesInvariants f}: compatsem (cdata D) :=
    inl {|
      sextcall_primsem_step := sextcall_generic_info f;
      sextcall_props := OK _;
      sextcall_invs := OK _
    |}.

Using primcall_sem


  Inductive primcall_generic_sem (f: T) (s: stencil):
    Asm.regsetmwd (cdata D) → Asm.regsetmwd (cdata D) → Prop :=
      primcall_generic_sem_intro rs m d :
        semof f nil d Vundef
        primcall_generic_sem f s rs (m, d) (Asm.nextinstr rs) (m, ).

  Lemma primcall_generic_determ (f: T) s rs m rs1 rs2 m1 m2:
    primcall_generic_sem f s rs m rs1 m1
    primcall_generic_sem f s rs m rs2 m2
    m1 = m2 rs1 = rs2.
  Proof.
    intros H1 H2.
    inv H1.
    inv H2.
    exploit semprops_determ.
    eexact H.
    eexact H6.
    intros [_ Hd]; subst.
    tauto.
  Qed.
End SEMANTICS.

Tactics

This tactic is used to prove extcall_generic_sem goals.

Ltac extcall_generic_sem_intro :=
  repeat econstructor; autorewrite with monad.

Inversion tactic for extcall_generic_sem and the like

Ltac inv_generic_sem H :=
  lazymatch type of H with

    
FIXME: probably not the right number of arguments
    | external_call _ _ _ _ _ _ _

      simpl in H;
      inv_generic_sem H

    | sextcall_generic_sem ?f _ _ _ _ _ _

      let args := fresh "args" in
      let m := fresh "m" in
      let v := fresh "v" in
      let := fresh "d'" in
      let Hsemof := fresh "Hsemof" in
      let Hargs := fresh "Hargs" in
      let Hm := fresh "Hm" in
      let Hv := fresh "Hv" in
      let Ht := fresh "Ht" in
      let Hd´ := fresh "Hd'" in
      inversion H as [args m d v Hsemof Hargs Hm Hv Hm´];

      
For pure functions, it will be the case that m = . Then, we can replace with Mem.get_abstract_data m with no loss of information. Once we move to lens, we can actually use same_context to relate m and in a generic way, and do that all the time. FIXME: this needs to be updated try match type of Hd' with Mem.put_abstract_data ?m ?d' = ?m => apply (f_equal Mem.get_abstract_data) in Hd'; rewrite Mem.get_put_abstract_data in Hd' end;

      subst;
      clear H;
      rename Hsemof into H;
      inv_generic_sem H

    | primcall_generic_sem ?f _ _ _ _ _ _ _ _ _ _

      let rs := fresh "rs" in
      let m := fresh "m" in
      let := fresh "d'" in
      let Hsemof := fresh "Hsemof" in
      let Hargs := fresh "Hargs" in
      let Hrs := fresh "Hrs" in
      let Hm := fresh "Hm" in
      let Hv := fresh "Hv" in
      let Ht := fresh "Ht" in
      let Hrs´ := fresh "Hrs'" in
      let Hm´ := fresh "Hm'" in
      inversion H as [m rs Hsemof Hargs Hrs Hm Ht Hv Hrs´ Hm´];
      subst;
      clear H;
      rename Hsemof into H;
      inv_generic_sem H

    | semof ?f _ _ _ _

      unfold semof in H;
      inv_generic_sem H

    | semof_nil_void _ _ _ _ _

      let f := fresh "f" in
      let d := fresh "d" in
      let := fresh "d'" in
      let Hfd := fresh "Hfd" in
      let Hf := fresh "Hf" in
      let Hargs := fresh "Hargs" in
      let Hd := fresh "Hd" in
      let Hv := fresh "Hv" in
      let Hd´ := fresh "Hd'" in
      inversion H as [f d Hfd Hf Hargs Hd Hv Hd´];
      subst;
      clear H;
      rename Hfd into H;
      inv_generic_sem H

    | semof_nil_int _ _ _ _ _

      let f := fresh "f" in
      let d := fresh "d" in
      let z := fresh "z" in
      let := fresh "d'" in
      let Hfd := fresh "Hfd" in
      let Hf := fresh "Hf" in
      let Hargs := fresh "Hargs" in
      let Hd := fresh "Hd" in
      let Hv := fresh "Hv" in
      let Hd´ := fresh "Hd'" in
      inversion H as [f d z Hfd Hf Hargs Hd Hv Hd´];
      subst;
      clear H;
      rename Hfd into H;
      inv_generic_sem H

    | semof_nil_int_pure _ _ _ _ _

      unfold semof_nil_int_pure in H;
      inv_generic_sem H

    | semof_nil_int_pure_total _ _ _ _ _

      unfold semof_nil_int_pure_total in H;
      inv_generic_sem H

    | semof_cons _ _ _ _ _

      let f := fresh "f" in
      let i := fresh "i" in
      let args := fresh "args" in
      let d := fresh "d" in
      let v := fresh "v" in
      let := fresh "d'" in
      let Hfd := fresh "Hfd" in
      let Hf := fresh "Hf" in
      let Hargs := fresh "Hargs" in
      let Hd := fresh "Hd" in
      let Hv := fresh "Hv" in
      let Hd´ := fresh "Hd'" in
      inversion H as [f i args d v Hfd Hf Hargs Hd Hv Hd´];
      subst;
      clear H;
      rename Hfd into H;
      inv_generic_sem H

    | semof_nil_int64 _ _ _ _ _

      let f := fresh "f" in
      let d := fresh "d" in
      let z := fresh "z" in
      let := fresh "d'" in
      let Hfd := fresh "Hfd" in
      let Hf := fresh "Hf" in
      let Hargs := fresh "Hargs" in
      let Hd := fresh "Hd" in
      let Hv := fresh "Hv" in
      let Hd´ := fresh "Hd'" in
      inversion H as [f d z Hfd Hf Hargs Hd Hv Hd´];
      subst;
      clear H;
      rename Hfd into H;
      inv_generic_sem H

    | semof_nil_int64_pure _ _ _ _ _

      unfold semof_nil_int64_pure in H;
      inv_generic_sem H

    | semof_nil_int64_pure_total _ _ _ _ _

      unfold semof_nil_int64_pure_total in H;
      inv_generic_sem H

    | semof_cons64 _ _ _ _ _

      let f := fresh "f" in
      let i := fresh "i" in
      let args := fresh "args" in
      let d := fresh "d" in
      let v := fresh "v" in
      let := fresh "d'" in
      let Hfd := fresh "Hfd" in
      let Hf := fresh "Hf" in
      let Hargs := fresh "Hargs" in
      let Hd := fresh "Hd" in
      let Hv := fresh "Hv" in
      let Hd´ := fresh "Hd'" in
      inversion H as [f i args d v Hfd Hf Hargs Hd Hv Hd´];
      subst;
      clear H;
      rename Hfd into H;
      inv_generic_sem H

    
When all else fail, fall back on more generic inversion tactics. This is useful not only as a base case, but sometimes we mix generic semantics with manually defined ones in a given layer, in which case it's more convenient if a single inversion tactic works and yield similar results for both kinds.

    | _

      try (inv_monad H);
      try inv H

  end.

Effect-free functions preserve invariants


Section PRESERVES_INVARIANTS.
  Context `{Hmem: Mem.MemoryModel}.
  Context {D} `{HD: CompatData D}.

  Global Instance semof_nil_int_pure_invar (f: Doption Z):
    PreservesInvariants f.
  Proof.
    split.
    × intros vargs m d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
  Qed.

  Global Instance semof_nil_int_pure_total_invar (f: DZ):
    PreservesInvariants f.
  Proof.
    split.
    × intros vargs m d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
  Qed.

  Global Instance semof_cons_invar `{Tsemof: Semof D} (f: ZT):
    ( n, PreservesInvariants (f n)) →
    PreservesInvariants f.
  Proof.
    intros Hf.
    split.
    × intros vargs m d vres H Hinv.
      inv_generic_sem H.
      eapply semprops_low_level_invariant;
      eassumption.
    × intros vargs d vres H Hinv.
      inv_generic_sem H.
      eapply semprops_high_level_invariant;
      eassumption.
    × intros vargs d vres H.
      inv_generic_sem H.
      eapply semprops_kernel_mode;
      eassumption.
  Qed.

  Global Instance semof_nil_int64_pure_invar (f: Doption Z64):
    PreservesInvariants f.
  Proof.
    split.
    × intros vargs m d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
  Qed.

  Global Instance semof_nil_int64_pure_total_invar (f: DZ64):
    PreservesInvariants f.
  Proof.
    split.
    × intros vargs m d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
    × intros vargs d vres H.
      inv_generic_sem H.
      tauto.
  Qed.

  Global Instance semof_cons64_invar `{Tsemof: Semof D} (f: Z64T):
    ( n, PreservesInvariants (f n)) →
    PreservesInvariants f.
  Proof.
    intros Hf.
    split.
    × intros vargs m d vres H Hinv.
      inv_generic_sem H.
      eapply semprops_low_level_invariant;
      eassumption.
    × intros vargs d vres H Hinv.
      inv_generic_sem H.
      eapply semprops_high_level_invariant;
      eassumption.
    × intros vargs d vres H.
      inv_generic_sem H.
      eapply semprops_kernel_mode;
      eassumption.
  Qed.

End PRESERVES_INVARIANTS.