* Update supervisor_001_draft.md
If the only node in the *FullNodes* set is the primary, that was just deemed faulty, we can't find honest primary.
* Update supervisor_001_draft.md
* abci: points of clarification ahead of v0.1.0
* lint++
* typo
* lint++
* double word score
* grammar
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* Update spec/abci/abci.md
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* pr feedback
* wip
* update non-zero status code docs
* fix event description
* update CheckTx description
Co-authored-by: M. J. Fromberger <fromberger@interchain.io>
* add parameters to byzantine send action
* make net not trusted
it's not necessary since for proofs Ivy will assume that the environment
does not break action preconditions
* use require instead of assume
it seems that assume is not checked when other isolates call!
* add comment
* add comment
* run with random seed
* make domain model extractable to C++
* substitute require for assume
assumes in an action are not checked when the action is called! I.e.
they place no requirement on the caller; we're just assuming that the
caller is going to do the right thing. This wasn't very important here
but it leade to a minor inconsistency slipping through.
* make the net isolate not trusted
there was no need for it
* add tendermint_test.ivy
contains a simple test scenario that show that the specification is no
vacuuous
* update comment
* add comments
* throw if trying to parse nset value in the repl
* add comment
* minor refactoring
* Avoid quantifier alternation cycle
The problematic quantifier alternation cycle arose because the
definition of accountability_violation was unfolded.
This commit also restructures the induction proof for clarity.
* add count_lines.sh
* fix typo and add forgotten complete=fo in comment
Co-authored-by: Giuliano <giuliano@eic-61-11.galois.com>
* ABCI++ RFC
This commit adds an RFC for ABCI++, which is a collection of three new phases of communication between the consensus engine and the application.
Co-authored-by: Sunny Aggarwal <sunnya97@protonmail.ch>
* Fix bugs pointed out by @liamsi
* Update rfc/004-abci++.md
Co-authored-by: Federico Kunze <31522760+fedekunze@users.noreply.github.com>
* Fix markdown lints
* Update rfc/004-abci++.md
Co-authored-by: Ismail Khoffi <Ismail.Khoffi@gmail.com>
* Update rfc/004-abci++.md
Co-authored-by: Tess Rinearson <tess.rinearson@gmail.com>
* Update rfc/004-abci++.md
Co-authored-by: Tess Rinearson <tess.rinearson@gmail.com>
* Add information about the rename in the context section
* Bold RFC
* Add example for self-authenticating vote data
* More exposition of the term IPC
* Update pros / negatives
* Fix sentence fragment
* Add desc for no-ops
Co-authored-by: Sunny Aggarwal <sunnya97@protonmail.ch>
Co-authored-by: Federico Kunze <31522760+fedekunze@users.noreply.github.com>
Co-authored-by: Ismail Khoffi <Ismail.Khoffi@gmail.com>
Co-authored-by: Tess Rinearson <tess.rinearson@gmail.com>
