Fix voting example

[DustinWehr]

What's your issue about?

The problem is described here https://github.com/ethereum/viper/pull/302#issuecomment-326341764

How can it be fixed?

I'm happy to help if @DavidKnott and @fubuloubu don't have the time.

3 options, all of which still need some scrutiny:

• @fubuloubu sketched a fix in two comments: this change alone seemed like it'd work, but the resulting program is more restricted than the Solidity example. The second comment is about addressing that restriction.
• I wrote one that differs more from @DavidKnott's.
• More complex version of the previous, including a cycle breaking capability.

[fubuloubu]

I think in general the examples don't need to be fully realized, production code. Their point is more to show how much simpler and clearer Viper syntax is as examples on how to get started.

That being said, replicating some Solidity examples is important as a comparison.

I didn't get a chance to look too deeply at what you did, but keep that in mind.

[DavidKnott]

@DustinWehr It'd be great if you made a PR. I second what @fubuloubu mentioned, it's a lot more important for people to understand examples and the viper syntax used then to have them be fully functionally. Maybe you could make a pr with 2 voting examples a simple one and your more complex / feature complete one?

[DavidKnott]

@DustinWehr Are you working on this, if not I can do it this week.

[DustinWehr]

@DavidKnott I can submit a PR in the morning. I wrote a version based on our discussion with @fubuloubu that should pass all the existing tests, and has all the essential features of the Solidity version. The only difference is that it moves the weight forwarding to a separate function forward_weight, which gets called by delegate once, but needs to get called more than once in the (presumably-rare) case of a delegation chain of length more than 10.

I do have a question first. It is unclear to me when one should use assertions. These are several of the distinct uses: (1) Assert something that is always true if the contract code is correct. In my experience this is the usual intent of an assert keyword, at least in PLs that give you the option to turn them off. (2) Check something that is meant to be checked by the off-chain code, but that isn't actually problematic for correctness if it's false. As @fubuloubu pointed out, delegation cycles are an example of this, since a delegation cycle just spoils all those votes. (3) Prevent calls to functions that are not allowed by the contract, reverting all changes if any were made before the discovery.

There should be at least a distinct alias of assert for each of those uses. Otherwise you're preventing easy opportunities for the programmer to formally specify their intention.

But, I humbly suggest that (3) should have different semantics from (1) and (2).

(1) Use assert only for this. These are always removed in production (main network). (2) Something like should, usage_assert, weak_assert, client_assert, offchain_assert? I dunno, I suck at naming. Anyway, the semantics is the same as (1), so these are also always removed in production. (3) Use ensure. These are never removed in production, since the proper functioning of the code depends on them.

[DustinWehr]

I never did get running tests working on my system... Can you run them (the existing tests) on this before I submit a PR? https://gist.github.com/DustinWehr/98c9310afab793588aa8e031f1d79aec

[fubuloubu]

@DustinWehr I think you need a clearer example of what you're suggesting for assert, probably in a different issue. I sort of like the require/assert thing in solidity (like maybe 80% like it lol). In solidity, require means front end assumptions about inputs, and assert means the backend of calculations executed correctly. Your suggestion of should actually sounds like a great candidate for what you are describing in (1), but I don't really follow exactly what you mean there (e.g. should describes a scenario that can potentially be optimized away assuming formal correctness is verified for that contract).

In my (old) industry, we wrote requirements documents that had different types of requirements with different assumptions on implementation. shall was different than will or should. It's interesting to think of them as all essentially assert under the hood, but with different semantic contexts designed to help the auditor/reader understand the assumptions present.

[DustinWehr]

Oh! How embarrassing... Thanks @fubuloubu. As you must have guessed, Viper is my first smart contract language; otherwise I would not have suggested inconsistent names. I'll open a more-thorough issue about it later.

A quick response to your comments though: So require is (2) and assert is (3). You understood what I meant by (1) (now should): should A means you believe that whenever the computation reaches that statement, A evaluates to true (and I forgot to mention A is side effect free). So it's something that should be provable. The compiler would ignore should statements, but a Viper interpreter (e.g. the python test runner) would stop immediately if the statement evaluates to false.

[fubuloubu]

Your suggestion for should sort of sounds like a Theorem Prover. Like, you suggest putting should A statements in your code to assert some invariant that should never be false if the system is designed correctly?

Typically, theorem provers work as having a separate model representing your intention as it's own system (aka a collection of requirements called "theorems" about your system's properties). You then take that system and formalize it to create a set of test cases showing all possible scenarios describing your system. Those test cases are run against the actual system to prove formal correctness of your system during actual operation (in this case, EVM Bytecode actually running on the EVM).

This is all part of the realm of Formal Verification, which is a very interesting subject (I took a course my last year in grad school). Ethereum/Smart Contract systems are a great application for this field of academic study both because it is so important to get the system to be provably correct, and because the smart contracts we create are actually pretty high-level and lend themselves well to being theorized against using these techniques. @pirapira is very active in this space. He has some musings you can read about here.

It would be an awesome feature for Viper to implement something in this regard, and probably speed along it's adoption (over Solidity). A few theorem provers out there can target Python (check out Z3 Prover), and since we're still operating on a subset of Python syntax (@DavidKnott, one reason to KEEP the Python AST), perhaps there might be an easy way to integrate this into the Viper compiler. It certainly is a big ask, but I think it is a big reward item.

I hope that isn't TMI lol

[DustinWehr]

Not TMI. Formal Verification is a major part of my work with Legalese. Our computational legal contracts will compile to EVM bytecode, probably via Viper. We expect to be in contact with Yoichi in the near future (if Virgil isn't already).

[fubuloubu]

@DustinWehr Very cool! Do you know/have experience with FV for Python? That post just got me thinking a little bit, and I think the current syntax of Viper can probably support any tool that was developed for Python without a large amount of modifications.

PM me on gitter if you want to talk more about it!

[fubuloubu]

P.S. I love the faux newspaper aesthetic to Legalese's website!

[pirapira]

Meaow, meaow.

[DavidKnott]

I'm looking into formal verification now, as @fubuloubu mentioned because we're using python syntax there are a bunch of cool tools at our fingertips :)

[fubuloubu]

Actually less tools then I thought, but there are some. I was thinking about a Bounded Model Checker

[DustinWehr]

This sounds like the right path as far as programmer interface: https://www.reddit.com/r/ethdev/comments/737jik/anyone_experince_to_use_formal_specifications_eg/dnor1tp/?context=3 It is consistent with #397

The lack of loops and recursion in Viper should be a huge benefit for FV.

[DustinWehr]

Ok with you guys if I change the meaning of the weight field, so it satisfies this invariant? (sum of weight over all voters) + (sum of vote_count over all proposals) = voter_count

This requires changing one of the test cases. The Solidity example doesn't do this (i.e. never sets a voter's weight to 0 after counting it), because it's not necessary, but I think that's kind of counterintuitive.

Also, a question: is the address 0x0000000000000000000000000000000000000000 falsey, and is it the only falsey address?

[fubuloubu]

Not sure I quite follow, but the invariant should be like "the overall amount of votes available (whether used or not) stays the same"

It would be cool as a way to define your own generated test cases in the source. Hmm....

[DavidKnott]

Closing as the voting example has been fixed, thanks again @DustinWehr