runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

Migrate cross-validation test harness to reference `.tzt` test runner #49

Open sskeirik opened 4 years ago

sskeirik commented 4 years ago

In this merge request (https://gitlab.com/metastatedev/tezos/-/merge_requests/83), the reference Tezos client gains the ability to run our .tzt tests. Unfortunately, due to the fact that the Tezos protocol is amended by vote, and that this merge request affects the protocol itself, it will take several months for this feature to stabilize and then be voted into master. In the meantime, we can check out this branch referenced in the merge request above for our testing purposes instead of master.

EDIT: If I understood correctly, this feature should be usable with the --mode mockup flag referenced in issue #50. This is worth double-checking on that branch.

ehildenb commented 4 years ago

@sskeirik we should not depend on an unmerged branch of Tezos. That will almost certainly cause sudden breakages in our builds down the road.

Until it's merged into master we should continue with our workarounds.

sskeirik commented 4 years ago

@ehildenb We can always save the current setup in some branch and resurrect it later. Additionally, due to the way that the Tezos protocol is updated, change happens very slowly --- I don't think we've ever had breakages when updating before. Lastly, the current test harness isn't very portable or maintainable, so rewriting it from scratch in the future if we had to might be an improvement.

EDIT: Although it is true that we never depended on anything but master before --- and typically stability guarantees are only made for master.

ehildenb commented 4 years ago

The point is that if we depend on a branch that is not merged into master, two problems may occur:

I'm sorry, but you simply must not depend on a non-master branch.

ehildenb commented 4 years ago

Keeping the shims in place for now is fine. It works, and we can wait for their approval process to filter through to update it.

rafoo commented 4 years ago

I understand the danger of depending on an unmerged branch, maybe a compromise is to wait for it to be merged on the proto-proposal branch of the https://gitlab.com/metastatedev/tezos repository. Being merged there means that the code has undergone several reviews and (unless a critical vulnerability is found) will be part of the next protocol amendment proposed by Metastate (aka. Cryptium Labs) and Nomadic Labs. The proto-proposal branch is regularly rebased on master so you don't have to wait for long before having the latest master features.

ehildenb commented 4 years ago

@rafoo that doesn't work, simply because you said that it is rebased on master, which means that our upstream will disappear. If it was merged into master instead, the commit history would be preserved.

The scenario I want to avoid (simply because it has cost of weeks of dev time in the past at RV, and it's silly money wasted) is this:

I am adamant about this, we cannot depend on a branch that will have its history rewritten. If you have another branch which you never force push to (only merges and fast-forwards) and it's a staging branch for master, we can depend on that branch. We have had problems with this too many times.

To give a blockchain analogy, depending on a branch that has its history rewritten is akin to mining on a short fork of the blockchain: maybe you can spend your money you earn for a little bit, but when history gets rewritten it will all disappear and you'll have to get all the transactions you made on that fork into the longer fork of the chain, which takes even more time.

ehildenb commented 4 years ago

There are two solutions which would work that I can think of.

This sounds really pedantic, but we really have lost lots of time because of exactly this issue where we depended on versions of software that disappeared in the past. If most of the updates go smoothly, but only 3-4 of them suddenly take 2 weeks each time to make our tool work with the new version, it can turn a 6 month engagement into an 8 month engagement, which makes everyone unhappy.

rafoo commented 4 years ago

@ehildenb : I understand your concerns, thank you for having taken the time to detail the problem.

TBH I doubt we will change our git workflow ; there are other advantages to use rebases that we probably aren't ready to lose. Tagging proto-proposal from time to time makes sense IMO.

@sskeirik : can you please point me to the test we are talking about? It might make sense to simply move them there.

Another option that I quickly mentioned during last meeting would be to use Mi-Cho-Coq once the TZT MR is finished and merged on master.

ehildenb commented 4 years ago

The git tags solution is nicest IMO if we need the proto-proposal version of the tool. Then you'll have a record of the old proto-proposals too, eg vX.Y.Z-rc tags for recording what went into each update.