Fix spec and add spec for supra governance

[axiongsupra]

No description provided.

[sjoshisupra]

@axiongsupra not sure why this aborts_if is required and what purpose does it serve.

[axiongsupra]

This is for checking the whether time already started. This is required if we have call to timestamp::now_seconds()

[sjoshisupra]

This property only ensures that time is recorded. Other properties we should aim at adding are

• vote by the voter is recorded (if not already voted)
• vote by the voter is recorded (if vote is flipped)
• total yes/no votes should tally (increase/decrease appropriately)

[axiongsupra]

Added in e65045b

[sjoshisupra]

Not sure I understand the role of these. @axiongsupra

[axiongsupra]

This looks strange to me. I will take a look and submit a patch.

[sjoshisupra]

What is the role of this?

[axiongsupra]

This is for checking the whether time already started. This is required if we have call to timestamp::now_seconds()

[axiongsupra]

The proofs are still valid.

[axiongsupra]

The spec are still valid

[INFO] 2.222s build, 2.298s trafo, 0.493s gen, 165.846s verify, total 170.858s
{
  "Result": "Success"
}

[axiongsupra]

Resolved conflict.

Aptos move prover verify this successfully.

[INFO] 686 verification conditions
[INFO] running solver
[INFO] 109.49s build, 2.64s trafo, 0.62s gen, 285.81s verify, total 398.56s
{
  "Result": "Success"
}

However, supra move prover end with the following error:

Error: General: {
  "Error": "Move Prover failed: [internal] boogie exited with compilation errors:\n/Users/supra/aptos-core/aptos-move/framework/supra-framework/boogie.bpl(103321,288): Error: cannot refer to a global variable in this context: #0_info\n/Users/supra/aptos-core/aptos-move/framework/supra-framework/boogie.bpl(103321,300): Error: cannot refer to a global variable in this context: #0_info\n/Users/supra/aptos-core/aptos-move/framework/supra-framework/boogie.bpl(103321,312): Error: cannot refer to a global variable in this context: #0_info\n/Users/supra/aptos-core/aptos-move/framework/supra-framework/boogie.bpl(103321,462): Error: cannot refer to a global variable in this context: #0_info\n/Users/supra/aptos-core/aptos-move/framework/supra-framework/boogie.bpl(103321,474): Error: cannot refer to a global variable in this context: #0_info\n/Users/supra/aptos-core/aptos-move/framework/supra-framework/boogie.bpl(103321,486): Error: cannot refer to a global variable in this context: #0_info\n6 name resolution errors detected in /Users/supra/aptos-core/aptos-move/framework/supra-framework/boogie.bpl\n"
}