Library eoisound

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.

Open Scope Z_scope.

Lemma eoi_ieon_rule_sound:forall Spec sd I r ri isr is id cs i aop,
                          0 <= Int.unsigned id < Z_of_nat INUM ->
                          i = Z.to_nat (Int.intval id) ->
                         RuleSem Spec sd I r ri
                        (OS[isr, true, i::is, cs] ** (getinv (I i)) //\\ <|aop|>)
                            (sprim (eoi id))
                        (OS[isrupd isr i false, true, i::is, cs] //\\ <|aop|>).

Lemma eoi_ieoff_rule_sound : forall Spec sd I r ri isr is id i cs aop,
                          0 <= Int.unsigned id < Z_of_nat INUM ->
                          i = Z.to_nat (Int.unsigned id) ->
                         RuleSem Spec sd I r ri
              (OS[isr, false, i::is, cs] //\\ <|aop|>)
                  (sprim (eoi id))
               (OS[isrupd isr i false, false, i::is, cs] //\\ <|aop|>).