mirror of
https://github.com/tendermint/tendermint.git
synced 2026-05-29 10:30:20 +00:00
24222c5855
* 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
40 lines
885 B
Bash
Executable File
40 lines
885 B
Bash
Executable File
#!/bin/bash
|
|
|
|
# returns non-zero error code if any proof fails
|
|
|
|
success=0
|
|
log_dir=$(cat /dev/urandom | tr -cd 'a-f0-9' | head -c 6)
|
|
cmd="ivy_check seed=$RANDOM"
|
|
mkdir -p output/$log_dir
|
|
|
|
echo "Checking classic safety:"
|
|
res=$($cmd classic_safety.ivy | tee "output/$log_dir/classic_safety.txt" | tail -n 1)
|
|
if [ "$res" = "OK" ]; then
|
|
echo "OK"
|
|
else
|
|
echo "FAILED"
|
|
success=1
|
|
fi
|
|
|
|
echo "Checking accountable safety 1:"
|
|
res=$($cmd accountable_safety_1.ivy | tee "output/$log_dir/accountable_safety_1.txt" | tail -n 1)
|
|
if [ "$res" = "OK" ]; then
|
|
echo "OK"
|
|
else
|
|
echo "FAILED"
|
|
success=1
|
|
fi
|
|
|
|
echo "Checking accountable safety 2:"
|
|
res=$($cmd complete=fo accountable_safety_2.ivy | tee "output/$log_dir/accountable_safety_2.txt" | tail -n 1)
|
|
if [ "$res" = "OK" ]; then
|
|
echo "OK"
|
|
else
|
|
echo "FAILED"
|
|
success=1
|
|
fi
|
|
|
|
echo
|
|
echo "See ivy_check output in the output/ folder"
|
|
exit $success
|