From 6670aaf9a8d080de424f4f65fde8a36799645c9b Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 21 Jul 2021 21:30:19 +0200
Subject: fix ci

---
 aarch64/BTL_SEsimplify.v   | 28 +++++++++++++---------------
 aarch64/ExpansionOracle.ml |  2 +-
 2 files changed, 14 insertions(+), 16 deletions(-)

(limited to 'aarch64')

diff --git a/aarch64/BTL_SEsimplify.v b/aarch64/BTL_SEsimplify.v
index 34b41eee..3e930439 100644
--- a/aarch64/BTL_SEsimplify.v
+++ b/aarch64/BTL_SEsimplify.v
@@ -14,30 +14,28 @@ Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list
 
 (* Main proof of simplification *)
 
-(*
-Lemma target_op_simplify_correct ge sp ctx op lr hrs fsv st args m: forall
+Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall
    (H: target_op_simplify op lr hrs = Some fsv)
    (REF: ris_refines ctx hrs st)
    (OK0: ris_ok ctx hrs)
-   (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args)
-   (OK2: eval_smem ctx (si_smem st) = Some m),
-   eval_sval ctx fsv = eval_operation ge sp op args m.
+   (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args),
+   eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx).
 Proof.
   unfold target_op_simplify; simpl.
-  intros H (LREF & SREF & SREG & SMEM) ? ? ?.
+  intros H ? ? ?.
   congruence.
 Qed.
 
-Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
-  (TARGET: target_cbranch_expanse hst c l = Some (c', l'))
-  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
-  (OK: hsok_local ge sp rs0 m0 hst),
-  seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
-  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
+Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall
+  (TARGET: target_cbranch_expanse hrs c l = Some (c', l'))
+  (REF: ris_refines ctx hrs st)
+  (OK: ris_ok ctx hrs),
+  eval_scondition ctx c' l' =
+  eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
 Proof.
-  unfold target_cbranch_expanse, seval_condition; simpl.
-  intros H (LREF & SREF & SREG & SMEM) ?.
+  unfold target_cbranch_expanse; simpl.
+  intros H ? ?.
   congruence.
 Qed.
 Global Opaque target_op_simplify.
-   Global Opaque target_cbranch_expanse.*)
+Global Opaque target_cbranch_expanse.
diff --git a/aarch64/ExpansionOracle.ml b/aarch64/ExpansionOracle.ml
index 0869007c..afcb29c2 100644
--- a/aarch64/ExpansionOracle.ml
+++ b/aarch64/ExpansionOracle.ml
@@ -12,4 +12,4 @@
 
 let expanse n ibf btl = btl
 
-let find_last_node_reg c = ()
+let find_last_reg c = ()
-- 
cgit