Theory Sep_Block_Allocator

section ‹Generic Block Allocator›
theory Sep_Block_Allocator
imports "../../lib/Monad"
begin

  text ‹This theory specifies the concepts of memory allocation and deallocation.
    It is parameterized over the actual type of blocks.
  ›

  subsection ‹Memory and Addresses›

  text ‹A memory is a list of allocated or already freed blocks.
    Allocated blocks are modeled by @{term ‹Some blk›}, 
    freed blocks are modeled by @{term ‹None›}
  ›  
  datatype 'blk memory = MEMORY (the_memory: "'blk option list")
  define_lenses memory

  text ‹An address indexes a block, and then addresses into the value of this block.›
  datatype 'baddr addr = ADDR nat 'baddr

  text ‹A pointer is either ‹null›, or an address›
  datatype 'addr rptr = RP_NULL | RP_ADDR (the_addr: "'addr")
  hide_const (open) the_addr

  text ‹Type-class to model that there is a base address.›  
  (* TODO: Remove from semantics, move to reasoning infrastructure? *)
  class this_addr = fixes this_addr :: 'a  
    
  text ‹We immediately show that the typeclass is not empty. 
    This avoids confusion of the code generator with lemmas depending on this typeclass.›
  typedecl this_addr_witness
  instantiation this_addr_witness :: this_addr begin
    instance ..
  end
  
  
  subsection ‹Memory Functions›
    
  text ‹
    We specify the standard functions ‹alloc›, ‹free›, ‹load›, and ‹store›. 
    They are parameterized over load and store functions for blocks.
    
    Additionally, we specify a ‹check_ptr› function, that asserts that a pointer is valid,
    i.e., is either ‹null›, or points to an allocated block, and its block address is valid 
    for this block.
  ›
  
  locale block_allocator1 =
    fixes static_err :: 'err
      and mem_err :: 'err
      and bload :: "'baddr::this_addr ⇒ ('val,_,'c::monoid_add,'block,'err) M"
      and bstore :: "'val ⇒ 'baddr ⇒ (unit,_,'c::monoid_add,'block,'err) M"
      and bcheck_addr :: "'baddr ⇒ (unit,_,'c::monoid_add,'block,'err) M"
  begin

    text ‹Allocate a new block, and a pointer to its start›
    definition alloc :: "'block ⇒ ('baddr addr rptr,_,_,'block memory,'err) M"
    where "alloc init ≡ zoom (lift_lens static_err the_memory⇩L) (doM {
      blocks ← Monad.get;
      let bi = length blocks;
      let blocks = blocks @ [Some init];
      Monad.set blocks;
      return (RP_ADDR (ADDR bi this_addr))
    })"

    text ‹Free a block, specified by a pointer to its start›    
    definition free :: "'baddr addr rptr ⇒ (unit,_,_,'block memory,'err) M"
    where "free ≡ 
      λRP_ADDR (ADDR bi ba) ⇒ doM {
          fcheck mem_err (ba=this_addr);
          ―‹ TODO: Use load here! ›
          let L = lift_lens static_err the_memory⇩L ∙ (lift_lens mem_err (idx⇩L bi));
          blk ← use L;
          fcheck mem_err (blk ≠ None);
          L ::= None
        } 
      | _ ⇒ fail mem_err"
      
    text ‹We define a lens that focuses a block index. ›  
    (* TODO: Can we define lenses to focus addresses/pointers instead? *)
    definition "lens_of_bi bi ≡ the_memory⇩L ∙⇩L idx⇩L bi ∙⇩L the⇩L"
    abbreviation "elens_of_bi bi ≡ lift_lens mem_err (lens_of_bi bi)"
    lemma lens_of_bi[simp, intro!]: "hlens (lens_of_bi bi)"
      unfolding lens_of_bi_def by auto
    
    text ‹Load from an address›  
    definition "load ≡ λRP_ADDR (ADDR bi ba) ⇒ zoom (elens_of_bi bi) (bload ba) | _ ⇒ fail mem_err"
    text ‹Store at an address›  
    definition "store ≡ λx. λRP_ADDR (ADDR bi ba) ⇒ zoom (elens_of_bi bi) (bstore x ba) | _ ⇒ fail mem_err"
    
    text ‹Check that pointer is valid›
    definition "check_ptr ≡ λRP_NULL ⇒ return () | RP_ADDR (ADDR bi ba) ⇒ zoom (elens_of_bi bi) (bcheck_addr ba)"
    
    text ‹The empty memory›
    definition "empty_memory ≡ MEMORY []"
    
  end    

  subsection ‹Isabelle Code Generator Setup›
  text ‹Setup to make the semantics executable inside Isabelle/HOL›
  
  lemmas block_allocator1_code[code] =
    block_allocator1.alloc_def 
    block_allocator1.free_def
    block_allocator1.lens_of_bi_def
    block_allocator1.load_def
    block_allocator1.store_def
    block_allocator1.check_ptr_def
    block_allocator1.empty_memory_def
  
  
end