More concise definition of absint_sound and absint_complete in AbstractInterpretation.v

[mdempsky]

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.

[mdempsky]

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.

[achlipala]

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.