--#include "alfa/ChipModel.alfa"

--#include "SeparationProof.alfa"

--#include "GoodAlgProof.alfa"

package ChipModelProofs where
  open Module_Prelude  use  List
  open Module_ChipModel
   use  Channel,  ChipState,  Packet,  chip,  Separation,
        CondSeparation,  Algs,  GoodAlg,  Invariant,  pick,  AllGoodAlg,
        SameState
  open GoodAlgProof  use  doAlgLemma,  proof
  proofAllGoodAlg :: AllGoodAlg
    = GoodAlgProof.proof
  proofSameState :: SameState
    = \(state::Module_Prelude.Tuple2
                 Module_Memories.Memory
                 (Module_FunFM.FM (Module_FunFM.FM Module_Prelude.Int))) ->
      \(ch::Module_Nat.Nat) ->
      Ref@_
  proofSeparation :: Separation
    = \(algs::Algs) ->
      \(ch::Channel) ->
      \(state::ChipState) ->
      SeparationProof.proof
        ch
        algs
        (proofAllGoodAlg (algs ch))
        state
        state
        (proofSameState state ch)
{-# Alfa unfoldgoals off
brief on
hidetypeannots on
wide

nd
hiding on
var "StateIndependent" hide 2
var "proofCondSeparation" hide 4
 #-}