| @@ -0,0 +1,131 @@ |
| 1 | +theory Execution |
| 2 | + imports Isolation |
| 3 | +begin |
| 4 | + |
| 5 | +datatype action = Read nat nat | Write nat nat nat |
| 6 | + |
| 7 | +fun valid :: "nat \<Rightarrow> nat \<Rightarrow> action \<Rightarrow> bool" where |
| 8 | + "valid slots bytes (Read k offset) = (k < slots \<and> offset < bytes)" |
| 9 | +| "valid slots bytes (Write k offset byte) = (k < slots \<and> offset < bytes \<and> byte < 256)" |
| 10 | + |
| 11 | +fun advance :: "pager \<Rightarrow> action \<Rightarrow> pager" where |
| 12 | + "advance s (Read k offset) = s" |
| 13 | +| "advance s (Write k offset byte) = store s k offset byte" |
| 14 | + |
| 15 | +fun reference :: "memory \<Rightarrow> action \<Rightarrow> memory" where |
| 16 | + "reference m (Read k offset) = m" |
| 17 | +| "reference m (Write k offset byte) = reference_write m k offset byte" |
| 18 | + |
| 19 | +fun observe :: "pager \<Rightarrow> action \<Rightarrow> nat" where |
| 20 | + "observe s (Read k offset) = view s k offset" |
| 21 | +| "observe s (Write k offset byte) = byte" |
| 22 | + |
| 23 | +fun reference_observe :: "memory \<Rightarrow> action \<Rightarrow> nat" where |
| 24 | + "reference_observe m (Read k offset) = m k offset" |
| 25 | +| "reference_observe m (Write k offset byte) = byte" |
| 26 | + |
| 27 | +fun execute :: "pager \<Rightarrow> action list \<Rightarrow> pager" where |
| 28 | + "execute s [] = s" |
| 29 | +| "execute s (a # actions) = execute (advance s a) actions" |
| 30 | + |
| 31 | +fun reference_execute :: "memory \<Rightarrow> action list \<Rightarrow> memory" where |
| 32 | + "reference_execute m [] = m" |
| 33 | +| "reference_execute m (a # actions) = reference_execute (reference m a) actions" |
| 34 | + |
| 35 | +fun observations :: "pager \<Rightarrow> action list \<Rightarrow> nat list" where |
| 36 | + "observations s [] = []" |
| 37 | +| "observations s (a # actions) = observe s a # observations (advance s a) actions" |
| 38 | + |
| 39 | +fun reference_observations :: "memory \<Rightarrow> action list \<Rightarrow> nat list" where |
| 40 | + "reference_observations m [] = []" |
| 41 | +| "reference_observations m (a # actions) = |
| 42 | + reference_observe m a # reference_observations (reference m a) actions" |
| 43 | + |
| 44 | +lemma advance_invariant: |
| 45 | + "invariant n s \<Longrightarrow> invariant n (advance s a)" |
| 46 | + by (cases a; simp add: write_invariant) |
| 47 | + |
| 48 | +lemma advance_simulation: |
| 49 | + "invariant n s \<Longrightarrow> represents n s m \<Longrightarrow> valid n bytes a \<Longrightarrow> |
| 50 | + represents n (advance s a) (reference m a)" |
| 51 | + by (cases a; auto intro: simulation) |
| 52 | + |
| 53 | +lemma observe_simulation: |
| 54 | + "represents n s m \<Longrightarrow> valid n bytes a \<Longrightarrow> |
| 55 | + observe s a = reference_observe m a" |
| 56 | + by (cases a; auto simp: represents_def) |
| 57 | + |
| 58 | +theorem execute_invariant: |
| 59 | + "invariant n s \<Longrightarrow> invariant n (execute s actions)" |
| 60 | + by (induction actions arbitrary: s) (auto intro: advance_invariant) |
| 61 | + |
| 62 | +theorem execute_refinement: |
| 63 | + assumes "invariant n s" "represents n s m" "list_all (valid n bytes) actions" |
| 64 | + shows "represents n (execute s actions) (reference_execute m actions)" |
| 65 | + using assms |
| 66 | + by (induction actions arbitrary: s m) |
| 67 | + (auto intro: advance_invariant advance_simulation) |
| 68 | + |
| 69 | +theorem observable_equivalence: |
| 70 | + assumes "invariant n s" "represents n s m" "list_all (valid n bytes) actions" |
| 71 | + shows "observations s actions = reference_observations m actions" |
| 72 | + using assms |
| 73 | + by (induction actions arbitrary: s m) |
| 74 | + (auto intro: advance_invariant advance_simulation observe_simulation) |
| 75 | + |
| 76 | +definition admitted :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> action \<Rightarrow> bool" where |
| 77 | + "admitted slots bytes capacity s a \<longleftrightarrow> valid slots bytes a \<and> |
| 78 | + (case a of Read k offset \<Rightarrow> True |
| 79 | + | Write k offset byte \<Rightarrow> writable s k \<or> frontier s < capacity)" |
| 80 | + |
| 81 | +definition checked :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> pager \<Rightarrow> action \<Rightarrow> pager option" where |
| 82 | + "checked slots bytes capacity s a = |
| 83 | + (if admitted slots bytes capacity s a then Some (advance s a) else None)" |
| 84 | + |
| 85 | +lemma checked_failure: |
| 86 | + "\<not> admitted slots bytes capacity s a \<Longrightarrow> checked slots bytes capacity s a = None" |
| 87 | + by (simp add: checked_def) |
| 88 | + |
| 89 | +lemma checked_success: |
| 90 | + "checked slots bytes capacity s a = Some t \<Longrightarrow> t = advance s a" |
| 91 | + by (auto simp: checked_def split: if_splits) |
| 92 | + |
| 93 | +theorem checked_invariant: |
| 94 | + "invariant slots s \<Longrightarrow> checked slots bytes capacity s a = Some t \<Longrightarrow> |
| 95 | + invariant slots t" |
| 96 | + using checked_success advance_invariant by blast |
| 97 | + |
| 98 | +theorem checked_capacity: |
| 99 | + "frontier s \<le> capacity \<Longrightarrow> checked slots bytes capacity s a = Some t \<Longrightarrow> |
| 100 | + frontier t \<le> capacity" |
| 101 | + by (cases a; auto simp: checked_def admitted_def prepare_frontier split: if_splits) |
| 102 | + |
| 103 | +theorem checked_simulation: |
| 104 | + "invariant slots s \<Longrightarrow> represents slots s m \<Longrightarrow> |
| 105 | + checked slots bytes capacity s a = Some t \<Longrightarrow> |
| 106 | + represents slots t (reference m a)" |
| 107 | + by (auto simp: checked_def admitted_def split: if_splits intro: advance_simulation) |
| 108 | + |
| 109 | +lemma invalid_slot_rejected: |
| 110 | + "slots \<le> k \<Longrightarrow> checked slots bytes capacity s (Write k offset byte) = None" |
| 111 | + by (simp add: checked_def admitted_def) |
| 112 | + |
| 113 | +lemma invalid_offset_rejected: |
| 114 | + "bytes \<le> offset \<Longrightarrow> checked slots bytes capacity s (Write k offset byte) = None" |
| 115 | + by (simp add: checked_def admitted_def) |
| 116 | + |
| 117 | +lemma invalid_byte_rejected: |
| 118 | + "256 \<le> byte \<Longrightarrow> checked slots bytes capacity s (Write k offset byte) = None" |
| 119 | + by (simp add: checked_def admitted_def) |
| 120 | + |
| 121 | +lemma exhausted_readonly_rejected: |
| 122 | + "\<not> writable s k \<Longrightarrow> capacity \<le> frontier s \<Longrightarrow> |
| 123 | + checked slots bytes capacity s (Write k offset byte) = None" |
| 124 | + by (simp add: checked_def admitted_def) |
| 125 | + |
| 126 | +lemma exhausted_writable_allowed: |
| 127 | + "writable s k \<Longrightarrow> valid slots bytes (Write k offset byte) \<Longrightarrow> |
| 128 | + checked slots bytes capacity s (Write k offset byte) = Some (store s k offset byte)" |
| 129 | + by (simp add: checked_def admitted_def) |
| 130 | + |
| 131 | +end |