More concise definition of absint_sound and absint_complete in AbstractInterpretation.v
Opened this issue · 2 comments
I was reading AbstractInterpretation.v's definitions of absint_sound and absint_complete, and found them quite challenging to read because of the verbosity.
I thought I'd try rewriting it a bit to more closely match the book's statement of the algebraic laws, and I think it's a lot clearer:
Section absint_theorems.
Variable A : absint.
Infix "~" := A.(Represents) (at level 70, no associativity).
Infix "⊔" := A.(Join) (at level 50).
Notation "a ⊑ b" := (forall n, n ~ a -> n ~ b) (at level 70, no associativity).
Infix "@+" := A.(Add) (at level 50).
Infix "@-" := A.(Subtract) (at level 50).
Infix "@*" := A.(Multiply) (at level 50).
Record absint_sound : Prop := {
TopSound : forall n, n ~ A.(Top);
ConstSound : forall n, n ~ A.(Constant) n;
AddSound : forall n m a b, n ~ a -> m ~ b -> (n + m) ~ (a @+ b);
SubtractSound : forall n m a b, n ~ a -> m ~ b -> (n - m) ~ (a @- b);
MultiplySound : forall n m a b, n ~ a -> m ~ b -> (n * m) ~ (a @* b);
AddMonotone : forall a b a' b', a ⊑ a' -> b ⊑ b' -> (a @+ b) ⊑ (a' @+ b');
SubtractMonotone : forall a b a' b', a ⊑ a' -> b ⊑ b' -> (a @- b) ⊑ (a' @- b');
MultiplyMonotone : forall a b a' b', a ⊑ a' -> b ⊑ b' -> (a @* b) ⊑ (a' @* b');
JoinSoundLeft : forall a b, a ⊑ (a ⊔ b);
JoinSoundRight : forall a b, b ⊑ (a ⊔ b)
}.
(* Here's a "bonus" condition that we'll sometimes use and sometimes not:
* [Join] gives a *least* upper bound of its two arguments, such that any other
* upper bound is also at or above the join. *)
Definition absint_complete := forall a b c, a ⊑ c -> b ⊑ c -> (a ⊔ b) ⊑ c.
End absint_theorems.
I wanted to use +^
, -^
, and *^
to more closely mimic the book's notation, but *^
is already used for transitive closures, and I couldn't figure out how to locally override that notation.
Notably, after rewriting it this way, I noticed that TopSound differs from the law stated on page 44 (forall a, a ⊑ A.(Top)
). Though assuming ConstSound, the two statements are equivalent. That is, (forall n, n ~ A.(Constant) n) -> (forall n, n ~ A.(Top)) <-> (forall a, a ⊑ A.(Top))
is true. (Maybe this is obvious to others, but I found it at least worth formally proving.)
--
Of course, the statement could be further refactored; e.g., instead of adding helper notation for the operations, the soundness and monotone theorems could be abstracted like:
Definition absop_sound natop absop := forall n m a b, n ~ a -> m ~ b -> (natop n m) ~ (absop a b).
Definition absop_monotone absop := forall a b a' b', a ⊑ a' -> b ⊑ b' -> (absop a b) ⊑ (absop a' b').
--
Finally, I note that page 43 says 𝓒 and the abstract operations calculate the "most precise abstractions", but there's no formalization of this concept.
I believe the correct theorems are:
Definition const_complete := forall n a, n ~ a -> A.(Constant) n ⊑ a.
Definition absop_complete natop absop :=
forall a b c, (forall n m, n ~ a -> m ~ b -> (natop n m) ~ c) -> (absop a b) ⊑ c.
None of the subsequent proofs actually rely on this, but for the purpose of proving an abstraction complete (e.g., #28), it might be worth including and then proving for at least parity_absint?
Edit: Also worth noting is that absop_sound and absop_complete together imply absop_monotone. (Again, probably expected, but I decided to formally verify.)
--
Happy to send a pull request for any of the above, but thought I'd file an issue first to check that it matches the intended direction.
On the topic of completeness, I thought I'd report that this weekend, as an exercise, I reimplemented the parity and interval lattices and proved their abstractions of addition, subtraction, and multiplication both sound and complete.
Notably, interval_combine mult
is not complete as it computes [0,0] × [n,∞) = [0,∞), whereas the most precise abstract result is [0,0]. Fixing this (and [n,∞) × [0,0]) makes it complete though.
Thanks for taking the initiative here! I'd be happy to accept a pull request, though I'd ask that it not use Unicode operators, which I've avoided through the rest of the book code.