Replace defn/chan with calls to the channel model

[tchajed]

theory/chan now has simple wrappers around the channel AU specs. The protocols are also stated over the defn/chan definitions, rather then referencing the model directly.

For backwards compatibility, chan_old.v provides the old axioms over the new definitions (probably unsoundly). This is used by all the existing channel proofs. They should be migrated over to the new and more real specs soon-ish.

As currently implemented, channel operations now depend on is_pkg_init channel.

This PR provides a model for select, but the model doesn't do random selection (it always tries in order). It provides a specification, which is currently admitted.

One of the examples needed chan.for_range, and I was able to model it using a for: loop. It turns out that it's pretty pleasant to just unfold chan.for_range and use wp_for to verify that loop, so we shouldn't need any special tactics for this iterator.

Depends on goose-lang/goose#151 for various translation changes and fixes.

[tchajed]

These changes have the very minor downside that it is now difficult to reason about code that directly calls the model. You can actually still do it - after using wp_method_call to resolve the method, the current logatom triples will apply, and then you can even use a protocol spec.

[tchajed]

There is one (slightly annoying) issue I didn't have time to implement. golang/theory.v is supposed to export all the theory needed to verify any Go primitive. But the channel model proofs import it, so we can't export golang/theory/chan.v (it would create a circular dependency). The solution is probably for all the channel logatom proofs to carefully import from New.golang.theory directly.

[lredlin]

These changes have the very minor downside that it is now difficult to reason about code that directly calls the model. You can actually still do it - after using wp_method_call to resolve the method, the current logatom triples will apply, and then you can even use a protocol spec.

So to be clear, this would allow reasoning about nonblocking select in a way that depends on attempting the cases before default? That is, we'd be able to step through a select statement through the model code if we need to since the choice based specs do not surface this to the user. We need that right now to be able to verify the code below but I think we should still be able to do that here

package main

import "math/rand"

func main() {
x := make(chan int)
if rand.Int() & 1 == 0 {
close(x)
}
select {
case <-x:
default:
close(x)
}
}

[lredlin]

This LGTM, it seems like the next step is to specify/verify select which should hopefully be easier than it was given the cleaner syntax

[tchajed]

There's already a specification for select in terms of the AUs, including both blocking and non-blocking variants. However, I didn't attempt to prove it at all.

The model for select doesn't do the random selection. I consider that low priority since we would end up with the same specification.

[lredlin]

There's already a specification for select in terms of the AUs, including both blocking and non-blocking variants. However, I didn't attempt to prove it at all.

The model for select doesn't do the random selection. I consider that low priority since we would end up with the same specification.

Ok yeah I missed that since I was expecting it to be in the chan_au_sel file