| 1 | theory Checker |
| 2 | imports Encoding |
| 3 | begin |
| 4 | |
| 5 | fun effect :: "opcode \<Rightarrow> nat \<Rightarrow> nat option" where |
| 6 | "effect (Push r) n = Some (Suc n)" |
| 7 | | "effect (Pop r) n = (if n = 0 then None else Some (n - 1))" |
| 8 | | "effect (Peek i) n = (if i < n then Some n else None)" |
| 9 | | "effect _ n = Some n" |
| 10 | |
| 11 | fun audit :: "opcode list \<Rightarrow> nat \<Rightarrow> nat option" where |
| 12 | "audit [] n = Some n" |
| 13 | | "audit (op # code) n = (if writes op \<subseteq> {Rax,Rcx,Rbx} then |
| 14 | Option.bind (effect op n) (\<lambda>m. if m \<le> 512 then audit code m else None) else None)" |
| 15 | |
| 16 | lemma effect_sound: |
| 17 | "effect op (length (stack s)) = Some n \<Longrightarrow> |
| 18 | \<exists>t. transition op s = Some t \<and> length (stack t) = n" |
| 19 | by (cases op; cases "stack s") (auto split: if_splits) |
| 20 | |
| 21 | theorem audit_sound: |
| 22 | "audit code (length (stack s)) = Some n \<Longrightarrow> |
| 23 | \<exists>t. run code s = Some t \<and> length (stack t) = n" |
| 24 | proof (induction code arbitrary: s) |
| 25 | case Nil |
| 26 | then show ?case by simp |
| 27 | next |
| 28 | case (Cons op code) |
| 29 | then show ?case |
| 30 | by (auto dest!: effect_sound split: if_splits bind_splits; fastforce) |
| 31 | qed |
| 32 | |
| 33 | lemma audit_scratch: |
| 34 | "audit code n = Some m \<Longrightarrow> list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code" |
| 35 | by (induction code arbitrary: n) (auto split: if_splits bind_splits) |
| 36 | |
| 37 | theorem audit_inputs: |
| 38 | "audit code n = Some m \<Longrightarrow> run code s = Some t \<Longrightarrow> inputs t = inputs s" |
| 39 | proof - |
| 40 | assume audited: "audit code n = Some m" and ran: "run code s = Some t" |
| 41 | have scratch: "list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code" |
| 42 | using audit_scratch[OF audited] . |
| 43 | show ?thesis |
| 44 | proof (rule ext) |
| 45 | fix i |
| 46 | have keep: "list_all (\<lambda>op. input_register i \<notin> writes op) code" |
| 47 | unfolding list_all_iff |
| 48 | proof (rule ballI) |
| 49 | fix op |
| 50 | assume member: "op \<in> set code" |
| 51 | have bound: "writes op \<subseteq> {Rax,Rcx,Rbx}" |
| 52 | using scratch member by (auto simp: list_all_iff) |
| 53 | show "input_register i \<notin> writes op" |
| 54 | proof |
| 55 | assume written: "input_register i \<in> writes op" |
| 56 | have "input_register i \<in> {Rax,Rcx,Rbx}" |
| 57 | using subsetD[OF bound written] . |
| 58 | then show False by simp |
| 59 | qed |
| 60 | qed |
| 61 | show "inputs t i = inputs s i" |
| 62 | unfolding inputs_def using run_preserves[OF ran keep] . |
| 63 | qed |
| 64 | qed |
| 65 | |
| 66 | end |