Library fcallsound

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 call_ignore_exprlist_sim: forall el tl vl Spec sd I r ri q vl´ tl´ ks ge le M ir aux
 aop O v f,
 evalexprlist´ el tl vl (ge,le,M) ->
 ({[Spec, sd, I, r, ri, q ]} ||- ((curs (sfexec f ((List.rev vl) ++ (cons v nil) ++ vl´) ((List.rev tl) ++ tl´)), (kenil, ks)), (ge, le, M, ir, aux)) <_msim (aop, O))->
 ({[Spec, sd, I, r, ri, q ]} ||- ((curs (sskip (Some v)), (kenil, kfuneval f vl´ tl´ el ks)),
             (ge, le, M, ir, aux)) <_msim (aop, O )).

Lemma call_rule_sound : forall f Spec sd I r ri pre post p P el vl tp tl logicl,
         GoodFrm p ->
         Spec f = Some (pre, post, (tp, tl)) ->
         P ==> PRE[pre, vl,logicl] ** p ->
         P ==> Rvl el@tl == vl ->
           tl_vl_match tl vl = true ->
               RuleSem Spec sd I r ri P (scall f el)
                                  (EX v,POST[post, vl,v,logicl] ** p).

Lemma calle_rule_sound: forall f e l Spec sd I r ri pre post P p el v´ vl tp tl logicl,
             GoodFrm p ->
             retpost post ->
             Spec f = Some (pre, post, (tp ,tl))->
             P ==> (PRE[pre,vl,logicl]** ((addrval_to_addr l)#tp|-> v´) ** p) ->
             P ==> Rvl el @ tl == vl ->
             (((addrval_to_addr l)#tp|-> v´) **p ==> (Alval e tp l)) ->
             tl_vl_match tl vl = true ->
             RuleSem Spec sd I r ri (P)
                     (scalle e f el) (EX v, POST[post, vl, Some v,logicl] ** (addrval_to_addr l)#tp|-> v ** p).

Lemma calle_rule_lvar_sound: forall f x Spec sd t I r ri pre post P p el v´ vl tp tl logicl,
             GoodFrm p ->
             retpost post ->
             Spec f = Some (pre, post, (tp ,tl))->
             P ==> (PRE[pre,vl,logicl] ** LV x @ t |-> v´ ** p) ->
             P ==> Rvl el @ tl == vl ->
             tl_vl_match tl vl = true ->
             RuleSem Spec sd I r ri P
                     (scalle (evar x) f el) (EX v, POST[post, vl, Some v,logicl] ** LV x @ t |-> v ** p ).