Update token pool spec - Githubissues

hjorthjort commented 3 years ago

Closes #206

I have a working positive case for the update_token_pool function but I have some question marks. I'm not sure exactly why some of these initial values need to look the way they look, or if the way I've written the spec is sound. Help appreciated.

sskeirik commented 3 years ago

@hjorthjort Hey Rikard, I noticed you commented out all of the other proofs?

hjorthjort commented 3 years ago

@hjorthjort Hey Rikard, I noticed you commented out all of the other proofs?

Yeah, I tend to do that while figuring out a specific one, to make it faster to run.

hjorthjort commented 3 years ago

Overall, looks good to me. The only thing that surprises me is that you needed to split the negative case into two subproofs. Was that for correctness or performance?

Performance. I got "broken pipe" issues without it I'll try pushing the combined spec and see if CI handles it better

hjorthjort commented 3 years ago

Okay, latest update: it's not just performance. Seems the prover can't resolve some of the orBool conditions into "either A or B or both", but rather gets stuck with something like this on the path conditions:

   true          
  #Equals                                                                                                                                                                     notBool ( Sender:Address ~> . ) ==K ( Source:Address ~> . ) orBool ( ( KnownAddresses [ TokenAddress:Address ] ~> . ) ==K ( #Contract ( _A , T ) ~> . ) andBool notBoo
l ( T:Type ~> . ) ==K ( pair .AnnotationList address .AnnotationList contract .AnnotationList nat .AnnotationList ~> . ) )

Let's use the double claims for now. I'll spend some time trying to resolve this in order to improve on #234, but it's already turning into a time sink to merge the two failure claims and I'd rather move on.

runtimeverification / michelson-semantics

Update token pool spec #226