Something went wrong. Try again.
Verified branch relaxing assembler in Isabelle/HOL with provably minimal bytecode layouts
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485theory Machine imports Encodingbegin
fun machine_advance :: "operation \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) option" where "machine_advance Idle pc a = Some (Suc pc, a)"| "machine_advance Raise pc a = Some (Suc pc, Suc a)"| "machine_advance Lower pc a = Some (Suc pc, a - 1)"| "machine_advance Finish pc a = None"| "machine_advance (Branch c wide d) pc a = (let next = pc + (if wide then 3 else 2) in if c \<and> a \<noteq> 0 then Some (next, a) else if 0 \<le> int next + d then Some (nat (int next + d), a) else None)"
definition machine_step :: "nat list \<Rightarrow> nat \<times> nat \<Rightarrow> (nat \<times> nat) option" where "machine_step code s = (case map_option fst (decode (drop (fst s) code)) of None \<Rightarrow> None | Some op \<Rightarrow> machine_advance op (fst s) (snd s))"
definition relocate :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" where "relocate p W s = (address p W (fst s), snd s)"
lemma lower_advance: assumes "i < length p" shows "machine_advance (lower p W i (p ! i)) (address p W i) a = map_option (relocate p W) (advance (p ! i) i a)" using assms unfolding relocate_def by (cases "p ! i") (auto simp: displacement_def destination_def width_def branches_def Let_def of_nat_add)
lemma source_closed: "wellformed p \<Longrightarrow> i \<le> length p \<Longrightarrow> source_step p (i,a) = Some (j,b) \<Longrightarrow> j \<le> length p" unfolding wellformed_def source_step_def branches_def destination_def by (cases "p ! i") (auto split: if_splits)
theorem step_correspondence: assumes "valid p W" "i \<le> length p" shows "machine_step (bytecode p W) (relocate p W (i,a)) = map_option (relocate p W) (source_step p (i,a))"proof (cases "i < length p") case True show ?thesis using fetch_instruction[OF assms(1) True] lower_advance[OF True, of W a] True by (auto simp: machine_step_def source_step_def relocate_def split: option.splits prod.splits)next case False with assms have "i = length p" by simp then show ?thesis by (simp add: machine_step_def source_step_def relocate_def bytecode_length[symmetric])qed
theorem execution_correspondence: assumes "wellformed p" "valid p W" "i \<le> length p" shows "execute (machine_step (bytecode p W)) fuel (relocate p W (i,a)) = relocate p W (execute (source_step p) fuel (i,a))" using assms(3)proof (induction fuel arbitrary: i a) case 0 then show ?case by simpnext case (Suc fuel) show ?case using Suc.IH source_closed[OF assms(1) Suc.prems] step_correspondence[OF assms(2) Suc.prems, of a] by (cases "source_step p (i,a)") (auto split: prod.splits)qed
definition assemble :: "nat instruction list \<Rightarrow> nat list option" where "assemble p = (if wellformed p \<and> valid p (layout p) then Some (bytecode p (layout p)) else None)"
theorem assembly_complete: "assemble p \<noteq> None \<longleftrightarrow> wellformed p \<and> (\<exists>W. valid p W)" by (simp add: assemble_def layout_complete)
theorem assembly_minimum: "assemble p = Some code \<Longrightarrow> valid p V \<Longrightarrow> length code \<le> address p V (length p)" using layout_minimum[of p V] by (auto simp: assemble_def bytecode_length split: if_splits)
theorem assembly_execution: assumes "assemble p = Some code" shows "execute (machine_step code) fuel (0,a) = relocate p (layout p) (execute (source_step p) fuel (0,a))" using assms execution_correspondence[of p "layout p" 0 fuel a] by (auto simp: assemble_def relocate_def split: if_splits)
end