Library soundness

The soundness proof of the inference rules, which are used to reasoning about the low-level statements

Require Import include.
Require Import memdata.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import inferules.
Require Import rulesound.

Theorem RuleSound:
  forall (Spec:funspec) (sd : ossched) (I:Inv) (r:retasrt) (ri:asrt)
         (pre:asrt) (s:stmts) (post:asrt),
    InfRules Spec sd I r ri pre s post ->
    RuleSem Spec sd I r ri pre s post.

Hint Resolve RuleSound.

Lemma WFFunEnv_imply_WFFuncsSim :
  forall P FSpec sd I,
    WFFunEnv P FSpec sd I ->
    WFFuncsSim P FSpec sd I .

Lemma MethSim_to_Methsim´ :
  forall P FSpec sd I s r p ri q,
    GoodI I sd ->
    WFFuncsSim P FSpec sd I ->
    RuleSem FSpec sd I r ri p s q->
    (
      forall o O aop,
        (o , O , aop ) |= p ->
        MethSim P sd (nilcont s) o aop O I r ri (lift q)
    ).

Lemma WFFunEnv_imply_Methsim´ :
  forall P FSpec sd I,
    GoodI I sd ->
    WFFunEnv P FSpec sd I ->
    WFFuncsSim´ P FSpec sd I.