From 5d9b049d3214c34f7cdac5358d6bce27af90d721 Mon Sep 17 00:00:00 2001 From: Arthur Azevedo de Amorim Date: Mon, 2 Feb 2015 13:14:43 -0500 Subject: [PATCH 1/2] Add typeclass database to eauto. --- compartmentalization/main.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/compartmentalization/main.v b/compartmentalization/main.v index 7be9e6d..398e235 100644 --- a/compartmentalization/main.v +++ b/compartmentalization/main.v @@ -195,7 +195,8 @@ Proof. move => GOOD REF EXEC. elim: EXEC ast GOOD REF => {sst sst'} [sst _ |sst sst' sst'' _ STEPS EXEC IH] ast GOOD REF; first by eauto 7. have [ast' [STEPA REF']] := backward_simulation GOOD REF STEPS. -have GOOD' : Abs.good_state ast' by eapply Abs.good_state_preserved; eauto. +have GOOD' : Abs.good_state ast' + by eapply Abs.good_state_preserved; eauto with typeclass_instances. have [ast'' [EXECA [GOOD'' REF'']]] := IH _ GOOD' REF'. by eauto 7. Qed. From b62b3fc78d17271fe9f56e0c3626940d7101b458 Mon Sep 17 00:00:00 2001 From: Arthur Azevedo de Amorim Date: Fri, 6 May 2016 19:43:21 -0400 Subject: [PATCH 2/2] Update to newest versions. --- Makefile.source | 1 - README.md | 5 +- cfi/abstract.v | 8 ++-- cfi/classes.v | 2 +- cfi/concrete.v | 4 +- cfi/main.v | 4 +- cfi/preservation.v | 4 +- cfi/preservationAS.v | 24 +++++----- cfi/property.v | 4 +- cfi/refinementAS.v | 55 +++++++++++----------- cfi/refinementSC.v | 26 +++++----- cfi/rules.v | 4 +- cfi/symbolic.v | 11 ++--- common/printing.v | 2 +- common/segment.v | 7 +-- common/types.v | 12 ++--- compartmentalization/abstract.v | 11 +++-- compartmentalization/common.v | 4 +- compartmentalization/isolate_sets.v | 5 +- compartmentalization/main.v | 8 ++-- compartmentalization/ranges.v | 4 +- compartmentalization/refinementSA.v | 73 +++++++++++++++-------------- compartmentalization/symbolic.v | 27 ++++++----- concrete/concrete.v | 7 ++- concrete/exec.v | 4 +- concrete/int_32.v | 6 +-- lib/haskell_notation.v | 2 +- lib/partmap_utils.v | 32 ++++++------- lib/ssr_list_utils.v | 3 +- lib/ssr_set_utils.v | 4 +- lib/utils.v | 3 +- lib/word_utils.v | 9 ++-- memory_safety/abstract.v | 4 +- memory_safety/classes.v | 2 +- memory_safety/main.v | 4 +- memory_safety/refinementAS.v | 54 ++++++++++----------- memory_safety/symbolic.v | 4 +- sealing/abstract.v | 4 +- sealing/classes.v | 2 +- sealing/main.v | 6 +-- sealing/refinementSA.v | 18 +++---- sealing/symbolic.v | 4 +- symbolic/backward.v | 4 +- symbolic/exec.v | 4 +- symbolic/fault_handler.v | 26 +++++----- symbolic/forward.v | 4 +- symbolic/int_32.v | 4 +- symbolic/refinement_common.v | 35 +++++++------- symbolic/rules.v | 4 +- symbolic/symbolic.v | 4 +- 50 files changed, 284 insertions(+), 278 deletions(-) diff --git a/Makefile.source b/Makefile.source index 621ffc6..4c9fb8d 100644 --- a/Makefile.source +++ b/Makefile.source @@ -1,5 +1,4 @@ -R . MicroPolicies --arg -no-native-compiler lib/utils.v lib/haskell_notation.v diff --git a/README.md b/README.md index fa5cea0..a436043 100644 --- a/README.md +++ b/README.md @@ -7,9 +7,8 @@ Coq formalization accompanying the paper: ### Prerequisites -- Coq 8.5beta1 (https://coq.inria.fr/download) -- SSReflect 1.5 (for Coq 8.5beta1) (http://ssr.msr-inria.inria.fr/FTP/) -- The Mathematical Components library 1.5 (for Coq 8.5beta1) +- Coq 8.5 (https://coq.inria.fr/download) +- The Mathematical Components library 1.6 (for Coq 8.5) (http://www.msr-inria.fr/projects/mathematical-components-2/) - The CoqUtils library (https://github.com/arthuraa/coq-utils) diff --git a/cfi/abstract.v b/cfi/abstract.v index 9a97b0c..89aa146 100644 --- a/cfi/abstract.v +++ b/cfi/abstract.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import word fset partmap. Require Import lib.utils lib.ssr_list_utils common.types. Require Import cfi.property cfi.classes. @@ -142,8 +142,8 @@ Inductive step : state -> state -> Prop := Inductive step_a : state -> state -> Prop := | step_attack : forall imem dmem dmem' reg reg' pc b - (MSAME: dmem =i dmem') - (RSAME: reg =i reg'), + (MSAME: domm dmem =i domm dmem') + (RSAME: domm reg =i domm reg'), step_a (State imem dmem reg pc b) (State imem dmem' reg' pc b). diff --git a/cfi/classes.v b/cfi/classes.v index d0911a7..50b5d69 100644 --- a/cfi/classes.v +++ b/cfi/classes.v @@ -1,4 +1,4 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Import common.types. Set Implicit Arguments. diff --git a/cfi/concrete.v b/cfi/concrete.v index 7722df7..ffd93c7 100644 --- a/cfi/concrete.v +++ b/cfi/concrete.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import ord word partmap. Require Import lib.utils lib.partmap_utils. Require Import common.types. diff --git a/cfi/main.v b/cfi/main.v index 0a31be5..c0db9fb 100644 --- a/cfi/main.v +++ b/cfi/main.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrfun Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq Ssreflect.fintype MathComp.ssrint. -Require Import CoqUtils.ord CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq fintype ssrint. +From CoqUtils Require Import ord hseq word partmap. Require Import lib.utils. Require Import common.types. diff --git a/cfi/preservation.v b/cfi/preservation.v index bd23fa5..75d2636 100644 --- a/cfi/preservation.v +++ b/cfi/preservation.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.seq. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq. +From CoqUtils Require Import word partmap. Require Import lib.utils common.types cfi.property. Set Implicit Arguments. diff --git a/cfi/preservationAS.v b/cfi/preservationAS.v index 2f92746..d06c834 100644 --- a/cfi/preservationAS.v +++ b/cfi/preservationAS.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import ord word partmap. Require Import lib.utils. Require Import common.types. @@ -96,9 +96,9 @@ Proof. intros RTG r v. split. - intros GET. - by rewrite getm_map /= GET. + by rewrite mapmE /= GET. - intros GET. - rewrite getm_map /= in GET. + rewrite mapmE /= in GET. destruct (reg r) eqn:GET'. + destruct a. simpl in GET. assert (taga = DATA) @@ -111,13 +111,13 @@ Qed. Lemma untag_data_implies_dmem_refinement mem : RefinementAS.refine_dmemory - (mapm RefinementAS.untag_atom (filterm RefinementAS.is_data mem)) mem. + (mapm RefinementAS.untag_atom (filterm [fun _ => RefinementAS.is_data] mem)) mem. Proof. intros addr v. split. - intros GET. - by rewrite getm_map /= getm_filter /= GET. - - rewrite getm_map /= getm_filter /= => GET. + by rewrite mapmE /= filtermE /= GET. + - rewrite mapmE /= filtermE /= => GET. destruct (getm mem addr) eqn:GET'. + destruct a as [val tg]. simpl in GET. @@ -136,13 +136,13 @@ Definition is_instr (a : atom (mword mt) cfi_tag) := Lemma untag_instr_implies_imem_refinement mem : RefinementAS.refine_imemory - (mapm RefinementAS.untag_atom (filterm is_instr mem)) mem. + (mapm RefinementAS.untag_atom (filterm [fun _ => is_instr] mem)) mem. Proof. intros addr v. split. - intros (ut & GET). - by rewrite getm_map /= getm_filter /= GET. - - rewrite getm_map /= getm_filter /=. + by rewrite mapmE /= filtermE /= GET. + - rewrite mapmE /= filtermE /=. case GET': (getm mem addr) => [[val tg]|] //=. by case: tg GET' => [[id|]|] //= _ [<-]; simpl; eauto. Qed. @@ -329,8 +329,8 @@ Qed. Next Obligation. (*initial state*) destruct H as [TPC [ITG [VTG [ETG [RTG ?]]]]]. destruct cst as [mem reg [pc tpc] int]. - exists (Abs.State (mapm RefinementAS.untag_atom (filterm is_instr mem)) - (mapm RefinementAS.untag_atom (filterm RefinementAS.is_data mem)) + exists (Abs.State (mapm RefinementAS.untag_atom (filterm [fun _ => is_instr] mem)) + (mapm RefinementAS.untag_atom (filterm [fun _ => RefinementAS.is_data] mem)) (mapm RefinementAS.untag_atom reg) pc true). split. - unfold Abs.initial. reflexivity. diff --git a/cfi/property.v b/cfi/property.v index 1fe38c0..68070f9 100644 --- a/cfi/property.v +++ b/cfi/property.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import word partmap. Require Import lib.utils common.types. Set Implicit Arguments. diff --git a/cfi/refinementAS.v b/cfi/refinementAS.v index d415789..03343bd 100644 --- a/cfi/refinementAS.v +++ b/cfi/refinementAS.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import ord word fset partmap. Require Import lib.utils lib.partmap_utils. Require Import common.types. @@ -691,7 +691,7 @@ Proof. intros areg reg reg' RTG REF EQUIV. unfold Sym.equiv in EQUIV. unfold refine_registers in REF. - assert (MAP := getm_map untag_atom reg'). + assert (MAP := mapmE untag_atom reg'). intros r v. split. - intro GET. @@ -757,23 +757,24 @@ Definition is_data (a : atom (mword mt) cfi_tag) := Lemma refine_dmemory_domains dmem mem : refine_dmemory dmem mem -> - dmem =i (filterm is_data mem : {partmap _ -> _}). + domm dmem =i domm (filterm [fun _ => is_data] mem : {partmap _ -> _}). Proof. intros REF addr. - unfold refine_dmemory in REF; rewrite !inE. + unfold refine_dmemory in REF; rewrite !mem_domm. destruct (getm dmem addr) eqn:GET. - + destruct (getm (filterm is_data mem) addr) eqn:GET'. + + destruct (getm (filterm [fun _ => is_data] mem) addr) eqn:GET'. * auto. - * assert (FILTER := getm_filter is_data mem addr); simpl in FILTER. + * assert (FILTER := filtermE [fun _ => is_data] mem addr); simpl in FILTER. apply REF in GET. - rewrite /= GET /= in FILTER. congruence. - + destruct (getm (filterm is_data mem) addr) eqn:GET'. - * assert (FILTER := getm_filter is_data mem addr). + rewrite /= GET /= GET' in FILTER. + congruence. + + destruct (getm (filterm [fun _ => is_data] mem) addr) eqn:GET'. + * assert (FILTER := filtermE [fun _ => is_data] mem addr). simpl in FILTER. destruct (getm mem addr) eqn:GET''. - destruct a0 as [v tg]. - destruct tg; simpl in FILTER; - [idtac | apply REF in GET'']; congruence. + destruct tg; rewrite /= GET' in FILTER; + [| apply REF in GET'']; congruence. - simpl in FILTER. rewrite FILTER in GET'. congruence. * by auto. Qed. @@ -786,9 +787,9 @@ Lemma dmem_refinement_preserved_by_equiv : refine_dmemory dmem' mem'. Proof. intros dmem mem mem' REF EQUIV. - assert (FILTER := getm_filter is_data mem'). - assert (MAP := getm_map untag_atom (filterm is_data mem')). - exists (mapm untag_atom (filterm is_data mem')). subst. + assert (FILTER := filtermE [fun _ => is_data] mem'). + assert (MAP := mapmE untag_atom (filterm [fun _ => is_data] mem')). + exists (mapm untag_atom (filterm [fun _ => is_data] mem')). subst. intros addr v. split. - intro GET. @@ -803,7 +804,7 @@ Proof. + destruct a as [v' tg]. destruct tg; simpl in FILTER'; rewrite /= FILTER' in MAP'; simpl in *; congruence. - + rewrite FILTER' in MAP'. simpl in MAP'. congruence. + + by rewrite FILTER' GET /= in MAP'. Qed. Lemma dmem_domain_preserved_by_equiv : @@ -811,19 +812,19 @@ Lemma dmem_domain_preserved_by_equiv : refine_dmemory dmem mem -> Sym.equiv mem mem' -> refine_dmemory dmem' mem' -> - dmem =i dmem'. + domm dmem =i domm dmem'. Proof. intros dmem dmem' mem mem' REF EQUIV REF'. assert (DOMAINMM' := Sym.equiv_same_domain EQUIV). assert (DOMAINDM' := refine_dmemory_domains REF'). assert (DOMAINDM := refine_dmemory_domains REF). subst. - assert (FILTER := getm_filter is_data mem'). + assert (FILTER := filtermE [fun _ => is_data] mem'). intro addr. assert (FILTER' := FILTER addr). assert (EQUIV' := EQUIV addr). - assert (DOMAINFMFM': (filterm is_data mem : {partmap _ -> _}) =i - (filterm is_data mem' : {partmap _ -> _})). + assert (DOMAINFMFM': domm (filterm [fun _ => is_data] mem : {partmap _ -> _}) =i + domm (filterm [fun _ => is_data] mem' : {partmap _ -> _})). { apply filter_domains; auto. intros. assert (FILTERK := FILTER k). assert (EQUIVK := EQUIV k). @@ -842,7 +843,7 @@ Proof. - destruct EQUIVK. - constructor. } - assert (DOMAIN: dmem =i dmem'); last by apply DOMAIN. + assert (DOMAIN: domm dmem =i domm dmem'); last by apply DOMAIN. simpl in *. eapply same_domain_trans; eauto. apply same_domain_comm. eapply same_domain_trans; eauto. apply same_domain_comm; @@ -852,9 +853,9 @@ Qed. Lemma refine_reg_domains areg reg : refine_registers areg reg -> Sym.registers_tagged reg -> - areg =i reg. + domm areg =i domm reg. Proof. - intros REF RTG n; rewrite !inE. + intros REF RTG n; rewrite !mem_domm. unfold refine_registers in REF. destruct (getm areg n) eqn:GET. + destruct (getm reg n) eqn:GET'. @@ -876,16 +877,16 @@ Lemma reg_domain_preserved_by_equiv : Sym.registers_tagged reg -> Sym.equiv reg reg' -> refine_registers areg' reg' -> - areg =i areg'. + domm areg =i domm areg'. Proof. intros areg areg' reg reg' REF RTG EQUIV REF'. unfold pointwise. - intro n; rewrite !inE. + intro n; rewrite !mem_domm. assert (RTG' : Sym.registers_tagged (cfg := cfg) reg') by (eapply Sym.register_tags_preserved_by_step_a'; eauto). - assert (DOMAIN : areg =i reg) + assert (DOMAIN : domm areg =i domm reg) by (apply refine_reg_domains; auto). - assert (DOMAIN' : areg' =i reg') + assert (DOMAIN' : domm areg' =i domm reg') by (apply refine_reg_domains; auto). assert (EQUIV' := EQUIV n). clear EQUIV. destruct (getm reg n) eqn:GET, (getm reg' n) eqn:GET'; rewrite GET in EQUIV'. diff --git a/cfi/refinementSC.v b/cfi/refinementSC.v index f2d6c21..5261b4a 100644 --- a/cfi/refinementSC.v +++ b/cfi/refinementSC.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import ord word partmap. Require Import lib.utils lib.partmap_utils. Require Import common.types. @@ -100,15 +100,15 @@ Lemma mem_refinement_equiv : Sym.equiv smem smem'. Proof. intros smem cmem cmem' REF EQUIV. - exists (mapm (coerce Symbolic.M) (filterm (is_user Symbolic.M) cmem')). + exists (mapm (coerce Symbolic.M) (filterm [fun _ => is_user Symbolic.M] cmem')). split. { (*refinement proof*) split. { move=> addr v ct t /= DEC CGET. - rewrite getm_map /= getm_filter /=. + rewrite mapmE /= filtermE /=. by rewrite CGET /is_user /= DEC /= /coerce DEC. } { move=> addr v t /=. - rewrite getm_map /= getm_filter /=. + rewrite mapmE /= filtermE /=. case CGET: (getm cmem' addr) => [[cv ctg]|] //=. rewrite /is_user /=. case DEC: (rules.fdecode _ _) => [[t'|]|] //=. @@ -129,7 +129,7 @@ Proof. destruct EQUIV as [v0 v'' ct ut ct' ut' EQ1 DEC1 EQ2 DEC2 SEQUIV|NEQ EQ]; subst. * inv EQ1. inv EQ2. - rewrite getm_map /= getm_filter /= CGET' /= + rewrite mapmE /= filtermE /= CGET' /= /is_user /= DEC2 /= /coerce /= DEC2. rewrite /= DEC1 in DEC. move: DEC => [?]. by subst. @@ -141,7 +141,7 @@ Proof. + by destruct EQUIV. - destruct (getm cmem addr) eqn:CGET. + destruct a as [v ctg]. unfold refinement_common.refine_memory in REF. - rewrite getm_map /= getm_filter /=. + rewrite mapmE /= filtermE /=. case CGET': (getm cmem' addr) EQUIV => [a|] //= EQUIV. rewrite /is_user /=. destruct EQUIV @@ -153,7 +153,7 @@ Proof. by rewrite DEC; eauto. } + destruct (getm cmem' addr) eqn:CGET'. * destruct EQUIV. - * rewrite getm_map /= getm_filter /=. + * rewrite mapmE /= filtermE /=. rewrite CGET'. simpl. constructor. } Qed. @@ -167,15 +167,15 @@ Lemma reg_refinement_equiv : Sym.equiv sregs sregs'. Proof. intros sreg creg creg' cmem REF EQUIV. - exists (mapm (coerce Symbolic.R) (filterm (is_user Symbolic.R) creg')). + exists (mapm (coerce Symbolic.R) (filterm [fun _ => is_user Symbolic.R] creg')). split. { (*Refinement proof*) split. { move=> n v ctg tg /= DEC CGET'. - by rewrite getm_map /= getm_filter /= + by rewrite mapmE /= filtermE /= CGET' /= /is_user /= DEC /= /coerce /= DEC. } { move=> n v tg. - rewrite getm_map /= getm_filter /=. + rewrite mapmE /= filtermE /=. case CGET': (creg' n)=> [[v' t']|] //=. rewrite /is_user /= /coerce /=. case CTG: (rules.fdecode _ _) => [[ut|?]|] //=. @@ -192,7 +192,7 @@ Proof. - destruct a as [v utg]. move: (proj2 REF n v utg SGET) => [ctg DEC CGET]. rewrite CGET in E1. inversion E1; subst v1 t1; clear E1. - rewrite getm_map /= getm_filter /=. + rewrite mapmE /= filtermE /=. destruct EQUIV as [v0 v'' ? ? ? ut' EQ1 DEC1 EQ2 DEC2 SEQUIV|NEQ EQ]; subst. * inv EQ1. inv EQ2. rewrite /= DEC1 in DEC. inv DEC. @@ -201,7 +201,7 @@ Proof. * inv EQ. simpl in NEQ. suff: False by []. by apply: NEQ; eexists; eauto. - - rewrite getm_map /= getm_filter /=. + - rewrite mapmE /= filtermE /=. rewrite E2. simpl. destruct EQUIV as [v0 v'' ? ? ? ut' EQ1 DEC1 EQ2 DEC2 SEQUIV|NEQ EQ]; subst. diff --git a/cfi/rules.v b/cfi/rules.v index 804a2e8..d8ea00c 100644 --- a/cfi/rules.v +++ b/cfi/rules.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat. -Require Import CoqUtils.hseq. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. +From CoqUtils Require Import hseq. Require Import lib.utils common.types symbolic.symbolic. Require Import cfi.classes. diff --git a/cfi/symbolic.v b/cfi/symbolic.v index d7ada31..60dcbad 100644 --- a/cfi/symbolic.v +++ b/cfi/symbolic.v @@ -1,6 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool. -Require Import Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import ord word partmap fset. Require Import lib.utils lib.partmap_utils. Require Import common.types. @@ -80,7 +79,7 @@ Inductive step_a : Symbolic.state mt -> Lemma equiv_same_domain (T : ordType) (m m' : {partmap T -> atom (mword mt) cfi_tag}) : equiv m m' -> - m =i m'. + domm m =i domm m'. Proof. exact: pointwise_same_domain. Qed. Local Notation "x .+1" := (x + 1)%w. @@ -236,12 +235,12 @@ Proof. end); match_inv; subst; try (simpl; assumption). + simpl in E. simpl. unfold instructions_tagged. intros addr i0 id GET. - move: E GET; rewrite /updm OLD /= => - [<-]; rewrite getm_set. + move: E GET; rewrite /updm OLD /= => - [<-]; rewrite setmE. have [EQ //|/eqP NEQ GET] := altP (addr =P w1); simpl in NEQ; subst. specialize (INVARIANT _ _ _ GET); assumption. + simpl in E. simpl. unfold instructions_tagged. move=> addr i0 id; move: E; rewrite /updm OLD /= => - [<-]. - rewrite getm_set. + rewrite setmE. have [EQ //|/eqP NEQ GET] := altP (addr =P w1); simpl in NEQ; subst. specialize (INVARIANT _ _ _ GET); assumption. + unfold Symbolic.run_syscall in CALL. simpl in CALL. diff --git a/common/printing.v b/common/printing.v index 129b37e..9c7470d 100644 --- a/common/printing.v +++ b/common/printing.v @@ -3,7 +3,7 @@ Require Import String. Require Import Ascii. Require Import ZArith. Require Import NPeano. -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. Import String. diff --git a/common/segment.v b/common/segment.v index 0145e97..f91130b 100644 --- a/common/segment.v +++ b/common/segment.v @@ -1,6 +1,7 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.choice Ssreflect.fintype. -Require Import MathComp.div MathComp.ssrint MathComp.ssralg MathComp.intdiv. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype div ssrint ssralg + intdiv. +From CoqUtils Require Import ord word partmap. Require Import lib.utils common.types. diff --git a/common/types.v b/common/types.v index fb0b37a..ddf8503 100644 --- a/common/types.v +++ b/common/types.v @@ -1,6 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.choice Ssreflect.fintype. -Require Import MathComp.div MathComp.ssrint MathComp.ssralg MathComp.intdiv. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype div ssrint ssralg intdiv. +From CoqUtils Require Import ord word partmap. Require Import lib.utils. @@ -173,15 +173,13 @@ Definition unpickle_opcode (n : nat) : option opcode := Lemma pickle_opcodeK : pcancel pickle_opcode unpickle_opcode. Proof. by do !case. Qed. -Definition opcode_ordMixin := PcanOrdMixin pickle_opcodeK. -Canonical opcode_ordType := Eval hnf in OrdType opcode opcode_ordMixin. - Definition opcode_choiceMixin := PcanChoiceMixin pickle_opcodeK. Canonical opcode_choiceType := Eval hnf in ChoiceType opcode opcode_choiceMixin. - Definition opcode_countMixin := CountMixin pickle_opcodeK. Canonical opcode_countType := Eval hnf in CountType opcode opcode_countMixin. +Definition opcode_ordMixin := PcanOrdMixin pickle_opcodeK. +Canonical opcode_ordType := Eval hnf in OrdType opcode opcode_ordMixin. Definition max_opcode := 24. diff --git a/compartmentalization/abstract.v b/compartmentalization/abstract.v index 5e79ec6..a82f248 100644 --- a/compartmentalization/abstract.v +++ b/compartmentalization/abstract.v @@ -1,5 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq MathComp.bigop Ssreflect.choice Ssreflect.fintype MathComp.finset. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq bigop choice fintype finset. +From CoqUtils Require Import word partmap. Require Import lib.utils common.types. Require Import lib.ssr_list_utils lib.ssr_set_utils. Require Import compartmentalization.isolate_sets compartmentalization.common. @@ -1256,7 +1257,7 @@ Proof. [clear GET; rename GET' into GET | discriminate]. move: GET UPDR; rewrite /updm. case: (M p) => [m'|] //= GET [<-]. - rewrite getm_set GET. + rewrite setmE GET. by case: (_ == _). + unfold syscall_address_space in *; cbv [address_space] in *. move: SAS => /existsP [sc /and3P [NGET TABLED /eqP ->]]. @@ -1264,7 +1265,7 @@ Proof. move: (UPDR); rewrite /updm /= => SET. destruct (M p) as [old|] eqn:GET; [|discriminate]. assert (NEQ : sc <> p) by by intro; subst; rewrite GET in NGET. - by move: SET => /= [<-]; rewrite getm_set (introF eqP NEQ). + by move: SET => /= [<-]; rewrite setmE (introF eqP NEQ). - (* Syscall *) assert (GOOD' : good_state MM') by (apply syscall_step_preserves_good with MM sc; subst; assumption); @@ -1448,7 +1449,7 @@ Proof. in STEP; eauto 3. by rewrite inE in VALID; replace c0 with c in * by eauto 3; apply/orP. + move: UPDR DIFF; rewrite /updm; case: (M p) => [?|] //= [<-]. - by rewrite getm_set (negbTE NE). + by rewrite setmE (negbTE NE). - (* Syscall *) unfold get_syscall,table in *; simpl in *. repeat match type of GETSC with diff --git a/compartmentalization/common.v b/compartmentalization/common.v index 6e1182d..ef4bcae 100644 --- a/compartmentalization/common.v +++ b/compartmentalization/common.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import word partmap. Require Import lib.utils common.types. Set Bullet Behavior "Strict Subproofs". diff --git a/compartmentalization/isolate_sets.v b/compartmentalization/isolate_sets.v index 061ef27..b602c29 100644 --- a/compartmentalization/isolate_sets.v +++ b/compartmentalization/isolate_sets.v @@ -1,5 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.finset MathComp.ssrint. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finset ssrint. +From CoqUtils Require Import word partmap. Require Import lib.utils common.types. Require Import compartmentalization.ranges. diff --git a/compartmentalization/main.v b/compartmentalization/main.v index 398e235..73d9593 100644 --- a/compartmentalization/main.v +++ b/compartmentalization/main.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.fintype Ssreflect.seq MathComp.ssrint MathComp.finset. -Require Import CoqUtils.ord CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype fintype seq ssrint finset. +From CoqUtils Require Import ord hseq word partmap. Require Import lib.utils lib.partmap_utils. Require Import common.types. @@ -43,7 +43,7 @@ Lemma read_kernel_word_monotonic mem addr x ct x' ct' : read_kernel_word (setm mem addr x'@ct') =1 read_kernel_word mem. Proof. move=> Hget Hnk Hnk' addr'. - rewrite /read_kernel_word getm_set. + rewrite /read_kernel_word setmE. have [-> {addr'} /=|//] := altP (addr' =P addr). by rewrite Hget /= (negbTE Hnk) (negbTE Hnk'). Qed. @@ -83,7 +83,7 @@ Lemma read_set_monotonic mem addr x ct x' ct' : read_set mem =1 read_set (setm mem addr x'@ct'). Proof. move=> Hget Hnk Hnk' addr'. - rewrite /read_set getm_set. + rewrite /read_set setmE. have [-> {addr'} /=|_] := altP (addr' =P addr). by rewrite Hget /= (negbTE Hnk) (negbTE Hnk'). case: (mem addr') => [count|] //=. diff --git a/compartmentalization/ranges.v b/compartmentalization/ranges.v index f79454a..88ed605 100644 --- a/compartmentalization/ranges.v +++ b/compartmentalization/ranges.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat. -Require Import CoqUtils.ord CoqUtils.word. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. +From CoqUtils Require Import ord word. Require Import common.types. Section WithClasses. diff --git a/compartmentalization/refinementSA.v b/compartmentalization/refinementSA.v index 016ae3c..a4ac004 100644 --- a/compartmentalization/refinementSA.v +++ b/compartmentalization/refinementSA.v @@ -1,5 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.finset. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finset. +From CoqUtils Require Import ord word fset partmap. Require Import lib.utils lib.partmap_utils common.types. Require Import symbolic.symbolic. @@ -135,8 +136,8 @@ Definition refine_previous_b (sk : where_from) (prev : Abs.compartment mt) end. Definition refine_syscall_addrs_b (AM : memory mt) (SM : Sym.memory mt) : bool := - [&& all (fun x => x \notin AM) syscall_addrs , - all (fun x => x \notin SM) syscall_addrs & + [&& all (fun x => x \notin domm AM) syscall_addrs , + all (fun x => x \notin domm SM) syscall_addrs & uniq syscall_addrs ]. Record refine (ast : astate) (sst : sstate) : Prop := RefineState @@ -577,7 +578,7 @@ Proof. rewrite /Sym.supd /=. move=> UPD REF p'. case REP: (repm m p _) UPD => [m''|]. - - generalize (getm_rep REP p') => {REP} REP [<- _ _ _ _ _ _]. + - generalize (repmE REP p') => {REP} REP [<- _ _ _ _ _ _]. rewrite REP. have [->|NE] := (p' =P p); last exact: REF. move: {REF} (REF p). @@ -593,12 +594,12 @@ Lemma supd_refine_syscall_addrs_b AM sst sst' p l : Proof. move=> UPD /and3P [Ha Hs Hu]. apply/and3P; split=> // {Ha Hu}; apply/allP=> x /(allP Hs). - rewrite !inE; case E: (getm _ _) => [//|] _. + rewrite !mem_domm; case E: (getm _ _) => [//|] _. by rewrite (Sym.get_supd_none E UPD). Qed. -Lemma sget_supd_good_internal (sst sst' : sstate) p c I1 W1 I2 W2 : - (forall c', c' \in I2 :|: W2 -> (c' < Sym.next_id (Symbolic.internal sst))%ord) -> +Lemma sget_supd_good_internal (sst sst' : sstate) p (c : mword mt) I1 W1 I2 W2 : + (forall c' : mword mt, c' \in I2 :|: W2 -> (c' < Sym.next_id (Symbolic.internal sst))%ord) -> Sym.sget sst p ?= Sym.DATA c I1 W1 -> Sym.supd sst p (Sym.DATA c I2 W2) ?= sst' -> Sym.good_internal sst -> @@ -1554,13 +1555,13 @@ Proof. have DIFF : cid <> Snext. { intros ?; subst. eapply Sym.sget_lt_next in RINT; [simpl in RINT | eassumption]. - by rewrite Ord.leqxx in RINT. + by rewrite Ord.ltxx in RINT. } have DIFF_sys : cid_sys <> Snext. { intros ?; subst. eapply Sym.sget_lt_next in RINT; [simpl in RINT | eassumption]. - by rewrite Ord.leqxx in RINT. + by rewrite Ord.ltxx in RINT. } have NIN : pc' \notin A'. { @@ -1609,7 +1610,7 @@ Proof. move: ASS => /allP/(_ _ AIN)/orP [UAS | SAS]. - have IN' : sc \in Aprev by move/subsetP in SUBSET_A'; apply SUBSET_A'. move/forall_inP/(_ _ IN') in UAS. - by rewrite inE UAS in ANGET. + by rewrite mem_domm UAS in ANGET. - rewrite /Abs.syscall_address_space /Abs.address_space /= in SAS. move: SAS => /existsP [sc' /and3P [NONE ELEM /eqP?]]; subst Aprev. move: SUBSET_A'; rewrite subset1; move => /orP [] /eqP?; subst A'. @@ -1713,7 +1714,7 @@ Proof. specialize (UAS _ pc_in_c_sys); simpl in UAS. rewrite -(lock eq) in IS_ISOLATE; subst. - by rewrite /= inE UAS in ANGET. + by rewrite /= mem_domm UAS in ANGET. } have SYSCALL_c_sys : Abs.syscall_address_space AM c_sys. { @@ -1798,7 +1799,7 @@ Proof. case GETp': (Sym.sget _ _) => [[cp' Ip' Wp']|] //= [E]. subst cp'. move: (Sym.sget_lt_next RINT GETp') => /=. - by rewrite Ord.leqxx. + by rewrite Ord.ltxx. + rewrite -RPREV RC_rest // => NEW. rewrite in_rem_all in c1_in_AC. case/andP: c1_in_AC => [/eqP ? ?]. @@ -1811,7 +1812,7 @@ Proof. case GETp': (Sym.sget _ _) => [[cp' Ip' Wp']|] //= [E]. subst cp'. move: (Sym.sget_lt_next RINT GETp') => /=. - by rewrite Ord.leqxx. + by rewrite Ord.ltxx. + rewrite !RC_rest //. rewrite !in_rem_all in c1_in_AC c2_in_AC. case/andP: c1_in_AC => ? ?; case/andP: c2_in_AC => ? ?. @@ -1835,7 +1836,9 @@ Proof. case: OR_Is => [-> // | <-{I2}]. rewrite inE in_set1. suff: cid != Snext by move=> /negbTE-> //. - suff: (cid < Snext)%ord by apply: contra => /eqP ->; rewrite Ord.leqxx. + suff: (cid < Snext)%ord. + rewrite Ord.ltNge. + by apply: contra => /eqP ->; rewrite Ord.leqxx. move: RPREV; rewrite /get_compartment_id. case: pickP => // x /eqP cid_set []?; subst x. have: Some cid == Some cid by apply eq_refl. @@ -1860,7 +1863,7 @@ Proof. case: (p' \in J'); first by rewrite in_setU1 eqxx. apply/esym/negbTE/negP=> Snext_in_I'. have /(_ Snext)/= := bounded_tags RINT Hold'. - by rewrite in_setU Snext_in_I' Ord.leqxx => /(_ erefl). + by rewrite in_setU Snext_in_I' Ord.ltxx => /(_ erefl). * have /(_ p') := Sym.retag_set_not_in def_s'. move: (p'_nin_sets). rewrite -(mem_enum (mem (A' :|: J' :|: S'))) {2 3}/Sym.sget /= => H /(_ H) {H} <-. @@ -1869,7 +1872,7 @@ Proof. case Hold': (Sym.sget _ _)=> [[cid' I' W']|//] /=. apply/esym/negbTE/negP=> Snext_in_I'. have /(_ Snext)/= := bounded_tags RINT Hold'. - by rewrite in_setU Snext_in_I' Ord.leqxx => /(_ erefl). + by rewrite in_setU Snext_in_I' Ord.ltxx => /(_ erefl). + move/(_ c' c'_in_AC') in RC_rest. rewrite RC_rest => GCI_cid'. move: (c'_in_AC'); rewrite in_rem_all => /andP [c'_neq_prev c'_in_AC]. @@ -1886,7 +1889,9 @@ Proof. case: OR_Is => [-> // | <-{I2}]. rewrite inE in_set1. suff: cid' != Snext by move=> /negbTE-> //. - suff: (cid' < Snext)%ord by apply: contra => /eqP ->; rewrite Ord.leqxx. + suff: (cid' < Snext)%ord. + rewrite Ord.ltNge. + by apply: contra => /eqP ->; rewrite Ord.leqxx. move: GCI_cid'; rewrite /get_compartment_id. case: pickP => // x /eqP cid'_set []?; subst x. have: Some cid' == Some cid' by apply eq_refl. @@ -1918,7 +1923,7 @@ Proof. case: OR_Ws => [-> // | <-{W2}]. rewrite inE in_set1. suff: cid != Snext by move=> /negbTE-> //. - suff: (cid < Snext)%ord by apply: contra => /eqP ->; rewrite Ord.leqxx. + suff: (cid < Snext)%ord by rewrite Ord.ltNge; apply: contra => /eqP ->; rewrite Ord.leqxx. move: RPREV; rewrite /get_compartment_id. case: pickP => // x /eqP cid_set []?; subst x. have: Some cid == Some cid by apply eq_refl. @@ -1943,7 +1948,7 @@ Proof. case: (p' \in S'); first by rewrite in_setU1 eqxx. apply/esym/negbTE/negP=> Snext_in_W'. have /(_ Snext)/= := bounded_tags RINT Hold'. - by rewrite in_setU Snext_in_W' orbT Ord.leqxx => /(_ erefl). + by rewrite in_setU Snext_in_W' orbT Ord.ltxx => /(_ erefl). * have /(_ p') := Sym.retag_set_not_in def_s'. move: (p'_nin_sets). rewrite -(mem_enum (mem (A' :|: J' :|: S'))) {2 3}/Sym.sget /= => H /(_ H) {H} <-. @@ -1952,7 +1957,7 @@ Proof. case Hold': (Sym.sget _ _)=> [[cid' I' W']|//] /=. apply/esym/negbTE/negP=> Snext_in_W'. have /(_ Snext)/= := bounded_tags RINT Hold'. - by rewrite in_setU Snext_in_W' orbT Ord.leqxx => /(_ erefl). + by rewrite in_setU Snext_in_W' orbT Ord.ltxx => /(_ erefl). + move/(_ c' c'_in_AC') in RC_rest. rewrite RC_rest => GCI_cid'. move: (c'_in_AC'); rewrite in_rem_all => /andP [c'_neq_prev c'_in_AC]. @@ -1969,7 +1974,7 @@ Proof. case: OR_Ws => [-> // | <-{W2}]. rewrite inE in_set1. suff: cid' != Snext by move=> /negbTE-> //. - suff: (cid' < Snext)%ord by apply: contra => /eqP ->; rewrite Ord.leqxx. + suff: (cid' < Snext)%ord by rewrite Ord.ltNge; apply: contra => /eqP ->; rewrite Ord.leqxx. move: GCI_cid'; rewrite /get_compartment_id. case: pickP => // x /eqP cid'_set []?; subst x. have: Some cid' == Some cid' by apply eq_refl. @@ -2138,7 +2143,7 @@ Proof. solve [ eassumption | rewrite /Sym.sget /= PC; reflexivity ]]. rewrite /refine_registers /pointwise in RREGS *; intros r'. - rewrite getm_set. + rewrite setmE. destruct (r' == r) eqn:EQ_r; move/eqP in EQ_r; [subst r'|]. * erewrite getm_upd_eq by eauto. by unfold refine_reg_b. @@ -2180,7 +2185,7 @@ Proof. solve [ eassumption | rewrite /Sym.sget /= PC; reflexivity ]]. rewrite /refine_registers /pointwise in RREGS *; intros r2'. - rewrite getm_set. + rewrite setmE. destruct (r2' == r2) eqn:EQ_r2; move/eqP in EQ_r2; [subst r2'|]. * erewrite getm_upd_eq by eauto. by specialize RREGS with r1; rewrite GET1 R1W /refine_reg_b in RREGS *. @@ -2225,7 +2230,7 @@ Proof. solve [ eassumption | rewrite /Sym.sget /= PC; reflexivity ]]. unfold updm; rewrite /refine_registers /pointwise in RREGS *; intros r3'. - rewrite getm_set. + rewrite setmE. destruct (r3' == r3) eqn:EQ_r3; move/eqP in EQ_r3; [subst r3'|]. * erewrite getm_upd_eq by eauto. { unfold refine_reg_b. apply/eqP; f_equal. @@ -2280,7 +2285,7 @@ Proof. | eassumption | rewrite /Sym.sget /= PC; reflexivity ]]. unfold updm; rewrite /refine_registers /pointwise in RREGS *; intros r2'. - rewrite getm_set. + rewrite setmE. destruct (r2' == r2) eqn:EQ_r2; move/eqP in EQ_r2; [subst r2'|]. * erewrite getm_upd_eq by eauto. by specialize RMEMS with w1; @@ -2364,7 +2369,7 @@ Proof. * { unfold updm; rewrite /refine_memory /refine_mem_loc_b /pointwise in RMEMS *; intros p. - rewrite getm_set. + rewrite setmE. destruct (p == w1) eqn:EQ_w1; move/eqP in EQ_w1; [subst p|]. - erewrite getm_upd_eq by eauto. by specialize RMEMS with w1; rewrite GETM1 in RMEMS *. @@ -2375,7 +2380,7 @@ Proof. move: def_mem' Hc'. rewrite !/Sym.sget /updm. case GET': (getm mem w1) => [[x tg]|] // [<-]. - rewrite getm_set. + rewrite setmE. by have [->|NE //] := (c' =P w1); rewrite GET'. * move=> c' c'_in_AC. rewrite -(get_compartment_id_same _ SAME). @@ -2408,14 +2413,14 @@ Proof. rewrite /Sym.sget /= PC; reflexivity. * have not_syscall : w1 \notin syscall_addrs. { apply/negP => contra; case/and3P: RSC => /allP /(_ _ contra). - by rewrite inE GETM1. } + by rewrite mem_domm GETM1. } case/and3P: RSC => [Ha Hs Hu]; apply/and3P; split=> //. - apply/allP=> x x_in_sc; rewrite inE getm_set; move: x_in_sc not_syscall. - by have [{x}-> ->|_ /(allP Ha _)] := altP (x =P _). + apply/allP=> x x_in_sc; rewrite mem_domm setmE; move: x_in_sc not_syscall. + by have [{x}-> ->|_ /(allP Ha _)] := altP (x =P _); rewrite // mem_domm. apply/allP=> x x_in_sc; rewrite inE. move: def_mem'; rewrite /updm OLD /= => - [<-]. - rewrite getm_set; move: x_in_sc not_syscall. - by have [{x}-> ->|_ /(allP Hs _)] := altP (x =P _). + rewrite mem_domm setmE; move: x_in_sc not_syscall. + by have [{x}-> ->|_ /(allP Hs _)] := altP (x =P _); rewrite // mem_domm. * rewrite /Sym.good_internal /= in RINT *. case: RINT=> /= Hbounded Hisolate. { split. @@ -2555,7 +2560,7 @@ Proof. solve [ eassumption | rewrite /Sym.sget /= PC; reflexivity ]]. rewrite /refine_registers /pointwise in RREGS *; intros r'. - rewrite getm_set. + rewrite setmE. destruct (r' == ra) eqn:EQ_r'; move/eqP in EQ_r'; [subst r'|]. * erewrite getm_upd_eq by eauto. by simpl. diff --git a/compartmentalization/symbolic.v b/compartmentalization/symbolic.v index 4e9afd7..d8c6860 100644 --- a/compartmentalization/symbolic.v +++ b/compartmentalization/symbolic.v @@ -1,6 +1,7 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.finset. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finset. -Require Import CoqUtils.ord CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From CoqUtils Require Import ord hseq word partmap fset. Require Import lib.utils lib.word_utils common.types. Require Import symbolic.symbolic. @@ -496,7 +497,7 @@ Proof. rewrite /supd /= /repm /sget. case GET: (getm m p) => [[x L']|] /=. - move=> {r' pc' ni'} [<- _ _ _ <- <- <-] p' /=. - rewrite getm_set. + rewrite setmE. by have [{p'} _|NE] := (p' =P p). - move: GET; have [{p} ->|NE1] := (p =P _). { move=> GET {r' pc' ni'} [<- _ _ _ <- <- <-] p'. @@ -536,7 +537,7 @@ Proof. rewrite /supd /= /repm /sget. case GET: (getm m p) => [[v tg]|] /=. - move=> [<- _ _ _ <- <- <-]. - rewrite getm_set. + rewrite setmE. by have [{p'} ->|NE] := (p' =P p); first by rewrite GET. - do !case: (p =P _) => ? //; subst. + move=> [<- _ _ _ <- <- <-]. @@ -557,7 +558,7 @@ Theorem get_supd_eq s s' p x L L' : Proof. case: s => m r pc [ni it atjt atst]; case: s' => m' r' pc' [ni' it' atjt' atst'] /=. rewrite /supd /repm => -> /= [<- _ _ _ _ _ _]. - by rewrite getm_set eqxx. + by rewrite setmE eqxx. Qed. Theorem get_supd_neq s s' p p' v : @@ -569,7 +570,7 @@ Proof. rewrite /supd. case REP: (repm _ _ _) => [m''|]. - move=> [<- _ _ _ _ _ _]. - by rewrite (getm_rep REP) (introF (_ =P _) NE). + by rewrite (repmE REP) (introF (_ =P _) NE). - repeat case: (p =P _) => _ //=; congruence. Qed. @@ -582,7 +583,7 @@ Proof. rewrite /supd. case REP: (repm _ _ _) => [m''|]. - move=> [<- _ _ _ _ _ _]. - rewrite (getm_rep REP) NONE. + rewrite (repmE REP) NONE. move: REP. rewrite /repm. have [{p'} <-|//] := (p =P p'). by rewrite NONE. @@ -598,7 +599,7 @@ Proof. rewrite /supd. case REP: (repm m p _) => [m''|]. - move=> [<- _ _ _ _ _ _] p' /=. - rewrite (getm_rep REP). + rewrite (repmE REP). have [->|_] := (p' =P p) => //. by case: (getm m p) => [[? ?]|]. - repeat case: (p =P _) => _; congruence. @@ -702,12 +703,12 @@ Qed. Lemma retag_one_preserves_get_definedness ok retag s p s' : retag_one ok retag s p ?= s' -> - forall p, Symbolic.mem s p = Symbolic.mem s' p :> bool. + domm (Symbolic.mem s) =i domm (Symbolic.mem s'). Proof. rewrite /retag_one. case GET: (sget _ _) => [[cid I W]|] //=. case: (ok _ _ _ _) => //=. - case: (retag _ _ _ _) => [cid' I' W'] //= UPD p'. + case: (retag _ _ _ _) => [cid' I' W'] //= UPD p'; rewrite !mem_domm. have [{p'} ->|NEQ] := (p' =P p). - case GET': (Symbolic.mem s p) => [[x L]|]. + by rewrite (get_supd_eq GET' UPD). @@ -717,11 +718,11 @@ Qed. Lemma retag_set_preserves_get_definedness ok retag ps s s' : retag_set ok retag ps s ?= s' -> - Symbolic.mem s =i Symbolic.mem s'. + domm (Symbolic.mem s) =i domm (Symbolic.mem s'). Proof. move=> H. have := (@ofoldl_preserve _ _ _ _ _ _ _ (@retag_one_preserves_get_definedness ok retag) _ _ H). -by apply; eauto. +by apply=> // ??? e1 e2 p; rewrite (e1 p). Qed. Lemma retag_one_preserves_registers ok retag s p s' : @@ -1024,7 +1025,7 @@ Proof. { move=> sc cid I W sc_is_sc Hsget. apply/negP=> /eqP ?. subst cid. move: (Hbounds sc cnew I W Hsget cnew). - by rewrite -setUA in_setU1 eqxx /= Ord.leqxx => /(_ erefl). } + by rewrite -setUA in_setU1 eqxx /= Ord.ltxx => /(_ erefl). } elim: ps s Hpreserved Hisolated Hretag => [ s _ _ [<-] // | p ps IH ] s Hpreserved Hisolated. diff --git a/concrete/concrete.v b/concrete/concrete.v index 5214b60..c107684 100644 --- a/concrete/concrete.v +++ b/concrete/concrete.v @@ -1,5 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq MathComp.ssrint. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq choice ssrint. +From CoqUtils Require Import ord word partmap. Require Import lib.utils common.types. @@ -56,6 +57,8 @@ Definition mvec_of_tuple tup : mvec mt := Lemma tuple_of_mvecK : cancel tuple_of_mvec mvec_of_tuple. Proof. by case. Qed. +Definition mvec_choiceMixin := CanChoiceMixin tuple_of_mvecK. +Canonical mvec_choiceType := Eval hnf in ChoiceType (mvec mt) mvec_choiceMixin. Definition mvec_ordMixin := CanOrdMixin tuple_of_mvecK. Canonical mvec_ordType := Eval hnf in OrdType (mvec mt) mvec_ordMixin. diff --git a/concrete/exec.v b/concrete/exec.v index 1e64470..c2c97dc 100644 --- a/concrete/exec.v +++ b/concrete/exec.v @@ -1,7 +1,7 @@ (* Executable formulation of concrete machine semantics *) -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.ssrnat Ssreflect.eqtype MathComp.ssrint. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssrint. +From CoqUtils Require Import word partmap. Require Import lib.utils common.types concrete.concrete. Import Concrete. Import DoNotation. diff --git a/concrete/int_32.v b/concrete/int_32.v index 17b21e5..d5f942b 100644 --- a/concrete/int_32.v +++ b/concrete/int_32.v @@ -1,8 +1,8 @@ (* Instantiate the concrete machine with 32-bit integers *) -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.choice Ssreflect.fintype. -Require Import MathComp.ssrint MathComp.tuple. -Require Import CoqUtils.hseq CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype ssrint tuple. +From CoqUtils Require Import hseq ord word partmap. Require Import lib.utils. Require Import common.types common.printing. diff --git a/lib/haskell_notation.v b/lib/haskell_notation.v index 2f4ba1c..cd4c1a7 100644 --- a/lib/haskell_notation.v +++ b/lib/haskell_notation.v @@ -1,4 +1,4 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun. +From mathcomp Require Import ssreflect ssrfun. Require Import lib.utils. diff --git a/lib/partmap_utils.v b/lib/partmap_utils.v index 0270cc9..57b8bfe 100644 --- a/lib/partmap_utils.v +++ b/lib/partmap_utils.v @@ -1,7 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool. -Require Import Ssreflect.eqtype. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype. -Require Import CoqUtils.ord CoqUtils.partmap. +From CoqUtils Require Import ord partmap fset. Set Implicit Arguments. Unset Strict Implicit. @@ -41,9 +40,9 @@ Qed. Lemma pointwise_same_domain P m1 m2 : pointwise P m1 m2 -> - m1 =i m2. + domm m1 =i domm m2. Proof. -move=> H k; move: {H} (H k); rewrite !inE. +move=> H k; move: {H} (H k); rewrite !mem_domm. destruct (getm m1 k) eqn:?; destruct (getm m2 k) eqn:?; tauto. Qed. @@ -56,7 +55,7 @@ Lemma refine_upd_pointwise2 P m1 m1' m2 m2' k v1 v2 : Proof. rewrite /updm; move=> pm1m2; move: (pm1m2 k). case: (m1 k) => [v1'|] //; case: (m2 k) => [v2'|] //= _ pv1v2 [<-] [<-] k'. -move/(_ k'): pm1m2; rewrite !getm_set. +move/(_ k'): pm1m2; rewrite !setmE. by case: (_ == _). Qed. @@ -70,7 +69,7 @@ Proof. rewrite /updm; move=> pm1m2; move: (pm1m2 k). case: (m2 k) => [v2'|] //; case: (m1 k) => [v1'|] //= _ pv1v2 [<-]. eexists; split; eauto=> k'. -by move/(_ k'): pm1m2; rewrite !getm_set; case: (_ == _). +by move/(_ k'): pm1m2; rewrite !setmE; case: (_ == _). Qed. End Pointwise. @@ -80,13 +79,13 @@ Section SameDomain. Variables (T : ordType) (S1 S2 S3 : Type). Lemma same_domain_trans (m : {partmap T -> S1}) (m' : {partmap T -> S2}) (m'' : {partmap T -> S3}) : - m =i m' -> - m' =i m'' -> - m =i m''. + domm m =i domm m' -> + domm m' =i domm m'' -> + domm m =i domm m''. Proof. by move=> h1 h2 k; rewrite -h2. Qed. Lemma same_domain_comm (m : {partmap T -> S1}) (m' : {partmap T -> S2}) : - m =i m' -> m' =i m. + domm m =i domm m' -> domm m' =i domm m. Proof. by move=> h k; rewrite h. Qed. End SameDomain. @@ -144,7 +143,7 @@ Lemma getm_upd_eq m m' key val : m' key = Some val. Proof. rewrite /updm; case: (m key) => [val' [<-]|//]. -by rewrite getm_set eqxx. +by rewrite setmE eqxx. Qed. Lemma getm_upd_neq m m' (key key' : T) (val : S) : @@ -153,7 +152,7 @@ Lemma getm_upd_neq m m' (key key' : T) (val : S) : m' key' = m key'. Proof. rewrite /updm; case: (m key) => [val'|] //= NEQ [<-]. -by rewrite getm_set (introF eqP NEQ). +by rewrite setmE (introF eqP NEQ). Qed. Lemma getm_upd m m' k v : @@ -167,15 +166,16 @@ by rewrite (getm_upd_neq Hneq Hupd). Qed. Lemma filter_domains (f : S -> bool) m m' : - m =i m' -> + domm m =i domm m' -> (forall k, match getm m k, getm m' k with | Some v, Some v' => f v = f v' | None, None => True | _, _ => False end) -> - (filterm f m : {partmap T -> S}) =i (filterm f m' : {partmap T -> S}). + domm (filterm [fun _ => f] m : {partmap T -> S}) =i + domm (filterm [fun _ => f] m' : {partmap T -> S}). Proof. -move => SAME E k; rewrite !inE; do! rewrite getm_filter /=. +move => SAME E k; do! rewrite mem_domm filtermE /=. case GET: (getm m k) (E k) => [v|] {E} E; case GET': (getm m' k) E => [v'|] E //=. rewrite E. diff --git a/lib/ssr_list_utils.v b/lib/ssr_list_utils.v index dfb0843..cf0b71e 100644 --- a/lib/ssr_list_utils.v +++ b/lib/ssr_list_utils.v @@ -1,5 +1,4 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool. -Require Import Ssreflect.eqtype Ssreflect.seq. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq. Require Import lib.utils. diff --git a/lib/ssr_set_utils.v b/lib/ssr_set_utils.v index 6a6dcba..5d2ad90 100644 --- a/lib/ssr_set_utils.v +++ b/lib/ssr_set_utils.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool. -Require Import Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq MathComp.bigop Ssreflect.fintype MathComp.finset. +From mathcomp Require Import + ssreflect ssrfun ssrbool ssrnat eqtype ssrnat seq bigop fintype finset. Set Implicit Arguments. Unset Strict Implicit. diff --git a/lib/utils.v b/lib/utils.v index ff5f5e2..1b25104 100644 --- a/lib/utils.v +++ b/lib/utils.v @@ -1,5 +1,4 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrfun. -Require Import Ssreflect.eqtype Ssreflect.seq. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype seq. Set Implicit Arguments. Unset Strict Implicit. diff --git a/lib/word_utils.v b/lib/word_utils.v index ffe5e26..feed1f5 100644 --- a/lib/word_utils.v +++ b/lib/word_utils.v @@ -1,5 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrfun Ssreflect.eqtype Ssreflect.ssrnat MathComp.div MathComp.ssrint MathComp.intdiv. -Require Import CoqUtils.ord CoqUtils.word. +From mathcomp Require Import + ssreflect ssrbool ssrfun eqtype ssrnat fintype div ssrint intdiv. +From CoqUtils Require Import ord word. Set Implicit Arguments. Unset Strict Implicit. @@ -27,7 +28,7 @@ Qed. Lemma leqw_succ : forall n (x y : word n), x < y -> x < x + 1. Proof. -move=> n [[x Px]] [[y Py]]; do !rewrite !/Ord.leq /=. +move=> n [[x Px]] [[y Py]]; do !rewrite ?Ord.ltNge !/Ord.leq /=. rewrite -!ltnNge !modz_nat !absz_nat !modn_mod. case: n Px Py => [|k Px Py Pxy] /=. by rewrite expn0 modn1; case: x y => [|x] [|y]. @@ -39,7 +40,7 @@ Qed. Lemma addw_le : forall n (x y : word n), x < y -> x + 1 <= y. Proof. -move=> n [[x Px]] [[y Py]]; do !rewrite !/Ord.leq /=. +move=> n [[x Px]] [[y Py]]; do !rewrite ?Ord.ltNge !/Ord.leq /=. rewrite -!ltnNge /= !modz_nat !absz_nat !modn_mod. case: n Px Py => [|k Px Py Pxy] /=. by rewrite expn0 modn1; case: x y => [|x] [|y]. diff --git a/memory_safety/abstract.v b/memory_safety/abstract.v index 0a2474f..b1e5b48 100644 --- a/memory_safety/abstract.v +++ b/memory_safety/abstract.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.ssrint. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype ssrint. +From CoqUtils Require Import ord word partmap. Require Import lib.utils. Require Import common.types memory_safety.classes. diff --git a/memory_safety/classes.v b/memory_safety/classes.v index 1414054..c5369d4 100644 --- a/memory_safety/classes.v +++ b/memory_safety/classes.v @@ -1,4 +1,4 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Import common.types. Set Implicit Arguments. diff --git a/memory_safety/main.v b/memory_safety/main.v index dd7c3bc..ffeeaab 100644 --- a/memory_safety/main.v +++ b/memory_safety/main.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.seq MathComp.ssrint. -Require Import CoqUtils.hseq CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrbool eqtype seq ssrint. +From CoqUtils Require Import hseq ord word partmap. Require Import lib.utils lib.word_utils. Require Import common.types. diff --git a/memory_safety/refinementAS.v b/memory_safety/refinementAS.v index 1cd7814..72685a9 100644 --- a/memory_safety/refinementAS.v +++ b/memory_safety/refinementAS.v @@ -1,8 +1,8 @@ Ltac type_of x := type of x. -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype. -Require Import MathComp.ssrint MathComp.ssralg. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype + ssrint ssralg. +From CoqUtils Require Import ord word partmap. Require Import lib.utils lib.partmap_utils common.types symbolic.symbolic. Require Import memory_safety.abstract memory_safety.symbolic. Require Import memory_safety.classes. @@ -270,7 +270,7 @@ eexists; split; first by []; do!split=> //. rewrite hn /Abstract.getv. have -> /=: base + pt.2 - base = pt.2. rewrite addwC; exact: GRing.addrK. - rewrite getm_set eqxx size_cat /= size_take size_drop gt_pt. + rewrite setmE eqxx size_cat /= size_take size_drop gt_pt. rewrite addnS -addSn addnC subnK // gt_pt. by rewrite nth_cat size_take gt_pt ltnn subnn /=. have [{n'}-> /rmem|neq_n] := altP (n' =P n). @@ -280,7 +280,7 @@ eexists; split; first by []; do!split=> //. rewrite addwC; apply/eqP/esym. exact: GRing.subrK. move: {w1'}(w1' - base) => w1' neq_w1'. - rewrite /Abstract.getv /= get_pt getm_set eqxx. + rewrite /Abstract.getv /= get_pt setmE eqxx. rewrite size_cat size_take /= size_drop gt_pt. rewrite addnS -addSn addnC subnK //. have [lt_w1'|//] := boolP (w1' < _). @@ -292,7 +292,7 @@ eexists; split; first by []; do!split=> //. by rewrite nth_drop addnC subnK. by rewrite eq_w1' eqxx in neq_w1'. move/rmem; case hn': (mi n') => [[b base']|//]. - rewrite /Abstract.getv (lock subw) /= -lock getm_set. + rewrite /Abstract.getv (lock subw) /= -lock setmE. case hb: (amem b) => [fr'|] //. suff /negbTE -> : b != pt.1 by []. apply: contra neq_n => /eqP ?; subst b. @@ -635,8 +635,8 @@ Proof. move=> fresh_col malloc [w'|b base' col' off mi_b]; first by constructor. constructor. have neq_col: col' <> col. - by move=> eq_col; move/fresh_col: mi_b; rewrite eq_col Ord.leqxx. -by rewrite getm_set (introF eqP neq_col). + by move=> eq_col; move/fresh_col: mi_b; rewrite eq_col Ord.ltxx. +by rewrite setmE (introF eqP neq_col). Qed. @@ -666,12 +666,12 @@ move=> [fresh_col [in_bl rist]] malloc miP. constructor => b col' col'' base' base''. have [->|/eqP neq_col'] := altP (col' =P col); have [-> //|/eqP neq_col''] := altP (col'' =P col). -+ rewrite !getm_set eqxx (introF eqP neq_col'') => [[<- _]] /in_bl. ++ rewrite !setmE eqxx (introF eqP neq_col'') => [[<- _]] /in_bl. by rewrite (negbTE (Abstract.malloc_fresh malloc)). -+ rewrite !getm_set eqxx (introF eqP neq_col') => get_col' [eq_b _]. ++ rewrite !setmE eqxx (introF eqP neq_col') => get_col' [eq_b _]. move/in_bl: get_col'. by rewrite -eq_b (negbTE (Abstract.malloc_fresh malloc)). -+ rewrite !getm_set (introF eqP neq_col') (introF eqP neq_col''). ++ rewrite !setmE (introF eqP neq_col') (introF eqP neq_col''). exact: (miIr miP). Qed. @@ -689,8 +689,8 @@ move=> w1 w2 col' ty. rewrite (get_write_block _ H1) => //. have [/andP [? ?] [<- <- <-]|_ /rmem get_w1] := boolP (inbounds base sz w1). - rewrite getm_set eqxx (Abstract.malloc_get malloc); last first. - rewrite -2!val_ordE (lock subw) /= -lock valw_sub // /Ord.leq /= -ltnNge. + rewrite setmE eqxx (Abstract.malloc_get malloc); last first. + rewrite Ord.ltNge -2!val_ordE (lock subw) /= -lock valw_sub // /Ord.leq /= -ltnNge. by rewrite -(ltn_add2r base) subnK // addnC. apply: (refine_val_malloc _ fresh_col malloc). by constructor. @@ -699,19 +699,19 @@ have neq_col: col' <> col. move: get_w1; rewrite eq_col. move: (fresh_col col). case: (mi col) => // [[b' base']] /(_ b' base' erefl) lt_col. - by rewrite Ord.leqxx in lt_col. + by rewrite Ord.ltxx in lt_col. move: get_w1. set mi' := mi_malloc _ _ _ _. have mi'P := (meminj_spec_malloc base rist malloc miP). have eq_mi: mi' col' = mi col'. - by rewrite getm_set (introF eqP neq_col). + by rewrite setmE (introF eqP neq_col). rewrite eq_mi; move: eq_mi. case: (mi col') => // [[b' base']] mi'_col'. have neq_b': b' <> newb. move=> eq_b'; rewrite eq_b' in mi'_col'. have mi'_col: mi' col = Some (newb, base). - by rewrite getm_set eqxx. + by rewrite setmE eqxx. exact/neq_col/(miIr mi'P mi'_col' mi'_col). rewrite /Abstract.getv (Abstract.malloc_get_neq malloc neq_b'). case: (amem b') => // fr. @@ -743,15 +743,15 @@ split. (* freshness of color *) move=> col b base. have [-> _|neq_col] := col =P color. exact/Sym.ltb_inc. - rewrite getm_set (introF eqP neq_col). + rewrite setmE (introF eqP neq_col). move/fresh_color => lt_col. apply: (@Ord.lt_trans _ color col) => //=. exact/Sym.ltb_inc. split. (* list of block is complete *) move=> col b base. have [->|neq_col] := col =P color. - by rewrite getm_set eqxx => [[<- _]]; rewrite inE eqxx. - by rewrite getm_set (introF eqP neq_col) inE => /in_bl ->; rewrite orbT. + by rewrite setmE eqxx => [[<- _]]; rewrite inE eqxx. + by rewrite setmE (introF eqP neq_col) inE => /in_bl ->; rewrite orbT. split. (* no overlap *) move=> i j def w. rewrite /Sym.update_block_info. @@ -905,7 +905,7 @@ have [eq_sz|neq_sz] := sz =P Sym.block_size bi. (* Showing invariant for the new block *) apply: (@BlockInfoLive _ _ _ color newb) => //. * by rewrite /bounded_add /= eq_sz. - * by rewrite getm_set eqxx. + * by rewrite setmE eqxx. move=> off /= lt_off. rewrite (get_write_block _ write_bi). suff ->: inbounds (Sym.block_base bi) sz (Sym.block_base bi + off)%w. @@ -923,8 +923,8 @@ have [eq_sz|neq_sz] := sz =P Sym.block_size bi. move=> col b color_bi' [? ?] mi_col get_bi'. apply: (@BlockInfoLive _ _ _ col b) => //. have neq_col: col <> color. - by move=> eq_col; move/fresh_color: mi_col; rewrite eq_col Ord.leqxx. - by rewrite getm_set (introF eqP neq_col). + by move=> eq_col; move/fresh_color: mi_col; rewrite eq_col Ord.ltxx. + by rewrite setmE (introF eqP neq_col). move=> off lt_off. rewrite (get_write_block _ write_bi). have [bounds_bi|] := boolP (inbounds _ _ _). @@ -988,7 +988,7 @@ have [eq_i <-|neq_i] := i =P index bi info. * rewrite /= /bounded_add; split=> //. rewrite -(leq_add2l (Sym.block_base bi)) in le_sz. by rewrite (leq_ltn_trans le_sz). - * by rewrite getm_set eqxx. + * by rewrite setmE eqxx. move=> off /= lt_off. rewrite (get_write_block _ write_bi). suff ->: inbounds (Sym.block_base bi) sz (Sym.block_base bi + off)%w @@ -1002,8 +1002,8 @@ case=> //. move=> col b color_bi' [? ?] mi_col get_bi'. apply: (@BlockInfoLive _ _ _ col b) => //. have neq_col: col <> color. - by move=> eq_col; move/fresh_color: mi_col; rewrite eq_col Ord.leqxx. - by rewrite getm_set (introF eqP neq_col). + by move=> eq_col; move/fresh_color: mi_col; rewrite eq_col Ord.ltxx. + by rewrite setmE (introF eqP neq_col). move=> off lt_off. rewrite (get_write_block _ write_bi). have [/andP [lbbi ubbi]|] := boolP (inbounds _ _ _). @@ -1256,7 +1256,7 @@ by solve_pc rpci. pose mi' := mi_malloc mi newb (Sym.block_base bi) color. have rnewb: refine_val mi' (Abstract.VPtr (newb, 0)) (Sym.block_base bi) (PTR color). rewrite -[Sym.block_base bi]addw0; constructor. - by rewrite /mi' /mi_malloc getm_set eqxx. + by rewrite /mi' /mi_malloc setmE eqxx. move/(refine_registers_malloc (Sym.block_base bi) fresh_color malloc): rregs => rregs. eapply (refine_registers_upd rregs rnewb) in E2. @@ -1288,7 +1288,7 @@ by solve_pc rpci. case: biP E E0 E1 color_x in_x => [|->] //. move=> col b color_bi [? ?] mi_col get_x E E0 E1 color_x in_x. case/andP: E1 => lb_val ub_val. - rewrite (lock addw) /= -!val_ordE /= /Ord.leq /= -lock in ub_val. + rewrite Ord.ltNge (lock addw) /= -!val_ordE /= /Ord.leq /= -lock in ub_val. rewrite valw_add' // -ltnNge in ub_val. have /andP [E1 E2]: Sym.block_base x <= vala < Sym.block_base x + Sym.block_size x. diff --git a/memory_safety/symbolic.v b/memory_safety/symbolic.v index dfb910e..85cf6d2 100644 --- a/memory_safety/symbolic.v +++ b/memory_safety/symbolic.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.ssrint. -Require Import CoqUtils.hseq CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype ssrint. +From CoqUtils Require Import hseq ord word partmap. Require Import lib.utils common.types. Require Import symbolic.symbolic memory_safety.classes. diff --git a/sealing/abstract.v b/sealing/abstract.v index a2aab48..fe009a8 100644 --- a/sealing/abstract.v +++ b/sealing/abstract.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq. +From CoqUtils Require Import ord word partmap. Require Import lib.utils common.types common.segment sealing.classes. Import DoNotation. diff --git a/sealing/classes.v b/sealing/classes.v index 7f7db93..3ba5e73 100644 --- a/sealing/classes.v +++ b/sealing/classes.v @@ -1,4 +1,4 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Import common.types. Class sealing_syscall_addrs mt := { diff --git a/sealing/main.v b/sealing/main.v index 87f935d..2bcaca2 100644 --- a/sealing/main.v +++ b/sealing/main.v @@ -1,6 +1,6 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.ssrbool Ssreflect.seq Ssreflect.choice Ssreflect.fintype. -Require Import MathComp.ssrint. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap CoqUtils.hseq. +From mathcomp Require Import + ssreflect ssrfun eqtype ssrnat ssrbool seq choice fintype ssrint. +From CoqUtils Require Import ord word partmap hseq. Require Import lib.utils lib.word_utils common.types common.segment. Require Import concrete.concrete. Require Import concrete.int_32. diff --git a/sealing/refinementSA.v b/sealing/refinementSA.v index 9569fec..2c777da 100644 --- a/sealing/refinementSA.v +++ b/sealing/refinementSA.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq. +From CoqUtils Require Import ord word partmap. Require Import lib.utils. Require Import lib.ssr_list_utils lib.partmap_utils. Require Import common.types symbolic.symbolic. @@ -40,7 +40,7 @@ Lemma fresh_set_inj : forall (km : {partmap Abs.key -> Sym.key}) akey skey, key_map_inj (setm km akey skey). Proof. move => km akey skey kmi nk ak ak' sk sk' E1 E2 Esk. -rewrite -{}Esk {sk'} in E2; move: E1 E2; rewrite !getm_set. +rewrite -{}Esk {sk'} in E2; move: E1 E2; rewrite !setmE. have [-> {ak}|Hne] := altP (_ =P _). move=> [<-] {sk}. have [-> {ak'} //|Hne'] := altP (_ =P _). @@ -132,7 +132,7 @@ Lemma refine_key_set_km : forall km ak sk akey skey, refine_key km ak sk -> refine_key (setm km akey skey) ak sk. Proof. - unfold refine_key. intros. rewrite getm_set. + unfold refine_key. intros. rewrite setmE. by have [eq_ak | /eqP neq_ak] := altP (ak =P akey); congruence. Qed. @@ -349,7 +349,7 @@ Proof. assert(refine_val_atom (setm km (Abs.mkkey_f akeys) skey) (Abs.VKey mt (Abs.mkkey_f akeys)) (monew@(Sym.KEY skey))) as rva. - unfold refine_val_atom, refine_key. by rewrite getm_set eqxx. + unfold refine_val_atom, refine_key. by rewrite setmE eqxx. (* need to show freshness for new abstract key to be able to use refine...set lemmas to port refinements to the extended km *) @@ -373,23 +373,23 @@ Proof. have [eq_ak | /eqP neq_ak] := altP (ak =P (Abs.mkkey_f akeys)). + subst. apply False_ind. by rewrite inE eqxx in ninak. + simpl in ninak. - rewrite getm_set (introF eqP neq_ak). + rewrite setmE (introF eqP neq_ak). destruct rins as [rins1 _]. apply rins1. by case/norP: ninak. - (* symbolic keys *) move => ak sk /=. have [eq_ak | /eqP neq_ak] := altP (ak =P (Abs.mkkey_f akeys)) => hsk. - + subst. rewrite getm_set eqxx in hsk => //. + + subst. rewrite setmE eqxx in hsk => //. injection hsk => hsk'. clear hsk. rewrite hsk'. by rewrite Sym.ltb_inc -?hsk' ?lt_skey //. - + rewrite getm_set (introF eqP neq_ak) in hsk => //. + + rewrite setmE (introF eqP neq_ak) in hsk => //. destruct rins as [_ [rins2 _]]. eapply Ord.lt_trans. eapply rins2. eassumption. by rewrite /= Sym.ltb_inc ?lt_skey. - (* injectivity *) apply fresh_set_inj. by destruct rins as [_ [_ rins3]]. destruct rins as [_ [rins2 _]]. - intros ? Hc. apply rins2 in Hc. by rewrite Ord.leqxx in Hc. + intros ? Hc. apply rins2 in Hc. by rewrite Ord.ltxx in Hc. } + {(* seal *) (* break up the effects of the system call *) diff --git a/sealing/symbolic.v b/sealing/symbolic.v index 7efeda0..6efe17c 100644 --- a/sealing/symbolic.v +++ b/sealing/symbolic.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.ord CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import ord hseq word partmap. Require Import lib.utils common.types. Require Import symbolic.symbolic sealing.classes. diff --git a/symbolic/backward.v b/symbolic/backward.v index d2dcadb..f6570fe 100644 --- a/symbolic/backward.v +++ b/symbolic/backward.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq. -Require Import CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq. +From CoqUtils Require Import hseq word partmap. Require Import lib.utils. Require Import common.types. diff --git a/symbolic/exec.v b/symbolic/exec.v index 5422b09..5652c95 100644 --- a/symbolic/exec.v +++ b/symbolic/exec.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import hseq word partmap. Require Import lib.utils common.types symbolic.symbolic. Set Implicit Arguments. diff --git a/symbolic/fault_handler.v b/symbolic/fault_handler.v index ce41139..3dac4f1 100644 --- a/symbolic/fault_handler.v +++ b/symbolic/fault_handler.v @@ -1,8 +1,8 @@ (* Fault handler implementation for concrete realization of symbolic machine *) -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq Ssreflect.choice Ssreflect.fintype. -Require Import MathComp.tuple MathComp.ssrint. -Require Import CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import + ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype tuple ssrint. +From CoqUtils Require Import word fset partmap. Require Import lib.utils. Require Import common.types. @@ -250,13 +250,13 @@ Proof. intros. destruct KINV as (RVEC & PROG & MEM & GRULES1 & GRULES2 & REGS & INT). repeat split; eauto. - intros addr' IN. - move: UPD; rewrite /updm GET /= => - [<-]; rewrite getm_set. + move: UPD; rewrite /updm GET /= => - [<-]; rewrite setmE. move: IN; have [-> {addr'}|_] := altP (_ =P _) => IN; last by eauto. apply RVEC in IN. destruct IN as [w1' IN]. assert (EQ : Concrete.TKernel = ct) by congruence. subst ct. by rewrite decode_kernel_tag in DEC. - intros addr' i GET'. - move: UPD; rewrite /updm GET /= => - [<-] {mem2}; rewrite getm_set. + move: UPD; rewrite /updm GET /= => - [<-] {mem2}; rewrite setmE. have [Heq|Hne] := altP (_ =P _). + rewrite -{}Heq {addr} in GET. specialize (@PROG _ _ GET'). @@ -279,7 +279,7 @@ Proof. intros. destruct KINV as (RVEC & PROG & MEM & GRULES1 & GRULES2 & REGS & INT). do 6 (split; eauto). move=> r' IN; move: UPD; rewrite /updm GET /= => - [<-] {regs'}. - rewrite getm_set. + rewrite setmE. have [Heq|Hneq] := altP (_ =P _). - rewrite {}Heq {r'} in IN. move: IN => /REGS [x GET']. @@ -295,20 +295,20 @@ Proof. intros (RVEC & PROG & MEM & GRULES1 & GRULES2 & REGS & INT). do 7 (try split; eauto). - move=> addr IN. - rewrite /Concrete.store_mvec getm_union. + rewrite /Concrete.store_mvec unionmE. set m := mkpartmap _. - rewrite -[isSome (m addr)]/(addr \in m) mem_mkpartmap /=. + rewrite -mem_domm domm_mkpartmap /=. have [Hin | Hnin] := boolP (addr \in Concrete.mvec_fields mt); last by eauto. - have: addr \in m by rewrite mem_mkpartmap. - rewrite inE; case Heq: (m addr)=> [v|] //= _. + have: addr \in domm m by rewrite domm_mkpartmap. + rewrite mem_domm; case Heq: (m addr)=> [v|] //= _. suff: taga v = Concrete.TKernel. by case: v {Heq} => [w t] /= ->; eauto. - apply/eqP; move/getm_mkpartmap': Heq. + apply/eqP; move/mkpartmap_Some: Heq. rewrite -{2}[v]/((addr, v).2); move: (addr, v). by apply/allP => /=; rewrite !eqxx /=. -- move=> addr instr Hget; rewrite getm_union. +- move=> addr instr Hget; rewrite unionmE. set m := mkpartmap _; set addr' := (_ + _)%w. - rewrite -[isSome (m addr')]/(addr' \in m) mem_mkpartmap /=. + rewrite -mem_domm domm_mkpartmap /=. have: addr' \notin Concrete.mvec_and_rvec_fields mt by apply: MEM. by rewrite mem_cat=> /norP [/negbTE -> _]; eauto. - by eapply policy_invariant_store_mvec; eauto. diff --git a/symbolic/forward.v b/symbolic/forward.v index 8624d2c..a76146d 100644 --- a/symbolic/forward.v +++ b/symbolic/forward.v @@ -1,4 +1,4 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. Require Import lib.utils. Require Import common.types. @@ -9,7 +9,7 @@ Require Import symbolic.exec. Require Import symbolic.rules. Require Import symbolic.refinement_common. -Require Import CoqUtils.word CoqUtils.partmap. +From CoqUtils Require Import word partmap. Set Implicit Arguments. Unset Strict Implicit. diff --git a/symbolic/int_32.v b/symbolic/int_32.v index 1f55208..a6f5f7f 100644 --- a/symbolic/int_32.v +++ b/symbolic/int_32.v @@ -7,9 +7,9 @@ Require Import concrete.concrete. Require Import symbolic.rules. Require Import symbolic.fault_handler. Require Import symbolic.symbolic. -Require Import Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq MathComp.ssrint. +From mathcomp Require Import ssrnat eqtype seq ssrint. -Require Import CoqUtils.word CoqUtils.partmap. +From CoqUtils Require Import word partmap. Import DoNotation. Import Concrete. diff --git a/symbolic/refinement_common.v b/symbolic/refinement_common.v index 6ddcce7..0d58585 100644 --- a/symbolic/refinement_common.v +++ b/symbolic/refinement_common.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import hseq word partmap fset. Require Import lib.utils. Require Import common.types. @@ -76,12 +76,11 @@ Definition mvec_in_kernel (cmem : Concrete.memory mt) := Lemma store_mvec_mvec_in_kernel cmem mvec : mvec_in_kernel (Concrete.store_mvec cmem mvec). Proof. -move=> k; rewrite /Concrete.store_mvec getm_union. +move=> k; rewrite /Concrete.store_mvec unionmE. set m := mkpartmap _. -rewrite -[isSome (m k)]/(k \in m) mem_mkpartmap /in_mvec /Concrete.mvec_fields. -move=> E; rewrite E; have: k \in m by rewrite mem_mkpartmap. -rewrite inE {E}; case E: (m k) => [v|] // _. -move/getm_mkpartmap': E; rewrite !inE. +rewrite -mem_domm domm_mkpartmap /in_mvec /Concrete.mvec_fields. +move=> E; rewrite E; have: k \in domm m by rewrite domm_mkpartmap. +case/dommP => v E'; rewrite E'; move/mkpartmap_Some: E'; rewrite !inE. do !(case/orP=> [/eqP [_ ->]|]; eauto). by move/eqP => [_ ->]; eauto. Qed. @@ -262,11 +261,11 @@ Proof. - split. + move=> w x ct'' st'' Hdec_ct' Hget''. rewrite Hdec_eq in Hdec_ct'. - move: Hget''; rewrite !getm_set. + move: Hget''; rewrite !setmE. have [Heq|Hneq] := w =P addr. * subst w; move=> [? ?]; subst; congruence. * by eapply (proj1 Hmem); eauto. - + move=> w x st Hget''; move: Hget'' Hdec_eq; rewrite /updm !getm_set. + + move=> w x st Hget''; move: Hget'' Hdec_eq; rewrite /updm !setmE. have [_ {w}|Hneq] := altP (w =P addr). move => [-> Ht]; eexists ct'=> //. by rewrite Hdec_eq Hdec' Ht. @@ -287,7 +286,7 @@ Proof. move=> Hwf Hget Hdec Hupd Hdec' addr' t''; rewrite Hwf. have := decode_monotonic _ _ Hget Hdec Hdec'. move: Hupd; rewrite /updm Hget /= => - [<-] {cmem'} Hmono. -rewrite getm_set. +rewrite setmE. have [-> {addr'}|_] := altP (addr' =P addr). by rewrite Hget !Hmono Hdec Hdec' !andbF. case: (cmem addr') => [[i ti]|] //. @@ -310,7 +309,7 @@ Proof. have CONTRA : Concrete.TKernel = ct by congruence. subst ct. by rewrite decode_kernel_tag in DEC. } move: UPD; rewrite /updm GET /= => - [<-]. - by rewrite getm_set (introF eqP NEQ) KER; eauto. + by rewrite setmE (introF eqP NEQ) KER; eauto. Qed. Lemma mvec_in_kernel_kernel_upd cmem cmem' addr w : @@ -320,7 +319,7 @@ Lemma mvec_in_kernel_kernel_upd cmem cmem' addr w : Proof. intros MVEC UPD addr' IN. move: UPD; rewrite /updm; case: (cmem _) => //= _ [<-]. -rewrite getm_set. +rewrite setmE. by have [?|/eqP NEQ] := altP (addr' =P addr); simpl in *; subst; eauto. Qed. @@ -359,13 +358,13 @@ Proof. by eauto. - move: Hupd; rewrite /updm Hget=> - [<-] {amem'}; split. + move=> w x'' ct'' st''. - rewrite Hdec_eq !getm_set. + rewrite Hdec_eq !setmE. have [_ {w}|_] := altP (w =P addr). move=> Hdec_ct'' [Hv Hct]. move: Hv Hct Hdec_ct'' => <- <- {x'' ct''}. by rewrite Hdec; move => [->]. by apply (proj1 Hmem). + move=> w x' st'. - rewrite !getm_set. + rewrite !setmE. case: (w == addr) => [{w} [<- <-] {x' st'}|]. exists ct=> //. by rewrite Hdec_eq. @@ -391,13 +390,13 @@ Proof. move: Hupd; rewrite {1}/updm Hget /= => - [<-]. rewrite Hupd'; eexists => //; split. - move=> r' x ct'' st''. - rewrite !getm_set. + rewrite !setmE. case: (r' == r) => [Hdec'' [Hx Hct'']|]. move: Hx Hct'' Hdec'' => <- <-. by rewrite Hdec'=> [[->]]. by apply (proj1 Hregs). - move=> r' x st''. - rewrite !getm_set. + rewrite !setmE. case: (r' == r) => [[<- <-] {x st''}|]; first by eauto. by apply (proj2 Hregs). Qed. @@ -414,12 +413,12 @@ Proof. have [ct0 Hdec' Hget'] := proj2 Hregs _ _ _ Hget. rewrite Hget' /=. eexists=> //; split. - - move=> r' x ct' st'; rewrite !getm_set. + - move=> r' x ct' st'; rewrite !setmE. case: (r' == r) => [Hdec_ct' [Hx Hct']|]. move: Hx Hct' Hdec_ct' => <- <- {x ct'}. by rewrite Hdec => [[<-]]. by apply (proj1 Hregs). - - move=> r' x st'; rewrite !getm_set. + - move=> r' x st'; rewrite !setmE. case: (r' == r) => [[<- <-] {x st'}|]; first by rewrite -Hdec; eauto. by apply (proj2 Hregs). Qed. diff --git a/symbolic/rules.v b/symbolic/rules.v index 191c4df..52ecd55 100644 --- a/symbolic/rules.v +++ b/symbolic/rules.v @@ -1,8 +1,8 @@ (* Definition of symbolic rules and tags used for kernel protection, along with conversion functions towards concrete integer tags. *) -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import hseq word partmap. Require Import lib.utils. Require Import common.types concrete.concrete symbolic.symbolic. diff --git a/symbolic/symbolic.v b/symbolic/symbolic.v index 09e712a..378500d 100644 --- a/symbolic/symbolic.v +++ b/symbolic/symbolic.v @@ -1,5 +1,5 @@ -Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq. -Require Import CoqUtils.hseq CoqUtils.word CoqUtils.partmap. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. +From CoqUtils Require Import hseq word partmap. Require Import lib.utils common.types. Require Import lib.ssr_list_utils.