| 1 | theory Bounds |
| 2 | imports Branches |
| 3 | begin |
| 4 | |
| 5 | fun guarded_run :: "nat \<Rightarrow> opcode list \<Rightarrow> machine \<Rightarrow> bool" where |
| 6 | "guarded_run limit [] s = (length (stack s) \<le> limit)" |
| 7 | | "guarded_run limit (op # code) s = (length (stack s) \<le> limit \<and> |
| 8 | (case transition op s of None \<Rightarrow> False | Some q \<Rightarrow> guarded_run limit code q))" |
| 9 | |
| 10 | fun guarded_flow :: "nat \<Rightarrow> flow \<Rightarrow> machine \<Rightarrow> bool" where |
| 11 | "guarded_flow limit (Basic code) s = guarded_run limit code s" |
| 12 | | "guarded_flow limit (Sequence a b) s = (guarded_flow limit a s \<and> |
| 13 | (case flowrun a s of None \<Rightarrow> False | Some q \<Rightarrow> guarded_flow limit b q))" |
| 14 | | "guarded_flow limit (Choice a b) s = guarded_flow limit (if registers s Rax = 0 then b else a) s" |
| 15 | |
| 16 | lemma effect_shift: |
| 17 | "effect op n = Some m \<Longrightarrow> effect op (n + base) = Some (m + base)" |
| 18 | by (cases op; cases n; auto split: if_splits; arith) |
| 19 | |
| 20 | lemma effect_frame: |
| 21 | "effect op n = Some m \<Longrightarrow> transition op s = Some q \<Longrightarrow> |
| 22 | drop m (stack q) = drop n (stack s)" |
| 23 | by (cases op; cases n; cases "stack s") (auto simp: effect.simps transition.simps split: if_splits) |
| 24 | |
| 25 | lemma audit_limit: |
| 26 | "n \<le> 512 \<Longrightarrow> audit code n = Some m \<Longrightarrow> m \<le> 512" |
| 27 | by (induction code arbitrary: n) (auto split: if_splits bind_splits) |
| 28 | |
| 29 | lemma flowaudit_limit: |
| 30 | "n \<le> 512 \<Longrightarrow> flowaudit code n = Some m \<Longrightarrow> m \<le> 512" |
| 31 | proof (induction code arbitrary: n m) |
| 32 | case (Basic code) |
| 33 | then show ?case by (auto dest: audit_limit) |
| 34 | next |
| 35 | case (Sequence a b) |
| 36 | obtain k where a: "flowaudit a n = Some k" and b: "flowaudit b k = Some m" |
| 37 | using Sequence.prems(2) by (auto split: bind_splits) |
| 38 | have "k \<le> 512" using Sequence.IH(1)[OF Sequence.prems(1) a] . |
| 39 | then show ?case using Sequence.IH(2)[OF _ b] by blast |
| 40 | next |
| 41 | case (Choice a b) |
| 42 | have "flowaudit a n = Some m" |
| 43 | using Choice.prems(2) by (auto split: option.splits if_splits) |
| 44 | then show ?case using Choice.IH(1)[OF Choice.prems(1)] by blast |
| 45 | qed |
| 46 | |
| 47 | theorem audit_window: |
| 48 | assumes "length (stack s) = base + n" "n \<le> 512" "audit code n = Some m" |
| 49 | shows "\<exists>q. run code s = Some q \<and> length (stack q) = base + m \<and> |
| 50 | drop m (stack q) = drop n (stack s) \<and> guarded_run (base + 512) code s" |
| 51 | using assms |
| 52 | proof (induction code arbitrary: s n m) |
| 53 | case Nil |
| 54 | then show ?case by auto |
| 55 | next |
| 56 | case (Cons op code) |
| 57 | obtain k where effect: "effect op n = Some k" and bound: "k \<le> 512" |
| 58 | and tail: "audit code k = Some m" |
| 59 | using Cons.prems(3) by (auto split: if_splits bind_splits) |
| 60 | have shifted: "effect op (length (stack s)) = Some (base + k)" |
| 61 | using effect_shift[OF effect, of base] Cons.prems(1) by (simp add: add.commute) |
| 62 | obtain p where p: "transition op s = Some p" "length (stack p) = base + k" |
| 63 | using effect_sound[OF shifted] by blast |
| 64 | obtain q where q: "run code p = Some q" "length (stack q) = base + m" |
| 65 | "drop m (stack q) = drop k (stack p)" "guarded_run (base + 512) code p" |
| 66 | using Cons.IH[OF p(2) bound tail] by blast |
| 67 | have frame: "drop k (stack p) = drop n (stack s)" |
| 68 | using effect_frame[OF effect p(1)] . |
| 69 | have "length (stack s) \<le> base + 512" using Cons.prems(1,2) by arith |
| 70 | then show ?case using p q frame by auto |
| 71 | qed |
| 72 | |
| 73 | theorem flow_window: |
| 74 | assumes "length (stack s) = base + n" "n \<le> 512" "flowaudit code n = Some m" |
| 75 | shows "\<exists>q. flowrun code s = Some q \<and> length (stack q) = base + m \<and> |
| 76 | drop m (stack q) = drop n (stack s) \<and> inputs q = inputs s \<and> |
| 77 | guarded_flow (base + 512) code s" |
| 78 | using assms |
| 79 | proof (induction code arbitrary: s n m) |
| 80 | case (Basic code) |
| 81 | have audit: "audit code n = Some m" using Basic.prems by simp |
| 82 | obtain q where q: "run code s = Some q" "length (stack q) = base + m" |
| 83 | "drop m (stack q) = drop n (stack s)" "guarded_run (base + 512) code s" |
| 84 | using audit_window[OF Basic.prems(1,2) audit] by blast |
| 85 | show ?case using q audit_inputs[OF audit q(1)] by auto |
| 86 | next |
| 87 | case (Sequence a b) |
| 88 | obtain k where a: "flowaudit a n = Some k" and b: "flowaudit b k = Some m" |
| 89 | using Sequence.prems(3) by (auto split: bind_splits) |
| 90 | obtain p where p: "flowrun a s = Some p" "length (stack p) = base + k" |
| 91 | "drop k (stack p) = drop n (stack s)" "inputs p = inputs s" |
| 92 | "guarded_flow (base + 512) a s" |
| 93 | using Sequence.IH(1)[OF Sequence.prems(1,2) a] by blast |
| 94 | have bound: "k \<le> 512" using flowaudit_limit[OF Sequence.prems(2) a] . |
| 95 | obtain q where q: "flowrun b p = Some q" "length (stack q) = base + m" |
| 96 | "drop m (stack q) = drop k (stack p)" "inputs q = inputs p" |
| 97 | "guarded_flow (base + 512) b p" |
| 98 | using Sequence.IH(2)[OF p(2) bound b] by blast |
| 99 | show ?case using p q by auto |
| 100 | next |
| 101 | case (Choice a b) |
| 102 | have a: "flowaudit a n = Some m" and b: "flowaudit b n = Some m" |
| 103 | using Choice.prems(3) by (auto split: option.splits if_splits) |
| 104 | show ?case |
| 105 | using Choice.IH(1)[OF Choice.prems(1,2) a] Choice.IH(2)[OF Choice.prems(1,2) b] |
| 106 | by (cases "registers s Rax = 0") auto |
| 107 | qed |
| 108 | |
| 109 | corollary checked_frame: |
| 110 | "flowaudit code 0 = Some 0 \<Longrightarrow> \<exists>q. flowrun code s = Some q \<and> |
| 111 | stack q = stack s \<and> inputs q = inputs s \<and> |
| 112 | guarded_flow (length (stack s) + 512) code s" |
| 113 | using flow_window[where s=s and base="length (stack s)" and n=0 and m=0 and code=code] |
| 114 | by auto |
| 115 | |
| 116 | end |