Agda to QuickCheck demonstration (#86)

* start on small example of connecting a quickcheck model and agda spec
* initial WIP on a Haskell-side model to use as the target
to aim for from Agda
* working quickCheck model of the super simple example protocol
* Some thoughts about what happens when you add negative testing
* some thinking and refining the protocol
* trying to make the model match the implementation
* modify the target model to align with outcome of meeting + stop using
negative actions as these are only going to complicate things
* a bit more cleanup
* simplify the model
* started on agda spec for the mini protocol
* some form completed agda spec for the toy protocol
* hook up agda2hs and get halfway on a soundness proof
* finished soundness proof and made it nice(ish)
* add dishonest actions to tests (not yet to soundness proof)
* some proofs about dishonest actions
* finished soundness proof for dishonest actions
* some thoughts on completeness
* some proof cleanup and soundness for sequences of actions
* Rename modules, add Makefile and start on documentation
* Test suite
* Run fourmolu on all the Haskell code
* Some cleanup of the agda code
* Some embryo of contents in Overview.lagda.md
* More documentation
* Remove bound on q-d

---------

Co-authored-by: Maximilian Algehed <m.algehed@gmail.com>
Co-authored-by: Arnaud Bailly <arnaud.bailly@iohk.io>

Author: 3 people

cabal.project

@@ -11,14 +11,15 @@ repository cardano-haskell-packages
 
 index-state: 2024-01-05T13:49:07Z
 index-state:
-  , hackage.haskell.org      2023-12-15T16:32:49Z
+  , hackage.haskell.org      2024-03-14T00:00:00Z
   , cardano-haskell-packages 2023-12-15T14:50:31Z
 
 packages:
   peras-hs
   peras-iosim
   peras-quickcheck
   peras-delta-q
+  test-demo
 
 tests: True
 test-show-details: direct

test-demo/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for test-demo
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

test-demo/LICENSE

@@ -0,0 +1,20 @@
+Copyright (c) 2024 Maximilian Algehed
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

test-demo/Makefile

@@ -0,0 +1,10 @@
+
+default : typecheck
+
+typecheck :
+	agda2hs src/Overview.lagda.md
+	@rm -f src/Overview.hs
+	fourmolu -i src/*.hs
+
+test : typecheck
+	cabal test

test-demo/src/CommonTypes.agda

@@ -0,0 +1,56 @@
+
+module CommonTypes where
+
+open import Haskell.Prelude
+open import Data.Nat.Base
+open import Relation.Binary.PropositionalEquality
+
+open import ProofPrelude
+
+{-# FOREIGN AGDA2HS import GHC.Generics #-}
+
+data Party : Set where
+  Alice Bob : Party
+
+{-# COMPILE AGDA2HS Party deriving (Eq, Ord, Show, Generic) #-}
+
+BlockIndex = ℕ
+Slot       = ℕ
+
+{-# FOREIGN AGDA2HS
+type BlockIndex = Integer
+type Slot       = Integer
+#-}
+
+record Block : Set where
+  constructor Blk
+  field
+    blockIndex : BlockIndex
+
+open Block public
+
+{-# COMPILE AGDA2HS Block deriving (Eq, Ord, Show, Generic) #-}
+
+instance
+  EqParty : Eq Party
+  EqParty ._==_ Alice Alice = True
+  EqParty ._==_ Alice Bob   = False
+  EqParty ._==_ Bob   Alice = False
+  EqParty ._==_ Bob   Bob   = True
+
+  EqBlock : Eq Block
+  EqBlock ._==_ (Blk i) (Blk j) = i == j
+
+eqParty-sound : ∀ {p q : Party} → (p == q) ≡ True → p ≡ q
+eqParty-sound {Alice} {Alice} _ = refl
+eqParty-sound {Bob}   {Bob}   _ = refl
+
+eqParty-complete : {p q : Party} → (p == q) ≡ False → p ≢ q
+eqParty-complete {Alice} {Bob}   h ()
+eqParty-complete {Bob}   {Alice} h ()
+
+eqBlock-sound : ∀ {b b₁ : Block} → (b == b₁) ≡ True → b ≡ b₁
+eqBlock-sound {Blk i} {Blk j} h = cong Blk (eqℕ-sound h)
+
+eqBlock-complete : ∀ {b b₁ : Block} → (b == b₁) ≡ False → b ≢ b₁
+eqBlock-complete {Blk i} isF refl = eqℕ-complete {i} isF refl

test-demo/src/CommonTypes.hs

@@ -0,0 +1,14 @@
+module CommonTypes where
+
+import GHC.Generics
+
+data Party
+  = Alice
+  | Bob
+  deriving (Eq, Ord, Show, Generic)
+
+type BlockIndex = Integer
+type Slot = Integer
+
+data Block = Blk {blockIndex :: BlockIndex}
+  deriving (Eq, Ord, Show, Generic)

test-demo/src/FormalSpec.agda

@@ -0,0 +1,194 @@
+
+-- The formal Agda specification with all the fancy types.
+
+module FormalSpec where
+
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.List.Base
+open import Data.Product.Base
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import Function
+
+open import CommonTypes
+
+-- Super simple protocol:
+--  - The hosts take turns round robin to produce blocks.
+--  - `blockIndex` is incremented with each block on the chain.
+--  - If a node misses its window the other node should produce the missed block in its slot
+--    instead.
+-- Network model: π-calculus style instant delivery
+
+record LocalState : Set where
+  constructor _,_
+  field
+    lastBlock     : Block
+    lastBlockSlot : Slot
+
+open LocalState public
+
+record State : Set where
+  constructor ⟦_,_,_⟧
+  field
+    clock        : Slot
+    aliceState   : LocalState
+    bobState     : LocalState
+
+open State public
+
+initLocalState : LocalState
+initLocalState = Blk 0 , 0
+
+initState : State
+initState = ⟦ 0 , initLocalState , initLocalState ⟧
+
+-- State manipulation
+
+getLocalState : Party → State → LocalState
+getLocalState Alice = aliceState
+getLocalState Bob   = bobState
+
+modifyLocalState : Party → (LocalState → LocalState) → State → State
+modifyLocalState Alice f ⟦ t , as , bs ⟧ = ⟦ t , f as , bs ⟧
+modifyLocalState Bob   f ⟦ t , as , bs ⟧ = ⟦ t , as , f bs ⟧
+
+setLocalState : Party → LocalState → State → State
+setLocalState p ls = modifyLocalState p λ _ → ls
+
+-- Honesty models. Encodes who is allowed to perform adversarial actions.
+
+data Honesty : Set where
+  happyPath : Honesty
+  badAlice  : Honesty
+  badBob    : Honesty
+
+-- Certificate that the given party is allowed to do bad things.
+data Dishonest : Honesty → Party → Set where
+  badAlice : Dishonest badAlice Alice
+  badBob   : Dishonest badBob   Bob
+
+variable
+  s s₀ s₁ s₂ s₃ s₄ : State
+  ls ls₀ ls₁       : LocalState
+  p q              : Party
+  b b₁             : Block
+  i j              : BlockIndex
+  t t₁ now         : Slot
+  h                : Honesty
+
+-- Alice has even slots, Bob has odd slots.
+data SlotOf (t : Slot) : Party → Set where
+  AliceSlot : t % 2 ≡ 0 → SlotOf t Alice
+  BobSlot   : t % 2 ≡ 1 → SlotOf t Bob
+
+-- `ValidBlock now ls p b`: At time `now` is it valid for a party `p`
+-- to send a block `b` from the point of view of a node with local
+-- state `ls`.
+data ValidBlock : Slot → LocalState → Party → Block → Set where
+  valid : t < now
+        → SlotOf now p
+        → ValidBlock now (Blk i , t) p (Blk (suc i))
+
+-- Local state update on receive
+data _⊢_[_,_]?_ : Slot → LocalState → Party → Block → LocalState → Set where
+  correctBlock : ValidBlock now ls p b
+               → now ⊢ ls [ p , b ]? (b , now)
+  wrongBlock   : ¬ ValidBlock now ls p b
+               → now ⊢ ls [ p , b ]? ls
+
+-- Global state update on receive
+data _[_,_↦_]?_ : State → Party → Block → Party → State → Set where
+  receive : clock s ⊢ getLocalState q s [ p , b ]? ls →
+            s [ p , b ↦ q ]? setLocalState q ls s
+
+-- Local state update on send
+data _,_,_⊢_[_↦_]!_ : Honesty → Slot → Party → LocalState → Block → Party → LocalState → Set where
+  correctBlock   : ValidBlock now ls p b
+                 → h , now , p ⊢ ls [ b ↦ q ]! (b , now)
+  dishonestBlock : Dishonest h p
+                 → h , now , p ⊢ ls [ b ↦ q ]! ls
+
+-- Global state update on send
+data _⊢_[_,_↦_]!_ : Honesty → State → Party → Block → Party → State → Set where
+  send : ∀ q b → h , clock s , p ⊢ getLocalState p s [ b ↦ q ]! ls
+               → p ≢ q
+               → h ⊢ s [ p , b ↦ q ]! setLocalState p ls s
+
+-- The top-level small-step semantics
+data _⊢_↝_ : Honesty → State → State → Set where
+
+  -- π-calculus-style instant message delivery
+  deliver : h ⊢ s₀ [ p , b ↦ q ]! s₁
+          →     s₁ [ p , b ↦ q ]? s₂
+          → h ⊢ s₀ ↝ s₂
+
+  -- We can only tick if the party whose slot it is has produced (or
+  -- pretends to have produced) their block.
+  tick : SlotOf (clock s) p
+       → lastBlockSlot (getLocalState p s) ≡ clock s
+       → h ⊢ s ↝ record s { clock = suc (clock s) }
+
+  -- A dishonest party can update their local state to whatever they want.
+  trickery : Dishonest h p → ∀ ls → h ⊢ s ↝ setLocalState p ls s
+
+-- Standard reflexive-transitive closure.
+data _⊢_↝*_ : Honesty → State → State → Set where
+  []  : h ⊢ s ↝* s
+  _∷_ : h ⊢ s₀ ↝ s₁ → h ⊢ s₁ ↝* s₂ → h ⊢ s₀ ↝* s₂
+
+infixr 5 _<>_
+_<>_ : h ⊢ s₀ ↝* s₁ → h ⊢ s₁ ↝* s₂ → h ⊢ s₀ ↝* s₂
+[]       <> tr  = tr
+(r ∷ tr) <> tr₁ = r ∷ tr <> tr₁
+
+-- Which blocks does Alice produce in a given trace?
+aliceBlocks : h ⊢ s₀ ↝* s₁ → List (Slot × Block)
+aliceBlocks [] = []
+aliceBlocks {s₀ = s₀} (deliver {p = Alice} {b} _ _ ∷ tr) = (clock s₀ , b) ∷ aliceBlocks tr
+aliceBlocks (deliver _ _  ∷ tr) = aliceBlocks tr
+aliceBlocks (trickery _ _ ∷ tr) = aliceBlocks tr
+aliceBlocks (tick _ _     ∷ tr) = aliceBlocks tr
+
+-- Some proofs
+
+liftHonesty : happyPath ⊢ s ↝ s₁ → h ⊢ s ↝ s₁
+liftHonesty (deliver (send q b (correctBlock v) !q) r) = deliver (send q b (correctBlock v) !q) r
+liftHonesty (tick sl sent) = tick sl sent
+
+liftHonesty* : happyPath ⊢ s ↝* s₁ → h ⊢ s ↝* s₁
+liftHonesty* []       = []
+liftHonesty* (r ∷ tr) = liftHonesty r ∷ liftHonesty* tr
+
+sameAliceBlocks : (tr : happyPath ⊢ s ↝* s₁) → aliceBlocks tr ≡ aliceBlocks (liftHonesty* {h = h} tr)
+sameAliceBlocks [] = refl
+sameAliceBlocks {h = h} (deliver {p = Alice} {b} (send _ _ (correctBlock _) _) _ ∷ tr)
+  rewrite sameAliceBlocks {h = h} tr = refl
+sameAliceBlocks (deliver {p = Bob} (send _ _ (correctBlock _) _) _ ∷ tr) = sameAliceBlocks tr
+sameAliceBlocks (tick _ _ ∷ tr) = sameAliceBlocks tr
+
+appendAliceBlocks : (tr : h ⊢ s₀ ↝* s₁) (tr₁ : h ⊢ s₁ ↝* s₂) → aliceBlocks (tr <> tr₁) ≡ aliceBlocks tr ++ aliceBlocks tr₁
+appendAliceBlocks []       tr₁ = refl
+appendAliceBlocks (deliver {p = Alice} _ _ ∷ tr) tr₁ rewrite appendAliceBlocks tr tr₁ = refl
+appendAliceBlocks (deliver {p = Bob  } _ _ ∷ tr) tr₁ = appendAliceBlocks tr tr₁
+appendAliceBlocks (trickery _ _ ∷ tr)            tr₁ = appendAliceBlocks tr tr₁
+appendAliceBlocks (tick _ _ ∷ tr)                tr₁ = appendAliceBlocks tr tr₁
+
+-- Examples
+
+_ : happyPath ⊢ initState ↝* ⟦ 2 , (Blk 2 , 2) , (Blk 2 , 2) ⟧
+_ = tick (AliceSlot refl) refl
+  ∷ deliver (send Alice (Blk 1) (correctBlock (valid ≤-refl (BobSlot refl))) λ())
+            (receive (correctBlock (valid ≤-refl (BobSlot refl))))
+  ∷ tick (BobSlot refl) refl
+  ∷ deliver (send Bob (Blk 2) (correctBlock (valid ≤-refl (AliceSlot refl))) λ())
+            (receive (correctBlock (valid ≤-refl (AliceSlot refl))))
+  ∷ []
+
+_ : badBob ⊢ initState ↝* ⟦ 2 , (Blk 1 , 2) , (Blk 1 , 2) ⟧
+_ = tick (AliceSlot refl) refl
+  ∷ trickery badBob (Blk 0 , 1)   -- Bob pretends to have sent a message (bumping lastBlkSlot)
+  ∷ tick (BobSlot refl) refl
+  ∷ deliver (send Bob (Blk 1) (correctBlock (valid (s≤s z≤n) (AliceSlot refl))) λ())
+            (receive (correctBlock (valid ≤-refl (AliceSlot refl))))
+  ∷ []