From b2c91fd80fc88f4583ceee56243c5845cb1a93ef Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 14 Mar 2020 08:15:48 +0100
Subject: no more 'admit' in CSE3

---
 backend/CSE3proof.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 888aa55e..a6de5a5f 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -678,9 +678,11 @@ Proof.
 
   - (* Istore *)
     exists (State ts tf sp pc' rs m'). split.
-    + eapply exec_Istore; try eassumption.
+    + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.
       * TR_AT. reflexivity.
-      * admit.
+      * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial.
+        rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved.
+        assumption.
     + econstructor; eauto.
       IND_STEP.
       apply store_sound with (a0:=a) (m0:=m); eauto with cse3.
-- 
cgit