From 414c9f51fc8dcafe5a1deb873c682105ba554bb8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 10:30:41 +0100 Subject: apply_cond1_sound --- backend/CSE3analysisproof.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'backend') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 8cc009cc..75dae91a 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1288,6 +1288,36 @@ Section SOUNDNESS. Hint Resolve external_call_sound : cse3. + + Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) := + match rel with + | None => False + | Some rel => sem_rel rel rs m + end. + + Lemma apply_cond1_sound : + forall pc cond args rel rs m + (COND : (eval_condition cond (rs ## args) m) = Some true) + (REL : (sem_rel rel rs m)), + (sem_rel_b (apply_cond1 (ctx:=ctx) pc cond args rel) rs m). + Proof. + intros. + unfold apply_cond1. + destruct eq_find as [eq_id | ] eqn:FIND; cbn. + 2: assumption. + destruct PSet.contains eqn:CONTAINS. + { + pose proof (eq_find_sound pc (Cond (negate_condition cond) args) eq_id FIND) as FIND_SOUND. + unfold sem_rel in REL. + pose proof (REL eq_id (Cond (negate_condition cond) args) CONTAINS FIND_SOUND) as REL_id. + cbn in REL_id. + rewrite eval_negate_condition in REL_id. + rewrite COND in REL_id. + discriminate. + } + exact REL. + Qed. + (* Section INDUCTIVENESS. Variable fn : RTL.function. -- cgit