tendermint

291 MiB

Tree: 98c122f471

Author	SHA1	Message	Date
Giuliano	24222c5855	Add C++ code generation and test scenario (#310 ) * 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	4 years ago
Sam Kleinman	048f6a32f9	lint: fix lint errors (#301 )	4 years ago
Giuliano	292828a01b	A few improvements to the Ivy proof (#288 ) * 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>	4 years ago
Giuliano	66e9106b4d	add Ivy proofs (#210 ) * add Ivy proofs * fix docker-compose command	4 years ago

4 Commits (98c122f4718adccfae6cf78da92eeefcd493b74f)