--#include "Memories.alfa"

--#include "Alfa/List.alfa"

--#include "Alfa/NatIdentities.alfa"

package MemoryProps
  (FM::Set -> Set)(fm::FiniteMaps.FiniteMap FM Natural.Nat)(Word::Set)
 where
  open Memories FM fm Word
   use  Addr,  nullPtr,  Memory,  Data,  storeList,  loadList,  updateM,
        lookupM,  updateSameM,  updateOtherM
  open Propositions  use  Prop,  Absurdity,  IsTrue
  open Identity
   use  Identical,  (==),  subst,  substSym,  sym,  trans,  refl,  cong2
  open Natural  use  Nat,  (+),  natEq,  natLt
  open NatIdentities
   use  succCong,  peano4,  addSucc,  zeroLtSucc,  addZero
  open Lists  use  List,  length,  cons
  peano4n (n::Nat) :: (==) Nat (Succ@_ n) n -> Absurdity
    = case n of {
        (Zero) -> peano4 Zero@_;
        (Succ n') ->
          \(h::(==) Nat (Succ@_ (Succ@_ n')) (Succ@_ n')) ->
          peano4n n' (succCong (Succ@_ n') n' h);}
  peano4' (n::Nat)(m::Nat) :: (==) Nat (Succ@_ n + m) n -> Absurdity
    = case m of {
        (Zero) -> peano4n n;
        (Succ n') ->
          case n of {
            (Zero) -> peano4 (Succ@_ Zero@_ + n');
            (Succ n0) ->
              \(h::(==) Nat (Succ@_ (Succ@_ n0) + Succ@_ n') (Succ@_ n0)) ->
              peano4'
                n0
                (Succ@_ n')
                (succCong
                   (Succ@_ n0 + Succ@_ n')
                   n0
                   (trans
                      Nat
                      (Succ@_ (Succ@_ n0 + Succ@_ n'))
                      (Succ@_ (Succ@_ n0) + Succ@_ n')
                      (Succ@_ n0)
                      (addSucc (Succ@_ n0) (Succ@_ n'))
                      h));};}
  peano4b (a::Nat)(n::Nat) :: (==) Nat (Succ@_ (a + n)) a -> Absurdity
    = substSym
        Nat
        (Succ@_ (a + n))
        (Succ@_ a + n)
        (\(h::Nat) -> (==) Nat h a -> Absurdity)
        (addSucc a n)
        (peano4' a n)
  -- Indexing into lists:
  index (A::Set)(xs::List A)(n::Nat)(p::IsTrue (natLt n (length A xs)))
    :: A
    = case xs of {
        (Nil) -> case p of { };
        (Cons x xs') ->
          case n of {
            (Zero) -> x;
            (Succ n') -> index A xs' n' p;};}
  lookup = lookupM
  update = updateM
  StoreProp (ws::Data)
            (mem::Memory)
            (a::Addr)
            (i::Nat)
            (p::IsTrue (natLt i (length Word ws)))
    :: Prop
    = (==) Word (lookup mem (a + i)) (index Word ws i p)
  AllStoreProp (ws::Data)(mem::Memory)(a::Addr) :: Prop
    = (i::Nat) ->
      (p::IsTrue (natLt i (length Word ws))) ->
      StoreProp ws mem a i p
  storeProp (ws::Data)
            (mem::Memory)
            (a::Addr)
            (i::Nat)
            (p::IsTrue (natLt i (length Word ws)))
    :: StoreProp ws (storeList a ws mem) a i p
    = case ws of {
        (Nil) -> case p of { };
        (Cons x xs) ->
          case i of {
            (Zero) ->
              updateSameM
                a
                (index Word (Cons@_ x xs) Zero@_ p)
                (storeList (Succ@_ a) xs mem);
            (Succ n) ->
              let ndgoal
                    :: StoreProp
                         (Cons@_ x xs)
                         (storeList a (Cons@_ x xs) mem)
                         a
                         (Succ@_ n)
                         p
                    = trans
                        Word
                        (lookupM (storeList a (Cons@_ x xs) mem) (a + Succ@_ n))
                        (lookupM (storeList (Succ@_ a) xs mem) (a + Succ@_ n))
                        (index Word (Cons@_ x xs) (Succ@_ n) p)
                        (let ndgoal
                               :: (==)
                                    Word
                                    (lookup
                                       (update a x (storeList (Succ@_ a) xs mem))
                                       (a + Succ@_ n))
                                    (lookup
                                       (storeList (Succ@_ a) xs mem)
                                       (a + Succ@_ n))
                               = updateOtherM
                                   (a + Succ@_ n)
                                   a
                                   x
                                   (storeList (Succ@_ a) xs mem)
                                   (peano4b a n)
                         in  ndgoal)
                        (let ndgoal
                               :: (==)
                                    Word
                                    (lookup
                                       (storeList (Succ@_ a) xs mem)
                                       (a + Succ@_ n))
                                    (index Word xs n p)
                               = subst
                                   Nat
                                   (Succ@_ a + n)
                                   (a + Succ@_ n)
                                   (\(h::Nat) ->
                                    (==)
                                      Word
                                      (lookupM (storeList (Succ@_ a) xs mem) h)
                                      (index Word xs n p))
                                   (sym
                                      Nat
                                      (a + Succ@_ n)
                                      (Succ@_ a + n)
                                      (addSucc a n))
                                   (storeProp xs mem (Succ@_ a) n p)
                         in  ndgoal)
              in  ndgoal;};}
  loadStoreLemma (ws::Data)(a::Addr)(mem::Memory)
    :: (==) Data (loadList a (length Word ws) (storeList a ws mem)) ws
    = case ws of {
        (Nil) ->
          refl Data (loadList a (length Word Nil@_) (storeList a Nil@_ mem));
        (Cons x xs) ->
          let indhyp
                :: (==)
                     Data
                     (loadList
                        (Succ@_ a)
                        (length Word xs)
                        (storeList (Succ@_ a) xs mem))
                     xs
                = loadStoreLemma xs (Succ@_ a) mem
              lemma (a::Addr)(i::Nat)(n::Nat)(x::Word)(m::Memory)
                :: (==)
                     Data
                     (loadList (Succ@_ a + i) n (update a x m))
                     (loadList (Succ@_ a + i) n m)
                = case n of {
                    (Zero) ->
                      refl Data (loadList (Succ@_ a + i) Zero@_ (updateM a x m));
                    (Succ n') ->
                      cong2
                        Word
                        (List Word)
                        Data
                        (lookupM (updateM a x m) (Succ@_ a + i))
                        (loadList (Succ@_ (Succ@_ a + i)) n' (updateM a x m))
                        (lookupM m (Succ@_ a + i))
                        (loadList (Succ@_ (Succ@_ a + i)) n' m)
                        (cons Word)
                        (updateOtherM (Succ@_ a + i) a x m (peano4' a i))
                        (lemma a (Succ@_ i) n' x m);}
          in  cong2
                Word
                (List Word)
                Data
                (lookupM (storeList a (Cons@_ x xs) mem) a)
                (loadList
                   (Succ@_ a)
                   (length Word xs)
                   (storeList a (Cons@_ x xs) mem))
                x
                xs
                (cons Word)
                (updateSameM a x (storeList (Succ@_ a) xs mem))
                (trans
                   (List Word)
                   (loadList
                      (Succ@_ a)
                      (length Word xs)
                      (storeList a (Cons@_ x xs) mem))
                   (loadList
                      (Succ@_ a)
                      (length Word xs)
                      (storeList (Succ@_ a) xs mem))
                   xs
                   (lemma
                      a
                      Zero@_
                      (length Word xs)
                      x
                      (storeList (Succ@_ a) xs mem))
                   indhyp);}
  -- The property that two memories are equal within a given range of addresses:
  EqRange (n::Nat)(a::Addr)(mem1::Memory)(mem2::Memory) :: Prop
    = (i::Nat) ->
      (p::IsTrue (natLt i n)) ->
      (==) Word (lookup mem1 (a + i)) (lookup mem2 (a + i))
  {- Proof that storing data in two different memories yields memories that are equal
within the range where the data was stored: -}
  storeEqRange (ws::Data)(a::Addr)(mem1::Memory)(mem2::Memory)
    :: EqRange
         (length Word ws)
         a
         (storeList a ws mem1)
         (storeList a ws mem2)
    = \(i::Nat) ->
      \(p::IsTrue (natLt i (length Word ws))) ->
      trans
        Word
        (lookup (storeList a ws mem1) (a + i))
        (index Word ws i p)
        (lookup (storeList a ws mem2) (a + i))
        (storeProp ws mem1 a i p)
        (sym
           Word
           (lookup (storeList a ws mem2) (a + i))
           (index Word ws i p)
           (storeProp ws mem2 a i p))
  -- Proof that reading the range where two different memories are equal gives the same result:
  loadEqRange (a::Addr)
              (n::Nat)
              (mem1::Memory)
              (mem2::Memory)
              (r::EqRange n a mem1 mem2)
    :: (==) Data (loadList a n mem1) (loadList a n mem2)
    = case n of {
        (Zero) -> refl Data (loadList a Zero@_ mem1);
        (Succ n') ->
          cong2
            Word
            (List Word)
            Data
            (lookupM mem1 a)
            (loadList (Succ@_ a) n' mem1)
            (lookupM mem2 a)
            (loadList (Succ@_ a) n' mem2)
            (cons Word)
            (r Zero@_ (zeroLtSucc n'))
            (loadEqRange
               (Succ@_ a)
               n'
               mem1
               mem2
               (\(i::Nat) ->
                \(p::IsTrue (natLt i n')) ->
                subst
                  Nat
                  (Succ@_ (a + i))
                  (Succ@_ a + i)
                  (\(h::Nat) -> (==) Word (lookup mem1 h) (lookup mem2 h))
                  (addSucc a i)
                  (r (Succ@_ i) p)));}
  lookupEqRange (a::Addr)
                (n::Nat)
                (mem1::Memory)
                (mem2::Memory)
                (p::IsTrue (natLt a n))
                (r::EqRange n nullPtr mem1 mem2)
    :: (==) Word (lookup mem1 a) (lookup mem2 a)
    = substSym
        Nat
        a
        (Zero@_ + a)
        (\(h::Nat) -> (==) Word (lookup mem1 h) (lookup mem2 h))
        (addZero a)
        (r a p)
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "index" hide 1
var "lookup" infix 9 as "!"
var "update" mixfix as "[3/1:=2]"
var "EqRange" distfix4 as "»" with symbolfont
 #-}