67 lines
2.3 KiB
Plaintext
67 lines
2.3 KiB
Plaintext
theory Checker
|
|
imports Encoding
|
|
begin
|
|
|
|
fun effect :: "opcode \<Rightarrow> nat \<Rightarrow> nat option" where
|
|
"effect (Push r) n = Some (Suc n)"
|
|
| "effect (Pop r) n = (if n = 0 then None else Some (n - 1))"
|
|
| "effect (Peek i) n = (if i < n then Some n else None)"
|
|
| "effect _ n = Some n"
|
|
|
|
fun audit :: "opcode list \<Rightarrow> nat \<Rightarrow> nat option" where
|
|
"audit [] n = Some n"
|
|
| "audit (op # code) n = (if writes op \<subseteq> {Rax,Rcx,Rbx} then
|
|
Option.bind (effect op n) (\<lambda>m. if m \<le> 512 then audit code m else None) else None)"
|
|
|
|
lemma effect_sound:
|
|
"effect op (length (stack s)) = Some n \<Longrightarrow>
|
|
\<exists>t. transition op s = Some t \<and> length (stack t) = n"
|
|
by (cases op; cases "stack s") (auto split: if_splits)
|
|
|
|
theorem audit_sound:
|
|
"audit code (length (stack s)) = Some n \<Longrightarrow>
|
|
\<exists>t. run code s = Some t \<and> length (stack t) = n"
|
|
proof (induction code arbitrary: s)
|
|
case Nil
|
|
then show ?case by simp
|
|
next
|
|
case (Cons op code)
|
|
then show ?case
|
|
by (auto dest!: effect_sound split: if_splits bind_splits; fastforce)
|
|
qed
|
|
|
|
lemma audit_scratch:
|
|
"audit code n = Some m \<Longrightarrow> list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code"
|
|
by (induction code arbitrary: n) (auto split: if_splits bind_splits)
|
|
|
|
theorem audit_inputs:
|
|
"audit code n = Some m \<Longrightarrow> run code s = Some t \<Longrightarrow> inputs t = inputs s"
|
|
proof -
|
|
assume audited: "audit code n = Some m" and ran: "run code s = Some t"
|
|
have scratch: "list_all (\<lambda>op. writes op \<subseteq> {Rax,Rcx,Rbx}) code"
|
|
using audit_scratch[OF audited] .
|
|
show ?thesis
|
|
proof (rule ext)
|
|
fix i
|
|
have keep: "list_all (\<lambda>op. input_register i \<notin> writes op) code"
|
|
unfolding list_all_iff
|
|
proof (rule ballI)
|
|
fix op
|
|
assume member: "op \<in> set code"
|
|
have bound: "writes op \<subseteq> {Rax,Rcx,Rbx}"
|
|
using scratch member by (auto simp: list_all_iff)
|
|
show "input_register i \<notin> writes op"
|
|
proof
|
|
assume written: "input_register i \<in> writes op"
|
|
have "input_register i \<in> {Rax,Rcx,Rbx}"
|
|
using subsetD[OF bound written] .
|
|
then show False by simp
|
|
qed
|
|
qed
|
|
show "inputs t i = inputs s i"
|
|
unfolding inputs_def using run_preserves[OF ran keep] .
|
|
qed
|
|
qed
|
|
|
|
end
|