--#include "alfa/ChipModel.alfa" --#include "Alfa/BoolProp.alfa" --#include "NatProofs.alfa" --#include "FunFMProofs.alfa" package SeparationProof where open Logic use IsTrue, subst, substSym, cong, sym, cong2, trans open Utils use IsPredTrue, PredIsTrue open BoolProp use ifPropD, ifProp, ifTrueProp, ifFalseProp open Module_Prelude use List, fst, snd, (==), Tuple2, Bool, PredTrue, (>>), Unit, (>>=), flip, (<), Monad, return open Module_Monad use liftM open Module_Nat use Nat, derived__Nat_Eq_Nat, eqNat open NatProofs use congSucc, eqId, eqNatRefl, idEq open Module_Algorithms use RegFile, Reg, Alg open Module_ChipModel use pick, doPacket, Channel, Regs, ChipState, Packet, onePacket, chip, Algs, Invariant, GoodAlg, regfile, CondSeparation open Module_Memories use Addr, Word, Memory, Data open Module_State use StateM, runS, st, load, update, inFst, inSnd open Module_FM use FiniteMap, empty, lookup, update open Module_FunFM use FM, PredFM, inst__FunFM_10_1 open FunFMProofs use lookupUpdateLemma, updateOtherLemma proof (ch::Channel) (algs::Algs) (goodAlgs::GoodAlg (algs ch)) (state1::ChipState) (state2::ChipState) (inv::Invariant state1 state2 ch) (ps::List Packet) :: (===) (List Packet) (pick ch (chip algs state1 ps)) (chip algs state2 (pick ch ps)) = case state1 of { (Tuple2 mem1 regs1) -> case state2 of { (Tuple2 mem2 regs2) -> case ps of { (Nil) -> Ref@_; (Cons p ps) -> case p of { (Tuple2 ch' ws) -> let one = runS ChipState (Tuple2 Channel Data) (onePacket algs (Tuple2@_ ch' ws)) r1 = one state1 r2 = one state2 p1 = fst Packet (Tuple2 Memory Regs) r1 p2 = fst Packet (Tuple2 Memory Regs) r2 state1' = snd (Tuple2 Channel Data) ChipState r1 state2' = snd (Tuple2 Channel Data) ChipState r2 regs1' = snd Memory Regs state1' regs2' = snd Memory Regs state2' sameCh (h::IsTrue ((==) Channel derived__Nat_Eq_Nat ch' ch)) :: (===) (List Packet) (Cons@_ p1 (pick ch (chip algs state1' ps))) (Cons@_ p2 (chip algs state2' (pick ch ps))) = let chId :: (===) Channel ch' ch = eqId ch' ch (IsPredTrue ((==) Channel derived__Nat_Eq_Nat ch' ch) h) d1 :: Tuple2 (Tuple2 Data RegFile) Memory = runS Memory (Tuple2 Data RegFile) (doPacket (algs ch') ws (regfile ch' state1)) mem1 d2 (regf2::RegFile) :: Tuple2 (Tuple2 Data RegFile) Memory = runS Memory (Tuple2 Data RegFile) (doPacket (algs ch') ws regf2) mem2 inv' :: Invariant state1 state2 ch' = substSym Channel ch' ch (Invariant state1 state2) chId inv ga :: GoodAlg (algs ch') = substSym Channel ch' ch (\(h'::Channel) -> GoodAlg (algs h')) chId goodAlgs gap :: (===) (Tuple2 Data RegFile) (fst (Tuple2 Data RegFile) Memory d1) (fst (Tuple2 Data RegFile) Memory (d2 (regfile ch' state1))) = ga ws (regfile ch' state1) mem1 mem2 go :: (===) (Tuple2 Data RegFile) (fst (Tuple2 Data RegFile) Memory d1) (fst (Tuple2 Data RegFile) Memory (d2 (regfile ch' state2))) = subst RegFile (regfile ch' (Tuple2@_ mem1 regs1)) (regfile ch' (Tuple2@_ mem2 regs2)) (\(h'::RegFile) -> (===) (Tuple2 Data RegFile) (fst (Tuple2 Data RegFile) Memory d1) (fst (Tuple2 Data RegFile) Memory (d2 h'))) inv' gap p1p2 :: (===) Packet p1 p2 = cong Data Packet (fst Data RegFile (fst (Tuple2 Data RegFile) Memory d1)) (fst Data RegFile (fst (Tuple2 Data RegFile) Memory (d2 (regfile ch' (Tuple2@_ mem2 regs2))))) (\(h'::Data) -> Tuple2@_ ch' h') (cong (Tuple2 Data RegFile) Data (fst (Tuple2 Data RegFile) Memory d1) (fst (Tuple2 Data RegFile) Memory (d2 (regfile ch' (Tuple2@_ mem2 regs2)))) (fst Data RegFile) go) inv'' :: Invariant state1' state2' ch = subst RegFile (regfile ch' (Tuple2@_ mem1 regs1)) (regfile ch' (Tuple2@_ mem2 regs2)) (\(h'::RegFile) -> (===) RegFile (regfile ch state1') (lookup FM RegFile inst__FunFM_10_1 (update FM RegFile inst__FunFM_10_1 ch' (snd Data RegFile (fst (Tuple2 Data RegFile) Memory (d2 h'))) regs2) ch)) inv' (subst (Tuple2 Data RegFile) (fst (Tuple2 Data RegFile) Memory d1) (fst (Tuple2 Data RegFile) Memory (d2 (regfile ch' (Tuple2@_ mem1 regs1)))) (\(h'::Tuple2 Data RegFile) -> (===) RegFile (regfile ch state1') (lookup FM RegFile inst__FunFM_10_1 (update FM RegFile inst__FunFM_10_1 ch' (snd Data RegFile h') regs2) ch)) gap (sym RegFile (lookup FM RegFile inst__FunFM_10_1 (update FM RegFile inst__FunFM_10_1 ch' (snd Data RegFile (fst (Tuple2 Data RegFile) Memory d1)) regs2) ch) (regfile ch state1') (lookupUpdateLemma RegFile ch ch' (snd Data RegFile (fst (Tuple2 Data RegFile) Memory d1)) regs2 regs1 (sym RegFile (lookup FM RegFile inst__FunFM_10_1 regs1 ch) (lookup FM RegFile inst__FunFM_10_1 regs2 ch) inv)))) in cong2 Packet (List Packet) (List Packet) p1 (pick ch (chip algs state1' ps)) p2 (chip algs state2' (pick ch ps)) (\(h'::Packet) -> \(h0::List Packet) -> Cons@_ h' h0) p1p2 (proof ch algs goodAlgs state1' state2' inv'' ps) otherCh (h::IsTrue ((==) Channel derived__Nat_Eq_Nat ch' ch) -> Absurdity) :: (===) (List Packet) (pick ch (chip algs state1' ps)) (chip algs state2 (pick ch ps)) = let inv1 :: Invariant state1 state1' ch = sym RegFile (regfile ch state1') (regfile ch (Tuple2@_ mem1 regs1)) (updateOtherLemma RegFile ch ch' (snd Data RegFile (fst (Tuple2 Data RegFile) Memory (runS Memory (Tuple2 Data RegFile) (doPacket (algs ch') ws (regfile ch' state1)) mem1))) regs1 (\(h'::(===) Channel ch ch') -> h (subst Channel ch ch' (\(h0::Channel) -> IsTrue (eqNat h0 ch)) h' (PredIsTrue (eqNat ch ch) (eqNatRefl ch))))) inv' :: Invariant state1' state2 ch = trans RegFile (regfile ch state1') (regfile ch (Tuple2@_ mem1 regs1)) (regfile ch (Tuple2@_ mem2 regs2)) (sym RegFile (regfile ch (Tuple2@_ mem1 regs1)) (regfile ch state1') inv1) inv in proof ch algs goodAlgs state1' state2 inv' ps in ifPropD (List Packet) (\(h::List Packet) -> (===) (List Packet) (pick ch (chip algs state1 (Cons@_ p ps))) (chip algs state2 h)) ((==) Channel derived__Nat_Eq_Nat ch' ch) (Cons@_ p (pick ch ps)) (pick ch ps) (\(h::Propositions.IsTrue ((==) Channel derived__Nat_Eq_Nat ch' ch)) -> ifTrueProp (List Packet) ((==) Channel derived__Nat_Eq_Nat ch' ch) (Cons@_ p1 (pick ch (chip algs state1' ps))) (pick ch (chip algs state1' ps)) (\(h'::List Packet) -> (===) (List Packet) h' (chip algs (Tuple2@_ mem2 regs2) (Cons@_ (Tuple2@_ ch' ws) (pick ch ps)))) h (sameCh h)) (\(h::(h::Propositions.IsTrue ((==) Channel derived__Nat_Eq_Nat ch' ch)) -> Propositions.Absurdity) -> ifFalseProp (List Packet) ((==) Channel derived__Nat_Eq_Nat ch' ch) (Cons@_ p1 (pick ch (chip algs state1' ps))) (pick ch (chip algs state1' ps)) (\(h'::List Packet) -> (===) (List Packet) h' (chip algs state2 (pick ch ps))) h (otherCh h));};};};} proofCondSeparation :: CondSeparation = \(algs::Algs) -> \(ch::Channel) -> \(state1::ChipState) -> \(state2::ChipState) -> \(ps::List Packet) -> ImpliesIntro (GoodAlg (algs ch)) (Implies (Invariant state1 state2 ch) ((===) (List Packet) (pick ch (chip algs state1 ps)) (chip algs state2 (pick ch ps)))) (\(goodAlg::GoodAlg (algs ch)) -> ImpliesIntro (Invariant state1 state2 ch) ((===) (List Packet) (pick ch (chip algs state1 ps)) (chip algs state2 (pick ch ps))) (\(inv::Invariant state1 state2 ch) -> proof ch algs goodAlg state1 state2 inv ps)) {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on var "updateOtherLemma" hide 5 var "IsPredTrue" hide 1 var "PredIsTrue" hide 1 #-}