-- This file contains the proof of the separation property --#include "ChipModel.alfa" --#include "Alfa/Propositions.alfa" --#include "Alfa/Identity.alfa" --#include "Alfa/BoolProp.alfa" --#include "Alfa/NatIdentities.alfa" --#include "PropertyDefs.alfa" package ChipModelProps (FM::Set -> Set) (fm::FiniteMaps.FiniteMap FM Natural.Nat) (Word::Set) (RegFile::Set) where public open PropertyDefs FM fm Word RegFile use GoodAlg, regfile, pick, Separation, Separation1 public open ChipModel FM fm Word RegFile use Channel, Packet, Regs, ChipState, Alg, Code, Algs, doPacket, onePacket, chip public open Memories FM fm Word use Addr, Memory, Data, nullPtr, storeList, loadList open Monads use Monad, return, (>>=), (>>) open State use StateM, inFst, inSnd, update, load, inst open Tuples use Pair, Unit, unit, pair, fst, snd open Natural use Nat, natEq open Lists use List, cons, length, filter open Booleans use Bool, if open Propositions use Prop, Absurdity, AbsurdityElim, Triviality, TrivialityIntro, Pred, NDGoal, IsTrue open BoolProp use ifPropD, ifProp, ifTrueProp, ifFalseProp open Identity use (==), refl, trans, sym, cong, cong2, cong1, subst, substSym open NatIdentities use eq2id, natEqRefl fmProp (B::Set) (x1::Nat) (x2::Nat) (y::B) (fm1::FM B) (fm2::FM B) (p::(==) B (fm.lookup B fm1 x1) (fm.lookup B fm2 x1)) :: (==) B (fm.lookup B (fm.update B x2 y fm1) x1) (fm.lookup B (fm.update B x2 y fm2) x1) = fm.updateProp B x1 x2 y fm1 fm2 p fmProp2 (B::Set) (x1::Nat) (x2::Nat) (y::B) (fm1::FM B) (p::(==) Nat x1 x2 -> Absurdity) :: (==) B (fm.lookup B fm1 x1) (fm.lookup B (fm.update B x2 y fm1) x1) = sym B (fm.lookup B (fm.update B x2 y fm1) x1) (fm.lookup B fm1 x1) (fm.updateOther B x1 x2 y fm1 p) -- The invariant that is used in the proof of the separation property Invariant (state1::ChipState)(state2::ChipState)(ch::Channel) :: Prop = (==) RegFile (regfile state1 ch) (regfile state2 ch) -- The main part of the separation proof (lhs simulates rhs): separation (algs::Algs) (ch::Channel) (good::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 { (Pair mem1 regs1) -> case state2 of { (Pair mem2 regs2) -> case ps of { (Nil) -> Ref@_; (Cons p ps) -> case p of { (Pair ch' ws) -> let one = onePacket algs ch' ws p1 = fst Packet ChipState (one state1) p2 = fst Packet ChipState (one state2) state1' = snd Packet ChipState (one state1) state2' = snd Packet ChipState (one state2) regs1' = snd Memory Regs state1' regs2' = snd Memory Regs state2' sameCh (h::IsTrue (natEq ch' ch)) :: (==) (List Packet) (Cons@_ p1 (pick ch (chip algs state1' ps))) (Cons@_ p2 (chip algs state2' (pick ch ps))) = let inv' :: Invariant state1 state2 ch' = substSym Nat ch' ch (Invariant state1 state2) (eq2id ch' ch h) inv ga :: GoodAlg (algs ch') = substSym Channel ch' ch (\(h'::Nat) -> GoodAlg (algs h')) (eq2id ch' ch h) good go :: (==) (Pair Data RegFile) (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile (Pair@_ mem1 regs1) ch') mem1)) (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile (Pair@_ mem2 regs2) ch') mem2)) = subst RegFile (regfile (Pair@_ mem1 regs1) ch') (regfile (Pair@_ mem2 regs2) ch') (\(h'::RegFile) -> (==) (Pair Data RegFile) (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile state1 ch') mem1)) (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws h' mem2))) inv' (ga ws (regfile state1 ch') mem1 mem2) hd :: (==) Packet p1 p2 = cong Data Packet (snd Channel Data p1) (snd Channel Data p2) (pair Channel Data ch') (cong (Pair Data RegFile) Data (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile state1 ch') mem1)) (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile state2 ch') mem2)) (fst Data RegFile) go) inv'' :: Invariant state1' state2' ch = subst RegFile (regfile (Pair@_ mem1 regs1) ch') (regfile (Pair@_ mem2 regs2) ch') (\(h'::RegFile) -> (==) RegFile (regfile state1' ch) (fm.lookup RegFile (fm.update RegFile ch' (snd Data RegFile (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws h' mem2))) regs2) ch)) inv' (subst (Pair Data RegFile) (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile (Pair@_ mem1 regs1) ch') mem1)) (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile (Pair@_ mem1 regs1) ch') mem2)) (\(h'::Pair Data RegFile) -> (==) RegFile (regfile state1' ch) (fm.lookup RegFile (fm.update RegFile ch' (snd Data RegFile h') regs2) ch)) (ga ws (regfile state1 ch') mem1 mem2) (fmProp RegFile ch ch' (snd Data RegFile (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile (Pair@_ mem1 regs1) ch') mem1))) regs1 regs2 inv)) in cong2 Packet (List Packet) (List Packet) p1 (pick ch (chip algs state1' ps)) p2 (chip algs state2' (pick ch ps)) (cons Packet) hd (separation algs ch good state1' state2' inv'' ps) otherCh (h::IsTrue (natEq ch' ch) -> Absurdity) :: (==) (List Packet) (pick ch (chip algs state1' ps)) (chip algs state2 (pick ch ps)) = let inv1 :: Invariant state1 state1' ch = fmProp2 RegFile ch ch' (snd Data RegFile (fst (Pair Data RegFile) Memory (doPacket (algs ch') ws (regfile state1 ch') mem1))) regs1 (\(h'::(==) Channel ch ch') -> h (subst Channel ch ch' (\(h0::Channel) -> IsTrue (natEq h0 ch)) h' (natEqRefl ch))) inv1b :: Invariant state1' state1 ch = sym RegFile (regfile (Pair@_ mem1 regs1) ch) (regfile state1' ch) inv1 inv' :: Invariant state1' state2 ch = trans RegFile (regfile state1' ch) (regfile (Pair@_ mem1 regs1) ch) (regfile (Pair@_ mem2 regs2) ch) inv1b inv in separation algs ch good state1' state2 inv' ps in ifPropD (List Packet) (\(h::List Packet) -> (==) (List Packet) (pick ch (chip algs state1 (Cons@_ (Pair@_ ch' ws) ps))) (chip algs state2 h)) (natEq ch' ch) (Cons@_ p (pick ch ps)) (pick ch ps) (\(h::IsTrue (natEq ch' ch)) -> ifTrueProp (List Packet) (natEq 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 (Cons@_ p (pick ch ps)))) h (sameCh h)) (\(h::(h::IsTrue (natEq ch' ch)) -> Absurdity) -> ifFalseProp (List Packet) (natEq 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));};};};} -- Corollary: separation hold (same state on lhs & rhs): separation1 (algs::Algs) (ch::Channel) (good::GoodAlg (algs ch)) (state::ChipState) (ps::List Packet) :: (==) (List Packet) (pick ch (chip algs state ps)) (chip algs state (pick ch ps)) = separation algs ch good state state (refl RegFile (regfile state ch)) ps {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on var "fmProp" hide 1 var "fmProp2" hide 1 #-}