Proof of the separation property

• The chip model is expressed in Haskell.
• Property assertions are expressed in P-logic embedded in the Haskell code.
• The Programatica tools allow Haskell + P-logic to be translated into the language used by the proof assistant Alfa.
• The proofs were constructed in Alfa and recorded in certificates attached to the P-logic assertion in the Haskell code.
• We can currently only handle total functions over finite data structures with this approach. Fortunately, the Haskell code for the chip model falls in this category.