Memories.hs

module Memories(
   Memory,Addr,Word,Data,
   Range,base,size,malloc,free,inRange,
   {-P: EqRange, -}
   nullPtr,initMem,lookupM,updateM,storeList,loadRange) where
import qualified FunFM as FM
import FM
import Nat

type Addr = Nat
type Word = Int
type Data = [Word]

nullPtr = O

data Memory = M Addr (FM.FM Word)

data Range = Range Addr Nat
base (Range b s) = b
size (Range b s) = s

-- inRange (Range b s) a = b<=a && a<s+b
inRange (Range b s) a = b `leNat` a && a `ltNat` s+b

initMem :: Memory
initMem = M nullPtr (FM.empty 0)

malloc :: Nat -> Memory -> (Range,Memory)
free :: Range -> Memory -> Memory

-- Initial dummy allocation/deallaction functions:
malloc n m = (Range nullPtr n,m)
free r m = m
{-
-- More realistic allocaton/deallocation functions:
malloc n (M b m) = (Range b n,M (n+b) m)
free (Range b n) (M _ m) = M b m -- can only free the last block allocated!!
-}

lookupM (M _ m) = FM.lookup m
updateM a w (M free m) = M free (FM.update a w m)

storeList a [] m = m
storeList a (w:ws) m = updateM a w (storeList (S a) ws m)

loadList a O m = []
loadList a (S n) m = lookupM m a:loadList (S a) n m

loadRange r m = loadList (base r) (size r) m

{-P:
assert LookupUpdateM = LookupUpdate lookupM updateM  {-#cert:LookupUpdateM#-}
assert UpdateSameM   = UpdateSame   lookupM updateM  {-#cert:UpdateSameM#-}
assert UpdateOtherM  = UpdateOther  lookupM updateM  {-#cert:UpdateOtherM#-}

property StoreProp =
  {| ws,mem,a,i |
       True {i `ltNat` len ws} ==> {lookupM mem (i+a)} === {index ws i} |}

assert StoreList = {-#cert:StoreList#-}
  All ws . All mem . All a . All i . StoreProp ws {storeList a ws mem} a i

property InRange r = {| a | True {inRange r a} |}

property EqRange r =
     {| m1,m2 | All a . InRange r a ==> {lookupM m1 a} === {lookupM m2 a} |}

assert StoreEqRange = {-#cert:StoreEqRange#-}
    All ws . All a . All mem1 . All mem2 .
    EqRange {Range a (len ws)} {storeList a ws mem1} {storeList a ws mem2}

assert LookupInRange =  {-#cert:LookupInRange#-}
    All a . All r . All mem1 . All mem2 .
    InRange r a ==>
    EqRange r mem1 mem2 ==>
    {lookupM mem1 a} === {lookupM mem2 a}

assert LoadEqRange = {-#cert:LoadEqRange#-}
    All r . All mem1 . All mem2 .
    EqRange r mem1 mem2 ==> {loadRange r mem1}==={loadRange r mem2}
-}