In tests/specs/verification.k, there are at least a couple of lemmas that I think are incorrect.
In all these cases the error being made is that we are not taking into account that operations are integer operations and so we can't do real number algebraic simplification.
rule N:Int >=Int X /Int Y => N *Int Y >=Int X [simplification]
has a counterexample of
3 >=Int 10 /Int 3 => 9 >=Int 10
and
rule N:Int >=Int log2Int(X:Int) => 2 ^Int N >=Int X [simplification]
has a counterexample of
2 >=Int log2Int(5) => 4 >=Int 5
I think we could possibly rectify this by replacing these two lemmas with
rule N:Int >=Int log2Int(X:Int) => (2 ^Int (N +Int 1)) -Int 1 >=Int X [simplification]
rule N:Int >=Int X /Int Y => ((N +Int 1) *Int Y) -Int 1 >=Int X [simplification]
But I'd like this to be double-checked, and I also need to see if this looser bound will break any of the proofs.
In
tests/specs/verification.k, there are at least a couple of lemmas that I think are incorrect. In all these cases the error being made is that we are not taking into account that operations are integer operations and so we can't do real number algebraic simplification.has a counterexample of
and
has a counterexample of
I think we could possibly rectify this by replacing these two lemmas with
But I'd like this to be double-checked, and I also need to see if this looser bound will break any of the proofs.