1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Title: Adaptation of example from HOL/Hoare/Separation 8 Author: Rafal Kolanski, 2012 9 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> 10 Rafal Kolanski <rafal.kolanski at nicta.com.au> 11*) 12 13chapter "Separation Algebra for Virtual Memory" 14 15theory VM_Example 16imports 17 Sep_Tactics 18 Map_Extra 19begin 20 21text \<open> 22 Example instantiation of the abstract separation algebra to the sliced-memory 23 model used for building a separation logic in ``Verification of Programs in 24 Virtual Memory Using Separation Logic'' (PhD Thesis) by Rafal Kolanski. 25 26 We wrap up the concept of physical and virtual pointers as well as value 27 (usually a byte), and the page table root, into a datatype for instantiation. 28 This avoids having to produce a hierarchy of type classes. 29 30 The result is more general than the original. It does not mention the types 31 of pointers or virtual memory addresses. Instead of supporting only 32 singleton page table roots, we now support sets so we can identify a single 33 0 for the monoid. 34 This models multiple page tables in memory, whereas the original logic was 35 only capable of one at a time. 36\<close> 37 38datatype ('p,'v,'value,'r) vm_sep_state 39 = VMSepState "((('p \<times> 'v) \<rightharpoonup> 'value) \<times> 'r set)" 40 41instantiation vm_sep_state :: (type, type, type, type) sep_algebra 42begin 43 44fun 45 vm_heap :: "('a,'b,'c,'d) vm_sep_state \<Rightarrow> (('a \<times> 'b) \<rightharpoonup> 'c)" where 46 "vm_heap (VMSepState (h,r)) = h" 47 48fun 49 vm_root :: "('a,'b,'c,'d) vm_sep_state \<Rightarrow> 'd set" where 50 "vm_root (VMSepState (h,r)) = r" 51 52definition 53 sep_disj_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state 54 \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state \<Rightarrow> bool" where 55 "sep_disj_vm_sep_state x y = vm_heap x \<bottom> vm_heap y" 56 57definition 58 zero_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state" where 59 "zero_vm_sep_state \<equiv> VMSepState (Map.empty, {})" 60 61fun 62 plus_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state 63 \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state 64 \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state" where 65 "plus_vm_sep_state (VMSepState (x,r)) (VMSepState (y,r')) 66 = VMSepState (x ++ y, r \<union> r')" 67 68instance 69 apply intro_classes 70 apply (simp add: zero_vm_sep_state_def sep_disj_vm_sep_state_def) 71 apply (fastforce simp: sep_disj_vm_sep_state_def map_disj_def) 72 apply (case_tac x, clarsimp simp: zero_vm_sep_state_def) 73 apply (case_tac x, case_tac y) 74 apply (fastforce simp: sep_disj_vm_sep_state_def map_add_ac) 75 apply (case_tac x, case_tac y, case_tac z) 76 apply (fastforce simp: sep_disj_vm_sep_state_def) 77 apply (case_tac x, case_tac y, case_tac z) 78 apply (fastforce simp: sep_disj_vm_sep_state_def map_add_disj) 79 apply (case_tac x, case_tac y, case_tac z) 80 apply (fastforce simp: sep_disj_vm_sep_state_def map_add_disj map_disj_com) 81 done 82 83end 84 85end 86