Updates to infinite gas abstraction #945
Conversation
| claim <k> runLemma(#gas(G) <Int #gas(G' +Int 700)) => doneLemma(false) ... </k> | ||
| claim <k> runLemma(#gas(G' +Int 700) <=Int #gas(G)) => doneLemma(true) ... </k> |
There was a problem hiding this comment.
How these 2 can be true? We don't know the value difference between G and G'
There was a problem hiding this comment.
The values under the #gas do not matter, they are only used for tracking the gas usage as metadata. #gas(_) with any argument is the same positive infinity as any other #gas(_)
| claim <k> runLemma(#if _:Int ==Int 0 #then #gas(VGas -Int Csstore(_, _, _,_)) #else #gas(VGas +Int -344) #fi <Int 8) => doneLemma(false) ... </k> | ||
| claim <k> runLemma(8 <=Int #if _:Int ==Int 0 #then #gas(VGas -Int Csstore(_, _, _,_)) #else #gas(VGas +Int -344) #fi) => doneLemma(true) ... </k> | ||
|
|
||
| claim <k> runLemma(#if _:Int ==Int 0 #then #gas(VGas -Int Csstore(_, _, _,_)) #else #gas(VGas +Int -344) #fi <Int minInt(#if _ #then #gas(_) #else #gas(_) #fi, #gas(_))) => doneLemma(false) ... </k> | ||
| claim <k> runLemma(minInt(#if _ #then #gas(_) #else #gas(_) #fi, #gas(_)) <=Int #if _:Int ==Int 0 #then #gas(VGas -Int Csstore(_, _, _,_)) #else #gas(VGas +Int -344) #fi) => doneLemma(true) ... </k> |
There was a problem hiding this comment.
Again, I don't understand how these lemmas can be proved. The if _ == 0 must be undecided.
There was a problem hiding this comment.
If both branches of the #if are +Inf gas, then the entire expression will always be infinite gas. Same with minInt.
We have to make sure that #gas always "bubbles up" to the top of the expression in the <gas> cell, so that when we compare any particular value to it during execution we never run out of gas.
| rule #gas(_) <Int #gas(_) => false [simplification] | ||
| rule #gas(_) <=Int #gas(_) => true [simplification] |
There was a problem hiding this comment.
The rationale behind these lemmas is unclear to me. Can you add a comment explaining them?
There was a problem hiding this comment.
Also, in what kind of scenarios are they useful?
There was a problem hiding this comment.
#gas represents positive infinite: +Inf. We have that +Inf <Int +Inf => false and +Inf <=Int +Inf => true
They are used when you make a CALL, because you end up with a comparison between the current gas (which is some #gas(_) expression), and the gas allocated for the call (which is another #gas(_)) expression..
These are setup so that we never fail due to OOG.
There was a problem hiding this comment.
Thanks! All makes sense now. I think it's useful to add your explanation as comment in k file, as this is non-obvious.
There was a problem hiding this comment.
I added a comment with this explanation to the documentation at the top of the file.
ehildenb
force-pushed
the
infinite-gas
branch
from
f624eda
to
028f8b9
Compare
concreteattribute.