From e2091f14f3e1938f2698b873d4a5873394fa5eda Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Thu, 9 Jan 2025 15:40:30 -0500 Subject: [PATCH] more cleanup --- bedrock2/src/bedrock2/FE310CSemantics.v | 2 +- bedrock2/src/bedrock2/MetricLeakageSemantics.v | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/bedrock2/src/bedrock2/FE310CSemantics.v b/bedrock2/src/bedrock2/FE310CSemantics.v index de7523fae..37d965de5 100644 --- a/bedrock2/src/bedrock2/FE310CSemantics.v +++ b/bedrock2/src/bedrock2/FE310CSemantics.v @@ -62,7 +62,7 @@ Section WithParameters. Qed. Global Instance ext_spec : Semantics.ExtSpec := deleakaged_ext_spec. - Global Instance ext_spec_ok : Semantics.ext_spec.ok sem_ext_spec := deleakaged_ext_spec_ok. + Global Instance ext_spec_ok : Semantics.ext_spec.ok ext_spec := deleakaged_ext_spec_ok. Global Instance locals: Interface.map.map String.string word := SortedListString.map _. Global Instance env: Interface.map.map String.string (list String.string * list String.string * cmd) := diff --git a/bedrock2/src/bedrock2/MetricLeakageSemantics.v b/bedrock2/src/bedrock2/MetricLeakageSemantics.v index 570af0b1d..91765244c 100644 --- a/bedrock2/src/bedrock2/MetricLeakageSemantics.v +++ b/bedrock2/src/bedrock2/MetricLeakageSemantics.v @@ -2,6 +2,7 @@ Require Import coqutil.sanity coqutil.Byte. Require Import coqutil.Tactics.fwd. Require Import coqutil.Map.Properties. Require coqutil.Map.SortedListString. +Require Import coqutil.Z.Lia. Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord. Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth. Require Export bedrock2.Memory. @@ -261,8 +262,6 @@ Module exec. Section WithParams. eauto 10. Qed. - Require Import coqutil.Z.Lia. - Lemma eval_expr_extends_trace : forall e0 m l mc k v mc' k', eval_expr m l e0 k mc = Some (v, k', mc') -> @@ -640,7 +639,7 @@ Section WithParams. destruct IHarges as (mc'' & IH). rewrite IH. eauto. Qed. - Definition deleakaged_ext_spec := + Definition deleakaged_ext_spec : Semantics.ExtSpec := fun t mGive a args post => ext_spec t mGive a args (fun mReceive resvals klist => post mReceive resvals). Lemma deleakaged_ext_spec_ok {ext_spec_ok: ext_spec.ok ext_spec}: @@ -652,7 +651,8 @@ Section WithParams. Qed. Context (e: env). - Instance sem_ext_spec : Semantics.ExtSpec := deleakaged_ext_spec. + Existing Instance deleakaged_ext_spec. + Existing Instance deleakaged_ext_spec_ok. Lemma to_plain_exec: forall c t m l post, Semantics.exec e c t m l post ->