1 (* Title: Adaptation of example from HOL/Hoare/Separation

     2    Author: Rafal Kolanski, 2012

     3    Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>

     4                 Rafal Kolanski <rafal.kolanski at nicta.com.au>

     5 *)

     6 

     7 header "Separation Algebra for Virtual Memory"

     8 

     9 theory VM_Example

    10 imports "../Sep_Tactics" "../Map_Extra"

    11 begin

    12 

    13 text {*

    14   Example instantiation of the abstract separation algebra to the sliced-memory

    15   model used for building a separation logic in ``Verification of Programs in

    16   Virtual Memory Using Separation Logic'' (PhD Thesis) by Rafal Kolanski.

    17 

    18   We wrap up the concept of physical and virtual pointers as well as value

    19   (usually a byte), and the page table root, into a datatype for instantiation.

    20   This avoids having to produce a hierarchy of type classes.

    21 

    22   The result is more general than the original. It does not mention the types

    23   of pointers or virtual memory addresses. Instead of supporting only

    24   singleton page table roots, we now support sets so we can identify a single

    25   0 for the monoid.

    26   This models multiple page tables in memory, whereas the original logic was

    27   only capable of one at a time.

    28 *}

    29 

    30 datatype ('p,'v,'value,'r) vm_sep_state

    31   = VMSepState "((('p \<times> 'v) \<rightharpoonup> 'value) \<times> 'r set)"

    32 

    33 instantiation vm_sep_state :: (type, type, type, type) sep_algebra

    34 begin

    35 

    36 fun

    37   vm_heap :: "('a,'b,'c,'d) vm_sep_state \<Rightarrow> (('a \<times> 'b) \<rightharpoonup> 'c)" where

    38   "vm_heap (VMSepState (h,r)) = h"

    39 

    40 fun

    41   vm_root :: "('a,'b,'c,'d) vm_sep_state \<Rightarrow> 'd set" where

    42   "vm_root (VMSepState (h,r)) = r"

    43 

    44 definition

    45   sep_disj_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state

    46                             \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state \<Rightarrow> bool" where

    47   "sep_disj_vm_sep_state x y = vm_heap x \<bottom> vm_heap y"

    48 

    49 definition

    50   zero_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state" where

    51   "zero_vm_sep_state \<equiv> VMSepState (empty, {})"

    52 

    53 fun

    54   plus_vm_sep_state :: "('a, 'b, 'c, 'd) vm_sep_state

    55                         \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state

    56                         \<Rightarrow> ('a, 'b, 'c, 'd) vm_sep_state" where

    57   "plus_vm_sep_state (VMSepState (x,r)) (VMSepState (y,r'))

    58      = VMSepState (x ++ y, r \<union> r')"

    59 

    60 instance

    61   apply default

    62         apply (simp add: zero_vm_sep_state_def sep_disj_vm_sep_state_def)

    63        apply (fastforce simp: sep_disj_vm_sep_state_def map_disj_def)

    64       apply (case_tac x, clarsimp simp: zero_vm_sep_state_def)

    65      apply (case_tac x, case_tac y)

    66      apply (fastforce simp: sep_disj_vm_sep_state_def map_add_ac)

    67     apply (case_tac x, case_tac y, case_tac z)

    68     apply (fastforce simp: sep_disj_vm_sep_state_def)

    69    apply (case_tac x, case_tac y, case_tac z)

    70    apply (fastforce simp: sep_disj_vm_sep_state_def map_add_disj)

    71   apply (case_tac x, case_tac y, case_tac z)

    72   apply (fastforce simp: sep_disj_vm_sep_state_def map_add_disj map_disj_com)

    73   done

    74 

    75 end

    76 

    77 end

    78