--#include "ChipModel.alfa"

--#include "Alfa/PropositionalCalculus.alfa"

--#include "Alfa/MaybeProp.alfa"

package PropertyDefs (FM::Set -> Set)(fm::FiniteMaps.FiniteMap FM Natural.Nat)(Word::Set)(RegFile::Set)  where
  open Propositional  use  Prop,  Absurdity,  Pred,  Rel,  And,  AndIntro,  AndElim1,  AndElim2,  AndElimCont
  open Types  use  Maybe
  open Identity  use  (==),  subst,  substSym,  refl
  open Tuples  use  Pair,  fst,  snd
  open Lists  use  List,  filter
  open Booleans  use  Bool
  open Natural  use  Nat,  natEq
  open ChipModel FM fm Word RegFile  use  Channel,  Packet,  Regs,  ChipState,  Alg,  Algs,  doPacket,  chip
  open State  use  StateM,  return,  uncurry,  inst,  load,  store,  update,  inFst,  inSnd
  open Memories FM fm Word  use  Memory,  Data,  Addr
  open Protected  use  EnvEx,  inst,  Protect,  protect,  mmprot,  runProtected
  open MaybeDefs  use  Maybe,  maybe,  MaybeProp,  MaybePropD
  open Monads  use  Monad,  return,  (>>=),  (>>),  liftM,  ap,  liftM2,  sequence_,  sequence,  mapM
  -- The property that the result of a state monad is independent of the initial state:
  StateIndependent (A::Set)(S::Set)(m::StateM S A) :: Prop
    = (s1::S) -> (s2::S) -> (==) A (fst A S (m s1)) (fst A S (m s2))
  RelatedResult (A::Set)(S::Set)(R::Rel S)(r1::Pair A S)(r2::Pair A S) :: Prop
    = And ((==) A (fst A S r1) (fst A S r2)) (R (snd A S r1) (snd A S r2))
  MostlyStateIndependent (A::Set)(S::Set)(R::Rel S)(m::StateM S A) :: Prop
    = (s1::S) -> (s2::S) -> (r::R s1 s2) -> RelatedResult A S R (m s1) (m s2)
  bindIndependent (S::Set)
                  (A::Set)
                  (B::Set)
                  (R::Rel S)
                  (m1::StateM S A)
                  (xm2::A -> StateM S B)
                  (p1::MostlyStateIndependent A S R m1)
                  (p2::(a::A) -> MostlyStateIndependent B S R (xm2 a))
    :: MostlyStateIndependent B S R (State.(>>=) S A B m1 xm2)
    = \(s1::S) ->
      \(s2::S) ->
      \(r::R s1 s2) ->
      AndElimCont
        ((==) A (fst A S (m1 s1)) (fst A S (m1 s2)))
        (R (snd A S (m1 s1)) (snd A S (m1 s2)))
        (RelatedResult B S R (State.(>>=) S A B m1 xm2 s1) (State.(>>=) S A B m1 xm2 s2))
        (p1 s1 s2 r)
        (\(a::(==) A (fst A S (m1 s1)) (fst A S (m1 s2))) ->
         \(b::R (snd A S (m1 s1)) (snd A S (m1 s2))) ->
         subst
           A
           (fst A S (m1 s1))
           (fst A S (m1 s2))
           (\(h::A) -> RelatedResult B S R (xm2 (fst A S (m1 s1)) (snd A S (m1 s1))) (xm2 h (snd A S (m1 s2))))
           a
           (p2 (fst A S (m1 s1)) (snd A S (m1 s1)) (snd A S (m1 s2)) b))
  MostlyStateIndependentP (A::Set)(S::Set)(R::Rel S)(valid::Addr -> Bool)(m::Protect (StateM S) Addr A) :: Prop
    = MostlyStateIndependent (Maybe A) S R (m valid)
  bindIndependentP (S::Set)
                   (A::Set)
                   (B::Set)
                   (R::Rel S)
                   (valid::Addr -> Bool)
                   (m1::Protect (StateM S) Addr A)
                   (xm2::A -> Protect (StateM S) Addr B)
                   (p1::MostlyStateIndependentP A S R valid m1)
                   (p2::(a::A) -> MostlyStateIndependentP B S R valid (xm2 a))
    :: MostlyStateIndependentP B S R valid ((>>=) A B (Protect (StateM S) Addr) (inst (\(A'::Set) -> S -> Pair A' S) (Addr -> Bool) (State.inst S)) m1 xm2)
    = \(s1::S) ->
      \(s2::S) ->
      \(r::R s1 s2) ->
      AndElimCont
        ((==) (Maybe A) (fst (Maybe A) S (m1 valid s1)) (fst (Maybe A) S (m1 valid s2)))
        (R (snd (Maybe A) S (m1 valid s1)) (snd (Maybe A) S (m1 valid s2)))
        (RelatedResult
           (Maybe B)
           S
           R
           ((>>=) A B (Protect (StateM S) Addr) (inst (\(A'::Set) -> (h::S) -> Pair A' S) ((h::Addr) -> Bool) (State.inst S)) m1 xm2 valid s1)
           ((>>=) A B (Protect (StateM S) Addr) (inst (\(A'::Set) -> (h::S) -> Pair A' S) ((h::Addr) -> Bool) (State.inst S)) m1 xm2 valid s2))
        (p1 s1 s2 r)
        (\(a::(==) (Maybe A) (fst (Maybe A) S (m1 valid s1)) (fst (Maybe A) S (m1 valid s2))) ->
         \(b::R (snd (Maybe A) S (m1 valid s1)) (snd (Maybe A) S (m1 valid s2))) ->
         subst
           (Maybe A)
           (fst (Maybe A) S (m1 valid s1))
           (fst (Maybe A) S (m1 valid s2))
           (\(h::Maybe A) ->
            RelatedResult
              (Maybe B)
              S
              R
              ((>>=) A B (Protect (StateM S) Addr) (inst (\(A'::Set) -> (h'::S) -> Pair A' S) ((h'::Addr) -> Bool) (State.inst S)) m1 xm2 valid s1)
              (maybe A (S -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) h (snd (Maybe A) S (m1 valid s2))))
           a
           (MaybePropD
              A
              ((h::S) -> Pair (Maybe B) S)
              ((State.inst S).unit (Maybe B) Nothing@_)
              (\(a'::A) -> xm2 a' valid)
              (fst (Maybe A) S (m1 valid s1))
              (\(h::S -> Pair (Maybe B) S) ->
               RelatedResult
                 (Maybe B)
                 S
                 R
                 ((>>=) A B (Protect (StateM S) Addr) (inst (\(A'::Set) -> (h'::S) -> Pair A' S) ((h'::Addr) -> Bool) (State.inst S)) m1 xm2 valid s1)
                 (h (snd (Maybe A) S (m1 valid s2))))
              (\(h::(==) (Maybe A) Nothing@_ (fst (Maybe A) S (m1 valid s1))) ->
               subst
                 (Maybe A)
                 Nothing@_
                 (fst (Maybe A) S (m1 valid s1))
                 (\(h'::Maybe A) ->
                  RelatedResult
                    (Maybe B)
                    S
                    R
                    (maybe A (S -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) h' (snd (Maybe A) S (m1 valid s1)))
                    (maybe A (S -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) Nothing@_ (snd (Maybe A) S (m1 valid s2))))
                 h
                 (AndIntro
                    ((==)
                       (Maybe B)
                       (fst
                          (Maybe B)
                          S
                          (maybe A ((h0::S) -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) Nothing@_ (snd (Maybe A) S (m1 valid s1))))
                       (fst
                          (Maybe B)
                          S
                          (maybe A ((h0::S) -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) Nothing@_ (snd (Maybe A) S (m1 valid s2)))))
                    (R
                       (snd
                          (Maybe B)
                          S
                          (maybe A ((h0::S) -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) Nothing@_ (snd (Maybe A) S (m1 valid s1))))
                       (snd
                          (Maybe B)
                          S
                          (maybe A ((h0::S) -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) Nothing@_ (snd (Maybe A) S (m1 valid s2)))))
                    (refl
                       (Maybe B)
                       (fst
                          (Maybe B)
                          S
                          (maybe A ((h0::S) -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) Nothing@_ (snd (Maybe A) S (m1 valid s1)))))
                    b))
              (\(a'::A) ->
               \(h::(==) (Maybe A) (Just@_ a') (fst (Maybe A) S (m1 valid s1))) ->
               subst
                 (Maybe A)
                 (Just@_ a')
                 (fst (Maybe A) S (m1 valid s1))
                 (\(h'::Maybe A) ->
                  RelatedResult
                    (Maybe B)
                    S
                    R
                    (maybe A (S -> Pair (Maybe B) S) ((State.inst S).unit (Maybe B) Nothing@_) (\(a'::A) -> xm2 a' valid) h' (snd (Maybe A) S (m1 valid s1)))
                    (xm2 a' valid (snd (Maybe A) S (m1 valid s2))))
                 h
                 (p2 a' (snd (Maybe A) S (m1 valid s1)) (snd (Maybe A) S (m1 valid s2)) b))))
  -- Definition of what a good algorithm is:
  GoodAlg (alg::Alg) :: Prop
    = (ws::Data) -> (regf::RegFile) -> StateIndependent (Pair Data RegFile) Memory (doPacket alg ws regf)
  regfile (state::ChipState)(ch::Channel) :: RegFile
    = fm.lookup RegFile (snd Memory Regs state) ch
  sameChannel (ch::Channel)(p::Packet) :: Bool
    = natEq (fst Nat Data p) ch
  pick (ch::Channel) :: List Packet -> List Packet
    = filter Packet (sameChannel ch)
  -- The separation property (lhs simulates rhs):
  Separation (algs::Algs)(ch::Channel)(state1::ChipState)(state2::ChipState)(ps::List Packet) :: Prop
    = (==) (List Packet) (pick ch (chip algs state1 ps)) (chip algs state2 (pick ch ps))
  -- The separation property (same state on lhs & rhs):
  Separation1 (algs::Algs)(ch::Channel)(state::ChipState)(ps::List Packet) :: Prop
    = Separation algs ch state state ps
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "EqStateM"
var "StateIndependent" hide 2
var "RelatedResult" hide 2
var "bindIndependent" hide 6
var "bindIndependentP" hide 7
var "MostlyStateIndependentP" hide 2
var "MaybeProp" hide 5
var "MaybePropD" hide 2
var "MostlyStateIndependent" hide 2
 #-}