Library retsound

Require Import include.
Require Import memory.
Require Import memdata.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import lemmasforseplog.
Require Import inferules.
Require Import tacticsforseplog.
Require Import includeLib.
Require Import baseTac.
Require Import auxdef.

Lemma ret_rule_sound : forall (Spec:funspec) sd (I:Inv) (r:retasrt) (p: asrt),
  (p ==> r None ) -> RuleSem Spec sd I r Afalse p sret Afalse.

Lemma exitint_rule_sound : forall (Spec:funspec) sd (I:Inv) (ri:asrt)
         (p: asrt),
  (p ==> ri ) ->
    RuleSem Spec sd I arfalse ri p (sprim exint) Afalse.


Lemma rete_rule_sound :
  forall (Spec:funspec) sd (I:Inv) (r:retasrt) (p: asrt) (e : expr) (v: val)
         (t:type),
      (p ==> r (Some v) //\\ Rv e@t == v ) ->
          RuleSem Spec sd I r Afalse p (srete e) Afalse.