-
Notifications
You must be signed in to change notification settings - Fork 135
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add README and improve folder structure
- Loading branch information
1 parent
09b1b87
commit 96c101f
Showing
6 changed files
with
468 additions
and
412 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
This folder contains a Quint model for the core logic of Cross-Chain Validation (CCV). | ||
|
||
### File structure | ||
The files are as follows: | ||
- ccv.qnt: Contains the type definitions, data structures, functional logic for CCV. | ||
The core of the protocol. | ||
- ccv_statemachine.qnt: Contains the state machine layer for CCV. Very roughly speaking, this could be seen as "e2e tests". | ||
Also contains invariants. | ||
- ccv_test.qnt: Contains unit tests for the functional layer of CCV. | ||
- libararies/*: Libraries that don't belong to CCV, but are used by it. | ||
|
||
### Model details | ||
|
||
To see the data structures used in the model, see the ProtocolState type in ccv.qnt. | ||
|
||
The "public" endpoints of the model are those functions that take as an input the protocol state, and return a Result. | ||
Other functions are for utility. | ||
|
||
The parameters of the protocol are defined as consts in ccv.qnt. | ||
|
Oops, something went wrong.