Theory Sep_Array_Block

section ‹Array-Blocks›
theory Sep_Array_Block
imports Sep_Block_Allocator
begin

text ‹This theory specifies the concept of blocks that are arrays of values. 
  It is parameterized over values.
›

subsection ‹Blocks and Block Addresses›

text ‹A block is modeled as list of values›
type_synonym 'val block = "'val list" 

text ‹An address into a block is an index into the list, and an address into the value.
  Note that, for technical reasons, we model the index into the list by an integer, instead of a 
  nat.›
datatype 'vaddr baddr = BADDR int 'vaddr
(* TODO: Can we use nat here? *)


text ‹The base address of a block points to its first index.›
instantiation baddr :: (this_addr) this_addr begin
  definition "this_addr ≡ BADDR 0 this_addr"
  instance ..
end

subsection ‹Memory and Pointer Operations›

locale array_block1 =
  fixes static_err :: 'err
    and mem_err :: 'err
    and vload :: "'vaddr::this_addr ⇒ ('val,_,'c::monoid_add,'val,'err) M"
    and vstore :: "'val ⇒ 'vaddr ⇒ (unit,_,'c::monoid_add,'val,'err) M"
    and vgep :: "'vaddr ⇒ 'vidx ⇒ ('vaddr,_,'c::monoid_add,'val,'err) M"
begin
  definition load :: "'vaddr baddr ⇒ ('val,_,'c::monoid_add,'val block,'err) M" where
    "load ≡ λBADDR i va ⇒ fcheck mem_err (i≥0) ⪢ zoom (lift_lens mem_err (idx⇩L (nat i))) (vload va)"

  definition store :: "'val ⇒ 'vaddr baddr ⇒ (unit,_,'c::monoid_add,'val block,'err) M" where
    "store ≡ λx. λBADDR i va ⇒ fcheck mem_err (i≥0) ⪢ zoom (lift_lens mem_err (idx⇩L (nat i))) (vstore x va)" 

  text ‹Check that a block address is in range, i.e., at most one past the end of the actual block.›
  definition check_addr :: "'vaddr baddr ⇒ (unit,_,'c::monoid_add,'val block,'err) M" where
    "check_addr ≡ λBADDR i va ⇒ doM {blk←Monad.get; fcheck mem_err (0≤i ∧ i≤int (length blk))}"

  text ‹Index (offset) an address. It must point to the start of a value.›  
  definition checked_idx_baddr :: "'vaddr baddr ⇒ int ⇒ ('vaddr baddr, _,'c::monoid_add, 'val list, 'err) M" where 
  "checked_idx_baddr ≡ λBADDR i va ⇒ λj. doM {
    fcheck mem_err (va = this_addr);
    let r = BADDR (i+j) va;
    check_addr r;
    return r
  }"

  text ‹Advance an address into the structure of a value.›
  definition checked_gep_addr :: "'vaddr baddr ⇒ 'vidx ⇒ ('vaddr baddr, _,'c::monoid_add, 'val list, 'err) M"
    where
    "checked_gep_addr ≡ λBADDR i va ⇒ λvi. doM {
      fcheck mem_err  (i≥0);
      va ← zoom (lift_lens mem_err (idx⇩L (nat i))) (vgep va vi); 
      return (BADDR i va)
      }"
    
          
  subsection ‹Lifting of Pointer Operations to Block Allocator›
      
  sublocale ba: block_allocator1 static_err mem_err load store check_addr .
  
  definition init :: "'val ⇒ nat ⇒ 'val list" where "init v n ≡ replicate n v"
     

  definition "ba_allocn v n ≡ ba.alloc (init v n)"
  
  definition "checked_idx_ptr ≡ 
    λRP_NULL ⇒ λ_. fail mem_err 
  | RP_ADDR (ADDR bi ba) ⇒ λi. zoom (ba.elens_of_bi bi) (doM { ba←checked_idx_baddr ba i; return (RP_ADDR (ADDR bi ba))})"

  definition "checked_gep_ptr ≡ 
    λRP_NULL ⇒ λ_. fail mem_err 
  | RP_ADDR (ADDR bi ba) ⇒ λvi. zoom (ba.elens_of_bi bi) (doM { ba←checked_gep_addr ba vi; return (RP_ADDR (ADDR bi ba))})
  "
    
    
end


subsection ‹Isabelle Code Generator Setup›

lemmas array_block1_code[code] = 
  array_block1.load_def 
  array_block1.store_def
  array_block1.check_addr_def
  array_block1.checked_idx_baddr_def
  
  array_block1.checked_gep_addr_def
  array_block1.init_def
  array_block1.ba_allocn_def
  array_block1.checked_idx_ptr_def
  array_block1.checked_gep_ptr_def

end