include/infinite-gas, tests/infinite-gas-spec: another disequality lemma for Cgascap

Author: ehildenb

include/kframework/infinite-gas.md

@@ -134,6 +134,7 @@ module INFINITE-GAS-COMMON
     rule         Cmem(_, N) <Int #gas(G) => true requires N  <Int #gas(G) [simplification]
 
     rule 0 <=Int Cgascap(_, _, _, _)                    => true                                            [simplification]
+    rule G <=Int Cgascap(_, GCAP, #gas(_), _)           => true  requires G <=Int GCAP                     [simplification]
     rule         Cgascap(_, GCAP, _, _)          <Int G => true  requires 0 <=Int GCAP andBool GCAP <Int G [simplification]
     rule         Cgascap(_, #gas(_), #gas(_), _) <Int _ => false                                           [simplification]
 

tests/specs/functional/infinite-gas-spec.k

@@ -128,4 +128,6 @@ module INFINITE-GAS-SPEC
     claim <k> runLemma(Cgascap(ISTANBUL, #gas(_), #gas(_), 700) <Int 3) => doneLemma(false) ... </k>
     claim <k> runLemma(0 <=Int Cgascap(ISTANBUL, #gas(VGAS +Int -5413), #gas(VGAS +Int -5413), 700)) => doneLemma(true) ... </k>
 
+    claim [Cgascap-comparison]: <k> runLemma(3000 <=Int Cgascap(ISTANBUL, #gas(VGAS +Int -491), #gas(VGAS +Int -491), Cextra(ISTANBUL, true, 0, _))) => doneLemma(true) ... </k>
+
 endmodule