--#include "alfa/ChipModel.alfa"

--#include "MemoriesProofs.alfa"

--#include "MemoryStateProofs.alfa"

--#include "Utils.alfa"

package GoodAlgProof where
  open Logic  use  cong2,  subst,  IsTrue
  open BoolProp  use  ifPropD,  ifProp,  ifTrueProp,  ifFalseProp
  open Utils  use  MaybePropD,  IsPredTrue
  open Module_Prelude
   use  List,  Unit,  Tuple2,  fst,  snd,  Bool,  Maybe,  (>>=),
        return,  maybe,  id,  PredTrue
  open Module_Monad  use  liftM
  open Module_Algorithms  use  RegFile,  Code,  runAlg,  Reg,  Alg
  open Module_Memories
   use  nullPtr,  Addr,  Word,  Data,  Range,  Memory,  EqRange,
        storeList,  inRange,  loadRange,  InRange,  lookupM,  updateM
  open Module_ChipModel
   use  doPacket3,  doPacket2,  doPacket,  finishPacket,
        StateIndependent,  GoodAlg,  AllGoodAlg
  open Module_State
   use  StateM,  runS,  returnS,  bindS,  load,
        inst__Monad_StateM = inst__State_11_1
  open Module_MemMonads  use  MemMonad,  rd,  wr
  open Module_MemoryState
   use  RelatedResult,  MostlyStateIndependent,  ReturnS_MSI,
        BindS_MSI,  inst__MemMonad_StateM = inst__MemoryState_8_1
  open Module_Protected
   use  EnvEx,  unE,  protect,  runProtected,  inst__Protected_10_1,
        Protect,  inst__Protected_18_1
  open Module_Nat  use  Nat,  len
  open MemoriesProofs
   use  proofLookupUpdateM,  proofStoreEqRange,  lemmaLoadEqRange,
        lemmaLookupInRange
  open MemoryStateProofs  use  return_MSI,  bindS_MSI
  ProtectM = Protect (StateM Memory) Addr
  mmp :: MemMonad ProtectM Addr Word
    = inst__Protected_18_1 (StateM Memory) Addr Word inst__MemMonad_StateM
  bindP (A::Set)(B::Set)
    :: ProtectM A -> (A -> ProtectM B) -> ProtectM B
    = (>>=) ProtectM A B mmp.method_1
  MostlyStateIndependentP (A::Set)
                          (r::Range)
                          (pm::Protect (StateM Memory) Addr A)
    :: Prop
    = MostlyStateIndependent
        (Maybe A)
        r
        (unE (StateM Memory) (Addr -> Bool) A pm (inRange r))
  returnP_MSI (A::Set)(a::A)(r::Range)
    :: MostlyStateIndependentP
         A
         r
         (return (Protect (StateM Memory) Addr) A mmp.method_1 a)
    = \(mem1::Memory) ->
      \(mem2::Memory) ->
      ImpliesIntro
        (EqRange r mem1 mem2)
        (RelatedResult
           (Maybe A)
           r
           (runS
              Memory
              (Maybe A)
              (return
                 (StateM Memory)
                 (Maybe A)
                 (inst__Monad_StateM Memory)
                 (Just@_ a))
              mem1)
           (runS
              Memory
              (Maybe A)
              (return
                 (StateM Memory)
                 (Maybe A)
                 (inst__Monad_StateM Memory)
                 (Just@_ a))
              mem2))
        (\(hyp::EqRange r mem1 mem2) ->
         AndIntro
           ((===)
              (Maybe A)
              (fst
                 (Maybe A)
                 Memory
                 (runS
                    Memory
                    (Maybe A)
                    (unE
                       (StateM Memory)
                       ((h::Addr) -> Bool)
                       A
                       (return (Protect (StateM Memory) Addr) A mmp.method_1 a)
                       (inRange r))
                    mem1))
              (fst
                 (Maybe A)
                 Memory
                 (runS
                    Memory
                    (Maybe A)
                    (unE
                       (StateM Memory)
                       ((h::Addr) -> Bool)
                       A
                       (return (Protect (StateM Memory) Addr) A mmp.method_1 a)
                       (inRange r))
                    mem2)))
           (EqRange r mem1 mem2)
           Ref@_
           hyp)
  liftM_MSI (A::Set)
            (B::Set)
            (r::Range)
            (f::A -> B)
            (m::StateM Memory A)
            (p::MostlyStateIndependent A r m)
    :: MostlyStateIndependent
         B
         r
         (liftM (StateM Memory) A B (inst__Monad_StateM Memory) f m)
    = bindS_MSI
        A
        B
        m
        (\(a::A) -> return (StateM Memory) B (inst__Monad_StateM Memory) (f a))
        r
        p
        (\(a::A) -> return_MSI B r (f a))
  bindP_MSI (A::Set)
            (B::Set)
            (m1::ProtectM A)
            (xm2::A -> ProtectM B)
            (r::Range)
            (pm1::MostlyStateIndependentP A r m1)
            (pxm2::(a::A) -> MostlyStateIndependentP B r (xm2 a))
    :: MostlyStateIndependentP B r (bindP A B m1 xm2)
    = let lemma
            :: MostlyStateIndependent
                 (Maybe B)
                 r
                 (bindS
                    Memory
                    (Maybe A)
                    (Maybe B)
                    (unE (StateM Memory) (Addr -> Bool) A m1 (inRange r))
                    (maybe
                       (StateM Memory (Maybe B))
                       A
                       (return
                          (StateM Memory)
                          (Maybe B)
                          (inst__Monad_StateM Memory)
                          Nothing@_)
                       (\(a::A) ->
                        unE
                          (StateM Memory)
                          ((h::Addr) -> Bool)
                          B
                          (xm2 a)
                          (inRange r))))
            = bindS_MSI
                (Maybe A)
                (Maybe B)
                (unE (StateM Memory) ((h::Addr) -> Bool) A m1 (inRange r))
                (maybe
                   (StateM Memory (Maybe B))
                   A
                   (return
                      (StateM Memory)
                      (Maybe B)
                      (inst__Monad_StateM Memory)
                      Nothing@_)
                   (\(a::A) ->
                    unE (StateM Memory) (Addr -> Bool) B (xm2 a) (inRange r)))
                r
                pm1
                (\(a::Maybe A) ->
                 MaybePropD
                   A
                   (StateM Memory (Maybe B))
                   (returnS (Maybe B) Memory Nothing@_)
                   (\(a'::A) ->
                    unE (StateM Memory) (Addr -> Bool) B (xm2 a') (inRange r))
                   a
                   (MostlyStateIndependent (Maybe B) r)
                   (\(h::(===) (Maybe A) Nothing@_ a) ->
                    return_MSI (Maybe B) r Nothing@_)
                   (\(a'::A) -> \(h::(===) (Maybe A) (Just@_ a') a) -> pxm2 a'))
      in  lemma
  protectLemma (A::Set)
               (a::Addr)
               (r::Range)
               (m::StateM Memory A)
               (p::InRange r a -> MostlyStateIndependent A r m)
    :: MostlyStateIndependentP
         A
         r
         (protect (StateM Memory) Addr A (inst__Monad_StateM Memory) a m)
    = ifPropD
        (StateM Memory (Maybe A))
        (MostlyStateIndependent (Maybe A) r)
        (inRange r a)
        (liftM
           (StateM Memory)
           A
           (Maybe A)
           (inst__Monad_StateM Memory)
           (\(a::A) -> Just@_ a)
           m)
        (return
           (StateM Memory)
           (Maybe A)
           (inst__Monad_StateM Memory)
           Nothing@_)
        (\(h::IsTrue (inRange r a)) ->
         liftM_MSI
           A
           (Maybe A)
           r
           (\(a::A) -> Just@_ a)
           m
           (p (IsPredTrue (inRange r a) h)))
        (\(h::(h::IsTrue (inRange r a)) -> Absurdity) ->
         return_MSI (Maybe A) r Nothing@_)
  runAlgLemma (r::Range)(code::Code)
    :: MostlyStateIndependentP
         RegFile
         r
         (runAlg (Protect (StateM Memory) Addr) mmp code)
    = case code of {
        (Done regf) -> returnP_MSI RegFile regf r;
        (Read a c) ->
          bindP_MSI
            Word
            RegFile
            (protect
               (StateM Memory)
               Addr
               Word
               (inst__Monad_StateM Memory)
               a
               (rd (StateM Memory) Addr Word inst__MemMonad_StateM a))
            (\(a'::Word) -> runAlg (Protect (StateM Memory) Addr) mmp (c a'))
            r
            (protectLemma
               Word
               a
               r
               (rd (StateM Memory) Addr Word inst__MemMonad_StateM a)
               (\(h::InRange r a) ->
                \(mem1::Memory) ->
                \(mem2::Memory) ->
                ImpliesIntro
                  (EqRange r mem1 mem2)
                  (And
                     ((===)
                        Word
                        (fst
                           Word
                           Memory
                           (runS
                              Memory
                              Word
                              (rd
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a)
                              mem1))
                        (fst
                           Word
                           Memory
                           (runS
                              Memory
                              Word
                              (rd
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a)
                              mem2)))
                     (EqRange r mem1 mem2))
                  (\(hyp::EqRange r mem1 mem2) ->
                   AndIntro
                     ((===)
                        Word
                        (fst
                           Word
                           Memory
                           (runS
                              Memory
                              Word
                              (rd
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a)
                              mem1))
                        (fst
                           Word
                           Memory
                           (runS
                              Memory
                              Word
                              (rd
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a)
                              mem2)))
                     (EqRange r mem1 mem2)
                     (lemmaLookupInRange a r mem1 mem2 h hyp)
                     hyp)))
            (\(a'::Word) -> runAlgLemma r (c a'));
        (Write a w c) ->
          bindP_MSI
            Unit
            RegFile
            (protect
               (StateM Memory)
               Addr
               Unit
               (inst__Monad_StateM Memory)
               a
               (wr (StateM Memory) Addr Word inst__MemMonad_StateM a w))
            (\(a'::Unit) -> runAlg (Protect (StateM Memory) Addr) mmp c)
            r
            (protectLemma
               Unit
               a
               r
               (wr (StateM Memory) Addr Word inst__MemMonad_StateM a w)
               (\(h::InRange r a) ->
                \(mem1::Memory) ->
                \(mem2::Memory) ->
                ImpliesIntro
                  (EqRange r mem1 mem2)
                  (And
                     ((===)
                        Unit
                        (fst
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem1))
                        (fst
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem2)))
                     (EqRange
                        r
                        (snd
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem1))
                        (snd
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem2))))
                  (\(hyp::EqRange r mem1 mem2) ->
                   AndIntro
                     ((===)
                        Unit
                        (fst
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem1))
                        (fst
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem2)))
                     (EqRange
                        r
                        (snd
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem1))
                        (snd
                           Unit
                           Memory
                           (runS
                              Memory
                              Unit
                              (wr
                                 (StateM Memory)
                                 Addr
                                 Word
                                 inst__MemMonad_StateM
                                 a
                                 w)
                              mem2)))
                     Ref@_
                     (\(a'::Addr) ->
                      ImpliesIntro
                        (PredTrue (inRange r a'))
                        ((===)
                           Word
                           (lookupM
                              (snd
                                 Unit
                                 Memory
                                 (runS
                                    Memory
                                    Unit
                                    (wr
                                       (StateM Memory)
                                       Addr
                                       Word
                                       inst__MemMonad_StateM
                                       a
                                       w)
                                    mem1))
                              a')
                           (lookupM
                              (snd
                                 Unit
                                 Memory
                                 (runS
                                    Memory
                                    Unit
                                    (wr
                                       (StateM Memory)
                                       Addr
                                       Word
                                       inst__MemMonad_StateM
                                       a
                                       w)
                                    mem2))
                              a'))
                        (\(hyp'::PredTrue (inRange r a')) ->
                         ImpliesElim
                           ((===) Word (lookupM mem1 a') (lookupM mem2 a'))
                           ((===)
                              Word
                              (lookupM
                                 (snd
                                    Unit
                                    Memory
                                    (runS
                                       Memory
                                       Unit
                                       (wr
                                          (StateM Memory)
                                          Addr
                                          Word
                                          inst__MemMonad_StateM
                                          a
                                          w)
                                       mem1))
                                 a')
                              (lookupM
                                 (snd
                                    Unit
                                    Memory
                                    (runS
                                       Memory
                                       Unit
                                       (wr
                                          (StateM Memory)
                                          Addr
                                          Word
                                          inst__MemMonad_StateM
                                          a
                                          w)
                                       mem2))
                                 a'))
                           (proofLookupUpdateM a' a w mem1 mem2)
                           (lemmaLookupInRange a' r mem1 mem2 hyp' hyp))))))
            (\(a'::Unit) -> runAlgLemma r c);}
  runProtectedLemma (regf::RegFile)(r::Range)(code::Code)
    :: MostlyStateIndependent
         RegFile
         r
         (runProtected
            (StateM Memory)
            RegFile
            (Addr -> Bool)
            (inst__Monad_StateM Memory)
            regf
            (inRange r)
            (runAlg (Protect (StateM Memory) Addr) mmp code))
    = liftM_MSI
        (Maybe RegFile)
        RegFile
        r
        (maybe RegFile RegFile regf (id RegFile))
        (unE
           (StateM Memory)
           ((h::Addr) -> Bool)
           RegFile
           (runAlg (Protect (StateM Memory) Addr) mmp code)
           (inRange r))
        (runAlgLemma r code)
  doPacket3Lemma (r::Range)(regf'::RegFile)
    :: MostlyStateIndependent (Tuple2 Data RegFile) r (doPacket3 r regf')
    = \(mem1::Memory) ->
      \(mem2::Memory) ->
      ImpliesIntro
        (EqRange r mem1 mem2)
        (And
           ((===)
              (Tuple2 Data RegFile)
              (fst
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem1))
              (fst
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem2)))
           (EqRange
              r
              (snd
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem1))
              (snd
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem2))))
        (\(hyp::EqRange r mem1 mem2) ->
         AndIntro
           ((===)
              (Tuple2 Data RegFile)
              (fst
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem1))
              (fst
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem2)))
           (EqRange
              r
              (snd
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem1))
              (snd
                 (Tuple2 Data RegFile)
                 Memory
                 (runS Memory (Tuple2 Data RegFile) (doPacket3 r regf') mem2)))
           (cong2
              Data
              RegFile
              (Tuple2 Data RegFile)
              (loadRange r mem1)
              regf'
              (loadRange r mem2)
              regf'
              (\(h::Data) -> \(h'::RegFile) -> Tuple2@_ h h')
              (lemmaLoadEqRange r mem1 mem2 hyp)
              Ref@_)
           hyp)
  doPacket2Lemma (code::Code)(r::Range)(regf::RegFile)
    :: MostlyStateIndependent
         (Tuple2 Data RegFile)
         r
         (doPacket2 code r regf)
    = bindS_MSI
        RegFile
        (Tuple2 Data RegFile)
        (runProtected
           (StateM Memory)
           RegFile
           (Addr -> Bool)
           (inst__Monad_StateM Memory)
           regf
           (inRange r)
           (runAlg (Protect (StateM Memory) Addr) mmp code))
        (doPacket3 r)
        r
        (runProtectedLemma regf r code)
        (doPacket3Lemma r)
  doAlgLemma (alg::Alg)(ws::Data)(regf::RegFile)
    :: StateIndependent
         Memory
         (Tuple2 (List Word) RegFile)
         (doPacket alg ws regf)
    = \(m1::Memory) ->
      \(m2::Memory) ->
      let r :: Range
            = Range@_ nullPtr (len Word ws)
          code :: Code
            = alg nullPtr regf
          sl :: Memory -> Memory
            = storeList nullPtr ws
          do2 = doPacket2 code r regf
          run1 = runS Memory (Tuple2 Data RegFile) do2 (sl m1)
          run2 = runS Memory (Tuple2 Data RegFile) do2 (sl m2)
          lemma :: RelatedResult (Tuple2 Data RegFile) r run1 run2
            = ImpliesElim
                (EqRange r (sl m1) (sl m2))
                (RelatedResult (Tuple2 Data RegFile) r run1 run2)
                (doPacket2Lemma (alg nullPtr regf) r regf (sl m1) (sl m2))
                (proofStoreEqRange ws nullPtr m1 m2)
      in  AndElim1
            ((===)
               (Tuple2 Data RegFile)
               (fst (Tuple2 Data RegFile) Memory run1)
               (fst (Tuple2 Data RegFile) Memory run2))
            (EqRange
               r
               (snd (Tuple2 Data RegFile) Memory run1)
               (snd (Tuple2 Data RegFile) Memory run2))
            lemma
  proof :: AllGoodAlg
    = doAlgLemma
{-# Alfa unfoldgoals off
brief on
hidetypeannots on
wide

nd
hiding on
var "StateIndependent" hide 2
var "MostlyStateIndependent" hide 1
var "RelatedResult" hide 1
var "bindS_MSI" hide 5
var "doPacket2Lemma" hide 3
var "RelatedResult2" hide 1
var "bindP" hide 2
var "bindP_MSI" hide 5
var "protectLemma" hide 1
var "MaybePropD" hide 5
var "liftM_MSI" hide 5
var "return_MSI" hide 2
 #-}