From 820e1ecbca864982ebc7b8efc453d057e374a4f7 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 21:34:46 +0100 Subject: [Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6 starting a new index-verimag.html on BTL doc --- scheduling/BTL_SEtheory.v | 52 +++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 55afc19a..b0765f09 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -122,9 +122,9 @@ with eval_smem ctx (sm: smem): option mem := (** The symbolic memory preserves predicate Mem.valid_pointer with respect to initial memory. Hence, arithmetic operations and Boolean conditions do not depend on the current memory of the block - (their semantics only depends on the initial memory of the block). + (their semantics only depends on the initial memory of the block). - The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. + The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. *) Lemma valid_pointer_preserv ctx sm: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs. @@ -308,31 +308,31 @@ Proof. Qed. Lemma eval_builtin_sval_arg ctx bs: - forall ba m v, - eval_builtin_sval ctx bs = Some ba -> - eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> - eval_builtin_sarg ctx m bs v. + forall ba m v, + eval_builtin_sval ctx bs = Some ba -> + eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> + eval_builtin_sarg ctx m bs v. Proof. - induction bs; simpl; - try (intros ba m v H; inversion H; subst; clear H; - intros H; inversion H; subst; - econstructor; auto; fail). - - intros ba m v; destruct (eval_sval _ _) eqn: SV; - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; auto. - - intros ba m v. - destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; eauto. - - intros ba m v. - destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; eauto. + induction bs; simpl; + try (intros ba m v H; inversion H; subst; clear H; + intros H; inversion H; subst; + econstructor; auto; fail). + - intros ba m v; destruct (eval_sval _ _) eqn: SV; + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; auto. + - intros ba m v. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. + - intros ba m v. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. Qed. Lemma eval_builtin_sarg_sval ctx m v: forall bs, -- cgit