A Proof of the Chip Model Separation Property in Alfa

• Thomas Hallgren
• Programatica meeting, February 27, 2004

Bottom Line

• A complete formal proof of the Separation Property of the Chip Model
• Proof developed and checked in Alfa
• All definitions are accepted by the termination checker
  • No bottoms in sight!
  • Confidence level is high!

What Chip Model?

• Starting Point: Haskell Chip Model
  • .../programatica/examples/ChannelSeparation/Monadic/
• Hand translation to Alfa
• One simplification of the model

Simplification

No failing algorithms

• The proof instead makes use of the extra assumption that algorithms are "good"
• No runProtected
• The type of onePacket is thus slightly simpler:
  • Original
    • onePacket :: Algs->Packet->StateM ChipState (Maybe Packet)
  • My model
    • onePacket :: Algs->Packet->StateM ChipState Packet
• Motivation: ...

Improved code reuse

One shared abstraction for finite maps

• Haskell model:
  • Memory implements finite maps using functions
  • Regs and Algs use a finite map implementation based on lists
• My Alfa model:
  • A single abstraction for finite maps

Modularity / Abstracting away from irrelevant details

• Finite maps
• Alg
• RegFile, Reg
• Addr, Word, Memory

Abstraction mechanisms

• Parameterized modules
  • Finite maps, RegFile, Word
  • Can plug in different implementations without invalidating the proof
• Marking definitons as abstract
  • Memory, Addr, and related functions
• Deforestation
  • Alg, Code

Parameterizing over finite maps

First attempt

• Corresponds to the following Haskell code:
  • class FiniteMap fm where
    empty :: v -> fm k v
    lookup :: fm k v -> k -> v
    update :: k -> v -> fm k v -> fm k v
• Problem: too general
  • No implementation can be completely polymorphic in the type of keys
• Also a reminder of the problem with type classes for container types in Haskell

Parameterizing over finite maps

Second attempt

• Corresponds to the following Haskell code:
  • class FiniteMap fm k | fm->k where
    empty :: v -> fm v
    lookup :: fm v -> k -> v
    update :: k -> v -> fm v -> fm v
• Problem: solved!
  • Implementations can impose restrictions on the key type:
    • instance Eq k => FiniteMap ((->) k) k where ...

Assumed properties of finite maps

• If two finite maps are equal at one key, they are still equal at that key after an update:
  ∀ fm₁ fm₂ k k' v .
  {lookup fm₁ k} === {lookup fm₂ k} ==>
  {lookup (update k' v fm₁) k}
  === {lookup (update k' v fm₂) k}
• Updating a key doesn't change the values associated with other keys:
  ∀ fm k k' v .
  True {k /= k'} ==>
  {lookup k (update k' v fm)} === {lookup k fm}
• This is elegantly captured as a record type in Alfa (see file FiniteMaps2.alfa)...

Representation of algorithms

My definition of Alg:

• type Alg = Nat -> RegFile -> StateM Memory RegFile
• The first argument is the packet size
• Required properties are stated extensionally

Assumed properties of algorithms

• The result of a good algorithm depends only on the packet it processes and the register file for the relevent channel:
  property GoodAlg alg =
  ∀ ws regf mem1 mem2
  {fst (doPacket alg ws regf mem1)}
  ===
  {fst (doPacket alg ws regf mem2)}
• We are running the state monad starting in two unrelated memories, and observing the result (the returned packet and modified register file)
  • doPacket :: Alg -> Data -> RegFile -> StateM Memory (Data,RegFile)

Other required properties

• RegFile: none
• Reg: none
• Word: none
• Channel: none
• StateM: none (except what you get for free from its implementation)

Types

• type Algs = Channel -> Alg
• type ChipState = (Memory,Regs)
• type Packet = (Channel,Data)
• type Data = [Word]
• type StateM s a = s -> (a,s)
• chip :: Algs -> ChipState -> [Packet] -> StateM ChipState [Packet]
• onePacket :: Algs -> Channel -> Data -> StateM ChipState Packet

Formulation of the Channel Separation property

Consider two circuits:

• one with a filter attatched at the input of a chip,
• one with the filter attatched to the output of a chip.

Formulation of the Channel Separation property

These two circuits produce the same output, provided

• the algorithm for the observed channel is good
• the initial states of two chips are related in an appropriate way
  ∀ algs ch state1 state2 ps .
  GoodAlg (algs ch) ==>
  Invariant state1 state2 ch ==>
  {pick ch (chip algs state1 ps)}
  ===
  {chip algs state2 (pick ch ps)}

Proof of the Channel Separation property

• Proof is by induction over the input packet list
• Proof is effectively by showing that one circuit simulates the other
• Invariant: the states of the two circuits stay related
  • Relation: the register file for the observed channel is the same in both states:
    property Invariant state1 state2 ch =
    {regfile state1 ch} === {regfile state2 ch}
    
    regifle :: ChipState -> Channel -> RegFile
    regfile state ch = lookup (snd state) ch

Outline of the proof

• Base case: ps = []
  • trivial, because LHS = RHS = []
• Induction step: ps = (ch',ws):ps'
  • Two cases
    • ch' == ch : the equation reduces to
      • {p1:pick ch (chip algs state1' ps')}
=== {p2:chip algs state2' (pick ch ps')}
    • ch' /= ch : the equation reduces to
      • {pick ch (chip algs state1' ps')}
=== {chip algs state2 (pick ch ps')}

Alfa Files

• Lines	Words	Chars	File name
  81	357	3202	ChipModel.alfa
  46	171	1244	FiniteMaps2.alfa
  30	123	882	Memories.alfa
  93	375	2316	Monads.alfa
  51	252	1457	State.alfa
  451	1225	22077	ChipModelProps5.alfa
  752	2503	31178	total

• Reminder: Alfa files are rather verbose, due to a lot of explicit type information

Conclusion

• Alfa is more than adequate for this example
• Haskell+Plogic is less appropriate for this kind of modelling (don't need partial functions or infinite data strutures)
• Possible future work:
  • Include runProtected and algorithms that can fail
  • Abstact away from the concrete state monad and make use of explicitly stated monad properties instead.
  • Use the Alfa certificate server and do the proof for the Haskell program
  • Feasibility check: create a concrete instance with good algorithms & associated proofs

The end

Questions?