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