// 4) Otherwise, the ith element equals the string representation of i.ensures forall i :: 0 <= i < n ==> i % 3 != 0 && i % 5 != 0 ==> ret[i] == i
The natural-language specification says ‘otherwise’, but the machine specification says ‘i % 3 != 0 && i % 5 != 0’—a subtle but crucial difference that makes the latter less modular and more difficult to reason about. TFA derides non-verified code for having the potential to accidentally invert conditions; but the exact same issue is present here, but even worse, since you have to duplicate the condition. You get proof of consistency between the specification and the code, but not between different parts of the specification, should you duplicate conditions because your specification language is insufficiently expressive.
I think formal verification has a great deal of value and untapped potential; but this does not make a very good showing. And formal verification will always suffer from specification errors: did you prove what you really wanted to prove?
There is another issue that straight-line code would avoid but which is present here (both in the proof and in the pudding): the former trivially initialises every element of the result array. Whereas here we must manually verify that the four cases presented form an exhaustive partition of the natural numbers. I would almost prefer an exhaustive pattern-match (or nested branch, whatever) on the two booleans (i%3==0,i%5==0), for this reason.
This is one reason I use verifying leftpad instead: the implementation is sufficiently different from the specification that it doesn’t feel redundant.
Speaking of verification, I have a seemingly simple problem the systems I tried it on (TLA+, Coq) seem to be unable to address (or, more likely, I don’t have the tools).
So I have these two integers a and b, that are in [0, K] (where K is a positive integer). I would like to prove the following:
a + b ≤ 2 K
a × b ≤ K²
Should be easy, right? Just one little snag: K is often fairly big, typically around 2^30 (my goal here is to prove that a given big number arithmetic never causes limb overflow). I suspect naive SAT solving around Peano arithmetic is not going to cut it.
This should be pretty easy for any modern SMT solver to prove.
I’m not exactly an expert, but this seems to work for Z3:
; Declare variables/constants
(declare-const K Int)
(declare-const a Int)
(declare-const b Int)
; Specify the properties of the variables
(assert (> K 0))
(assert (>= a 0))
(assert (>= b 0))
(assert (<= a K))
(assert (<= b K))
; Now let's prove facts
(push) ; Save context
; Note how I've actually inserted the opposite statement of what you are trying to prove, see below as to why
(assert (> (+ a b) (* 2 K)))
(check-sat)
; If you get an `unsat` answer, it means your statement is proved
; If instead you get a `sat` answer, you can use the (get-model) command here
; to get a set of variable assignments which satisfy all the assertions, including
; the assertion stating the opposite of what you are trying to prove
(pop) ; Restore context
(assert (> (* a b) (* K K)))
(check-sat)
; See above for the comment about the (get-model) command
Save that to a file and then run z3 <file.smt>.
Z3 should give you 2 unsat answers in a fraction of a second, which means that your 2 statements were proven to be true. Notably, it proves this for any K > 0 (including 2^30, 2^250, 2^1231823, etc…)
As far as I understand, the biggest gotcha is that you have to negate the statement that you are trying to prove and then let the SMT solver prove that there is no combination of values for the a, b and K integers that satisfy all the assertions. It’s a bit unintuitive at first, but it’s not hard to get used to it.
my goal here is to prove that a given big number arithmetic
never causes limb overflow
I’m not exactly sure what you mean here, is it that you’re using
modulo arithmetic? If not, I’ve got a little proof here in Coq:
Theorem for_lobsters : forall a b k : nat,
a<=k /\ b<=k -> a+b <= 2*k /\ a*b <= k*k.
Proof.
split.
- lia.
- now apply PeanoNat.Nat.mul_le_mono.
Qed.
I think even if you’re doing modulo arithmetic, it shouldn’t be too
hard to prove the given lemmas. But you might need to put some
tighter restrictions on the bounds of a and b. For example
requiring that a and b are both less than sqrt(k) (though
this is too strict).
I’m not sure what “split” means, though I guess it splits
conjunction in the conclusion of the theorem into 2 theorems…
Yep!
I have no idea what lia means.
The lia tactic solves arithmetic expressions. It will magically
solve a lot of proofs that are composed of integer arithmetic. The
docs on lia can be found here. Note that I omitted an import
statement in the snippet above. You need to prepend From Coq Require Import Lia to use it.
I have no idea how PeanoNat.Nat.mul_le_mono applies here. I guess
I’ll have to look at the documentation.
The mul_le_mono function has the following definition, which
almost exactly matches the goal. I found it using Search "<=".
PeanoNat.Nat.mul_le_mono
: forall n m p q : nat, n <= m -> p <= q -> n * p <= m * q
I used now apply ... which is shorthand for apply ...; easy.
The easy tactic will try to automatically solve the proof using
a bunch of different tactics. You could do without the automation
and solve the goal with apply PeanoNat.Nat.mul_le_mono; destruct H; assumption, if you’re so inclined.
I take issue with part of this:
The natural-language specification says ‘otherwise’, but the machine specification says ‘i % 3 != 0 && i % 5 != 0’—a subtle but crucial difference that makes the latter less modular and more difficult to reason about. TFA derides non-verified code for having the potential to accidentally invert conditions; but the exact same issue is present here, but even worse, since you have to duplicate the condition. You get proof of consistency between the specification and the code, but not between different parts of the specification, should you duplicate conditions because your specification language is insufficiently expressive.
I think formal verification has a great deal of value and untapped potential; but this does not make a very good showing. And formal verification will always suffer from specification errors: did you prove what you really wanted to prove?
There is another issue that straight-line code would avoid but which is present here (both in the proof and in the pudding): the former trivially initialises every element of the result array. Whereas here we must manually verify that the four cases presented form an exhaustive partition of the natural numbers. I would almost prefer an exhaustive pattern-match (or nested branch, whatever) on the two booleans (i%3==0,i%5==0), for this reason.
This is one reason I use verifying leftpad instead: the implementation is sufficiently different from the specification that it doesn’t feel redundant.
Speaking of verification, I have a seemingly simple problem the systems I tried it on (TLA+, Coq) seem to be unable to address (or, more likely, I don’t have the tools).
So I have these two integers a and b, that are in [0, K] (where K is a positive integer). I would like to prove the following:
Should be easy, right? Just one little snag: K is often fairly big, typically around 2^30 (my goal here is to prove that a given big number arithmetic never causes limb overflow). I suspect naive SAT solving around Peano arithmetic is not going to cut it.
This should be pretty easy for any modern SMT solver to prove. I’m not exactly an expert, but this seems to work for Z3:
Save that to a file and then run
z3 <file.smt>.Z3 should give you 2
unsatanswers in a fraction of a second, which means that your 2 statements were proven to be true. Notably, it proves this for anyK > 0(including 2^30, 2^250, 2^1231823, etc…)As far as I understand, the biggest gotcha is that you have to negate the statement that you are trying to prove and then let the SMT solver prove that there is no combination of values for the
a,bandKintegers that satisfy all the assertions. It’s a bit unintuitive at first, but it’s not hard to get used to it.I’m not exactly sure what you mean here, is it that you’re using modulo arithmetic? If not, I’ve got a little proof here in Coq:
I think even if you’re doing modulo arithmetic, it shouldn’t be too hard to prove the given lemmas. But you might need to put some tighter restrictions on the bounds of
aandb. For example requiring thataandbare both less thansqrt(k)(though this is too strict).My, I’m starting to understand why I couldn’t prove that trivial theorem:
liameans.Thanks a lot though, I’ll try this out.
Yep!
The
liatactic solves arithmetic expressions. It will magically solve a lot of proofs that are composed of integer arithmetic. The docs onliacan be found here. Note that I omitted an import statement in the snippet above. You need to prependFrom Coq Require Import Liato use it.The
mul_le_monofunction has the following definition, which almost exactly matches the goal. I found it usingSearch "<=".I used
now apply ...which is shorthand forapply ...; easy. Theeasytactic will try to automatically solve the proof using a bunch of different tactics. You could do without the automation and solve the goal withapply PeanoNat.Nat.mul_le_mono; destruct H; assumption, if you’re so inclined.I hope this is helpful!