Failure of verification of liveness properties in examples

[prpr2770]

While attempting to verify the liveness-properties mentioned in the example-files provided in the repository, I found a couple of errors for some of the files, while most files checked OK.

1. Hybrid Reliable Broadcast (Clock synchronization, Widder, Schmid)

   The following temporal property is being proved:
   
       liveness4.ivy: line 254: hrb.correctness
   Traceback (most recent call last):
   File "/home/user/.local/bin/ivy_check", line 11, in <module>
   sys.exit(main())
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 793, in main
   check_module()
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 765, in check_module
   check_isolate()
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 579, in check_isolate
   check_temporals()
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 120, in check_temporals
   subgoals = pc.admit_proposition(prop,proof,subgoals)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_proof.py", line 107, in admit_proposition
   subgoals = self.apply_proof(subgoals,proof)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_proof.py", line 161, in apply_proof
   return self.tactic_tactic(decls,proof)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_proof.py", line 169, in tactic_tactic
   return tactic(self,decls,proof)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_l2s.py", line 559, in l2s_tactic
   assert len(named_binders['l2s_g']) == len(named_binders['_old_l2s_g'])
   AssertionError

2. [TLB] (https://github.com/kenmcmil/ivy/blob/master/examples/liveness/tlb.ivy)

   
   The following temporal property is being proved:
   
       liveness4.ivy: line 903: tlb.nonstarvation
   Traceback (most recent call last):
   File "/home/user/.local/bin/ivy_check", line 11, in <module>
   sys.exit(main())
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 793, in main
   check_module()
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 765, in check_module
   check_isolate()
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 579, in check_isolate
   check_temporals()
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_check.py", line 120, in check_temporals
   subgoals = pc.admit_proposition(prop,proof,subgoals)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_proof.py", line 107, in admit_proposition
   subgoals = self.apply_proof(subgoals,proof)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_proof.py", line 161, in apply_proof
   return self.tactic_tactic(decls,proof)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_proof.py", line 169, in tactic_tactic
   return tactic(self,decls,proof)
   File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_l2s.py", line 559, in l2s_tactic
   assert len(named_binders['l2s_g']) == len(named_binders['_old_l2s_g'])
   AssertionError

3. [Test Liveness 2] (https://raw.githubusercontent.com/microsoft/ivy/9f3c7ecc0b2383129fdd0953e10890d98d09a82d/test/test_liveness2.ivy)

... (internal) idle Test_Liveness.ivy: line 294: ticket_protocol.invar68 ... FAIL Test_Liveness.ivy: line 306: ticket_protocol.invar69 ... FAIL ...

The following program assertions are treated as guarantees:
    in action idle when called from the environment,the environment:
        Test_Liveness.ivy: line 158: guarantee ... FAIL

error: failed checks: 3

4. [Test Liveness 1](https://raw.githubusercontent.com/microsoft/ivy/9f3c7ecc0b2383129fdd0953e10890d98d09a82d/test/test_liveness.ivy)

Test_Liveness.ivy(201): error: token 'property': syntax error

5. [Leader Election](https://raw.githubusercontent.com/microsoft/ivy/9f3c7ecc0b2383129fdd0953e10890d98d09a82d/doc/examples/leader_tutorial_liveness.ivy)

Test_Liveness.ivy(96): error: token 'call': syntax error

6. [Liveness 1](https://raw.githubusercontent.com/microsoft/ivy/9f3c7ecc0b2383129fdd0953e10890d98d09a82d/test/liveness1.ivy)

Isolate this:

The following properties are to be checked:

The following action implementations are present:
    Test_Liveness.ivy: line 10: implementation of a

The following initializers are present:
    Test_Liveness.ivy: line 5: init[after1]

Any assertions in initializers must be checked ... PASS

The following temporal property is being proved:

    Test_Liveness.ivy: line 13: prop2

The inductive invariant consists of the following conjectures:
    Test_Liveness.ivy: line 16: inv1

The following action implementations are present:
    Test_Liveness.ivy: line 10: implementation of a

The following initializers are present:
    Noneinit

Initialization must establish the invariant
    Test_Liveness.ivy: line 16: inv1 ... PASS

Any assertions in initializers must be checked ... PASS

The following set of external actions must preserve the invariant:
    (internal) ext:a
        Test_Liveness.ivy: line 16: inv1 ... PASS
    (internal) idle
        Test_Liveness.ivy: line 16: inv1 ... PASS

The following program assertions are treated as assumptions:
    in action idle when called from the environment:
        Test_Liveness.ivy: line 13: assumption
        Test_Liveness.ivy: line 13: assumption
        Test_Liveness.ivy: line 13: assumption
    in action a when called from the environment:
        Test_Liveness.ivy: line 13: assumption
        Test_Liveness.ivy: line 13: assumption
        Test_Liveness.ivy: line 13: assumption
        Test_Liveness.ivy: line 13: assumption

The following program assertions are treated as guarantees:
    in action idle when called from the environment,the environment:
        Test_Liveness.ivy: line 13: guarantee ... FAIL

error: failed checks: 1

[odedp]

Thanks for raising this! Can you please check which ivy commit you used, and also post the command line used? I just ran these on master and got different input for some files. (https://github.com/kenmcmil/ivy/blob/master/examples/liveness/hybrid_reliable_broadcast_cisa.ivy and https://github.com/kenmcmil/ivy/blob/master/examples/liveness/tlb.ivy worked and passed for me.)

[prpr2770]

I'm sorry, I should've shared that information when I raised the issue. I used the following Ivy version:

$git log -1
commit 271ee38980699115508eb90a0dd01deeb750a94b (HEAD -> master, origin/master, origin/HEAD)
Merge: 1cc3ad0 01e0350
Author: Ken McMillan <kenmcmil@microsoft.com>
Date:   Wed Aug 26 11:39:51 2020 -0700

    merge arith_proofs branch

The command line instruction I used for obtaining the above errors was:

ivy_check <filename.ivy>

[jyao15]

I got the exact same errors on https://github.com/kenmcmil/ivy/blob/master/examples/liveness/hybrid_reliable_broadcast_cisa.ivy and https://github.com/kenmcmil/ivy/blob/master/examples/liveness/tlb.ivy. I installed Ivy via pip install ms-ivy (version 1.7.0).

[nano-o]

I gave it a try on the latest master (83d08ee).

• In examples/liveness, all work except tlb.ivy, on which ivy_check seemingly hangs.
• test/liveness1.ivy and test/liveness2.ivy both have a VC that fails to verify.
• doc/examples/leader_tutorial.ivy works.
• test/test_liveness2.ivy has a VC that fails.
• test/test_liveness.ivy has a syntax error.

If it can be of any use, I'm running Ivy using a Docker container built with this Dockerfile: https://github.com/nano-o/ivy-docker/blob/main/standalone/Dockerfile

[odedp]

On latest master I'm getting the same results as @nano-o except tlb.ivy passes in a few minutes. Maybe it's a different z3 version (I'm using 4.8.10).

I think installing ivy via pip doesn't get you the latest ivy version, but it's pretty easy to install ivy from source (as in the above docker file).

[nano-o]

Could be the Z3 version: I'm using the one that comes as a sub-module in the Ivy repository, which seems to be 4.7.1