Revert "Revert "Merge branch 'ph/quint-model-v2' of https://github.co…

…m/cosmos/interchain-security into ph/quint-model-v2"" This reverts commit 3afd300.
cosmos · Sep 18, 2023 · cdebe89 · cdebe89
1 parent 3afd300
commit cdebe89
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -1,10 +1,16 @@
+-*- mode: Bluespec; -*-
 module ccv {
     import extraSpells.* from "./extraSpells"
 
     // Things that are not modelled:
     // * Reward distribution
     // * Starting/Stopping chains during execution
     // * Slashes
+
+    // Things that explicitly are modelled:
+    // * Validator set changes are propagated from provider to consumers
+    // * VSC packets mature
+    // * Consumers can be forcefully dropped due to timeouts, or stop on their own volition
 
     // TYPE DEFINITIONS
     type Node = str
@@ -610,4 +616,4 @@ module ccv {
     }
 
 
-}
+}
diff --git a/tests/difference/core/quint_model/extraSpells.qnt b/tests/difference/core/quint_model/extraSpells.qnt
@@ -1,3 +1,5 @@
+-*- mode: Bluespec; -*-
+// This module is just a library with utility functions (sometimes called spells in Quint).
 module extraSpells {
 
   pure def prepend(__list: List[a], __elem: a): List[a] = {
@@ -188,4 +190,4 @@ module extraSpells {
         __set.union(Set(elem))
     }
 
-}
+}