Dumping inferred types #546

skius · 2023-11-01T17:17:14Z

skius
Nov 1, 2023

I've been looking into abstract refinements, and was really excited to see something like this work:

#[flux::sig(
    fn<refine p: int -> bool>(x: i32, y: i32) -> i32{v: p(v) && v >= x && v >= y}
    requires p(x) && p(y)
)]
fn max(x: i32, y: i32) -> i32 {
    if x > y {
        x
    } else {
        y
    }
}

#[flux::sig(fn() -> i32[{v: v % 4 == 2}])] // note this is only satisfied by 6, not by i32{v: v >= 4 && v >= 6}
fn test00() -> i32 {
    max(4, 6)
}

In particular, how it was able to infer that v % 4 == 2 must be true for the max of 4 and 6. I can see "by eye" that by instantiating p(x) := x == 4 || x == 6 such a postcondition is easily proven, but I was wondering what exactly flux is doing behind the scenes.

I tried enabling a bunch of DUMP_ environment variables, which got me this .smt2 file:

// Tag 0: Call at 22:5: 22:14
// Tag 1: Ret at 22:5: 22:14

(qualif EqZero ((a0 int)) (a0 = 0))
(qualif GtZero ((a0 int)) (a0 > 0))
(qualif GeZero ((a0 int)) (a0 >= 0))
(qualif LtZero ((a0 int)) (a0 < 0))
(qualif LeZero ((a0 int)) (a0 <= 0))
(qualif Eq ((a0 int) (a1 int)) (a0 = a1))
(qualif Gt ((a0 int) (a1 int)) (a0 > a1))
(qualif Ge ((a0 int) (a1 int)) (a0 >= a1))
(qualif Lt ((a0 int) (a1 int)) (a0 < a1))
(qualif Le ((a0 int) (a1 int)) (a0 <= a1))
(qualif Le1 ((a0 int) (a1 int)) (a0 <= (a1 - 1)))
(data Pair 2 = [| Pair { fst: @(0), snd: @(1) } ])
(data Unit 0 = [| Unit { }])
(var $k0 ((int))) // orig: $k0

(constraint
  (and
    (forall ((a0 int) (a0 = 4))
      (forall ((a1 int) (a1 = 6))
        (and
          (tag ($k0 a0) "0")
          (tag ($k0 a1) "0")
        )
      )
    )
    (forall ((a2 int) (true))
      (forall ((_ Unit) (and ($k0 a2) (a2 >= 4) (a2 >= 6)))
        (tag ((a2 mod 4) = 2) "1")
      )
    )
  )
)

And after feeding that into liquid-fixpoint with the -v option, I got:

Liquid-Fixpoint Copyright 2013-21 Regents of the University of California.
All Rights Reserved.

Options: Config {srcFile = "max_mod4.test00.smt2", cores = Nothing, minPartSize = 500, maxPartSize = 700, solver = z3, linear = False, stringTheory = False, defunction = False, allowHO = False, allowHOqs = False, eliminate = none, scrape = no, elimBound = Nothing, smtTimeout = Nothing, elimStats = False, solverStats = False, metadata = False, stats = False, parts = False, save = False, minimize = False, minimizeQs = False, minimizeKs = False, minimalSol = False, etaElim = False, gradual = False, ginteractive = False, autoKuts = False, nonLinCuts = False, noslice = False, rewriteAxioms = False, pleWithUndecidedGuards = False, interpreter = False, oldPLE = False, noIncrPle = False, noEnvironmentReduction = False, inlineANFBindings = False, checkCstr = [], extensionality = False, rwTerminationCheck = False, stdin = False, json = False, noLazyPLE = False, fuel = Nothing, restOrdering = "rpo"}
Horn Uniq:
(and
 (forall ((a0 int) (a0 == 4))
  (forall ((a1 int) (a1 == 6))
   (and
    (($k0 a0))
    (($k0 a1)))))
 (forall ((a2 int) (true))
  (forall ((_ Unit) (and ($k0 a2) (a2 >= 4) (a2 >= 6)))
   ((a2 mod 4 == 2)))))
Number of partitions : 1
number of cores      : Nothing
minimum part size    : 500
maximum part size    : 700

**** DONE:  Uniqify & Rename ***************************************************


**** DONE:  Worklist Initialize ************************************************

Working   0% [.................................................................]
Computing50% [=================================
; SMT Says: Unsat
UNSAT id 3 False
LHS: ((exists [lq_karg$nnf_arg##k0##0##k0 : int]
         . lq_karg$nnf_arg##k0##0##k0 == a2
           && exists [a0 : int; a1 : int; a1##2 : int]
                . (a0 : int) == (4 : int)
                  && (a1 : int) == (6 : int)
                  && (a1##2 : int) == (6 : int)
                  && lq_karg$nnf_arg##k0##0##k0 == a1##2
       || exists [lq_karg$nnf_arg##k0##0##k0 : int]
            . lq_karg$nnf_arg##k0##0##k0 == a2
              && exists [a0 : int; a1 : int; a1##1 : int]
                   . (a0 : int) == (4 : int)
                     && (a1 : int) == (6 : int)
                     && (a1##1 : int) == (6 : int)
                     && lq_karg$nnf_arg##k0##0##k0 == a0)
      && (exists [lq_karg$nnf_arg##k0##0##k0 : int]
            . lq_karg$nnf_arg##k0##0##k0 == a2
              && exists [a0 : int; a1 : int; a1##2 : int]
                   . (a0 : int) == (4 : int)
                     && (a1 : int) == (6 : int)
                     && (a1##2 : int) == (6 : int)
                     && lq_karg$nnf_arg##k0##0##k0 == a1##2
          || exists [lq_karg$nnf_arg##k0##0##k0 : int]
               . lq_karg$nnf_arg##k0##0##k0 == a2
                 && exists [a0 : int; a1 : int; a1##1 : int]
                      . (a0 : int) == (4 : int)
                        && (a1 : int) == (6 : int)
                        && (a1##1 : int) == (6 : int)
                        && lq_karg$nnf_arg##k0##0##k0 == a0))
     && (a2 >= 4
         && a2 >= 6)
     && (a2 >= 4
         && a2 >= 6)
RHS: ((a2 : int) mod (4 : int) : int) == (2 : int)
RESULT: 1afe (Stats {numCstr = 1, numIter = 1, =================================================================]
Safe ( 1  constraints checked)

I was wondering how (if that is even possible) to extract a "definition" for $k0 from the tools?

nilehmann · 2023-11-01T21:19:10Z

nilehmann
Nov 1, 2023
Maintainer

Hi @skius thanks for the interest!

The short answer is no. In this particular case, a solution for $k0 cannot be extracted from fixpoint. The reason is that when kvars are not included in a cycle fixpoint doesn't bother generating inference variables and it just "pushes" the strongest postcondition. The details of the algorithm are explained here https://ranjitjhala.github.io/static/local_refinement_typing.pdf.

When a variable is included in a cycle then there's an option in fixpoint that will give you back the solution.

I don't know if it's technically possible to modify fixpoint to also output solutions for the first type of kvars. @ranjitjhala will certainly known this better.

5 replies

nilehmann Nov 1, 2023
Maintainer

Take for example the constraint generated by this code

#[flux::sig(fn(n: u32) -> u32[n])]
fn foo(n: u32) -> u32 {
    let mut i = 0;
    while i < n {
        i += 1;
    }
    i
}

// Tag 0: Goto(bb1) at 3:9: 3:14
// Tag 1: Ret at 7:5: 7:6
// Tag 2: Goto(bb1) at 4:17: 6:6

(qualif EqZero ((a0 int)) (a0 = 0))
(qualif GtZero ((a0 int)) (a0 > 0))
(qualif GeZero ((a0 int)) (a0 >= 0))
(qualif LtZero ((a0 int)) (a0 < 0))
(qualif LeZero ((a0 int)) (a0 <= 0))
(qualif Eq ((a0 int) (a1 int)) (a0 = a1))
(qualif Gt ((a0 int) (a1 int)) (a0 > a1))
(qualif Ge ((a0 int) (a1 int)) (a0 >= a1))
(qualif Lt ((a0 int) (a1 int)) (a0 < a1))
(qualif Le ((a0 int) (a1 int)) (a0 <= a1))
(qualif Le1 ((a0 int) (a1 int)) (a0 <= (a1 - 1)))
(data Pair 2 = [| Pair { fst: @(0), snd: @(1) } ])
(data Unit 0 = [| Unit { }])
(var $k0 ((int) (int))) // orig: $k0

(constraint
  (forall ((a0 int) (true))
    (forall ((_ Unit) (a0 >= 0))
      (and
        (forall ((a1 int) (a1 = 0))
          (tag ($k0 a1 a0) "0")
        )
        (forall ((a2 int) (true))
          (forall ((_ Unit) ($k0 a2 a0))
            (and
              (forall ((_ Unit) (~(a2 < a0)))
                (tag (a2 = a0) "1")
              )
              (forall ((_ Unit) (a2 < a0))
                (forall ((a3 int) (a3 = (a2 + 1)))
                  (tag ($k0 a3 a0) "2")
                )
              )
            )
          )
        )
      )
    )
  )
)

In this case, if you run fixpoint --save it will give you the solution for $k0


Solution:
$k0 := nnf_arg##k0 >= 0
       && nnf_arg##k0 <= nnf_arg##k0


Non-cut kvars:

nilehmann Nov 1, 2023
Maintainer

Oh I'm confused now. I always thought fixpoint didn't materialize the solutions for the non-cut kvars. But if you run fixpoint --save it does give you the (unreadable) answer

Solution:



Non-cut kvars:

$k0 := exists [lq_karg$nnf_arg##k0##0##k0 : int;
               a0 : int;
               a1 : int;
               a1##2 : int]
         . lq_karg$nnf_arg##k0##0##k0 == a1##2
           && a0 == 4
           && a1 == 6
           && a1##2 == 6
       || exists [lq_karg$nnf_arg##k0##0##k0 : int;
                  a0 : int;
                  a1 : int;
                  a1##1 : int]
            . lq_karg$nnf_arg##k0##0##k0 == a0
              && a0 == 4
              && a1 == 6
              && a1##1 == 6

I'll let @ranjitjhala chime in...

skius Nov 1, 2023
Author

Thank you for the reply!

Ah! I had looked at the paper about local refinement typing (and read the Flux paper), but I missed the implication in the SMT syntax for forall so I didn't think to do strongest postcondition. In that case, can't I rewrite the subtype constraint for the generic predicate p (not sure if this is the correct terminology - I'm talking about the first conjunct) as ∀a. (a=4 -> k(a)) && (a=6 -> k(a)), meaning when I apply the section from the paper "In essence, if we have implications of the form: Pi ⇒ κ (ν ) then we can assign κ to the disjunction κ (x) = ∨i Pi after taking care to existentially quantify variables", I get k(z) := ...some existential things... (z=4) || (z=6)? Which would coincide with my "by eye" result! Is this correct?

Regarding the loop invariant, how should I read the predicate? I would expect k(i, n) := i >= 0 && i <= n, but I only see a single identifier nnf_arg##k0 inside that definition.

I suppose knowing how to differentiate different arguments to the predicate would also make the "Non-cut kvars" section more readable?

nilehmann Nov 2, 2023
Maintainer

I get k(z) := ...some existential things... (z=4) || (z=6)? Which would coincide with my "by eye" result! Is this correct?

Yes this is correct

Regarding the loop invariant, how should I read the predicate? I would expect k(i, n) := i >= 0 && i <= n, but I only see a single identifier nnf_arg##k0 inside that definition.

That looks like an error in the way Fixpoint prints the solution, you are indeed right the solution should involve two variables. Thanks for spotting it! I reported it as a bug ucsd-progsys/liquid-fixpoint#658

I suppose knowing how to differentiate different arguments to the predicate would also make the "Non-cut kvars" section more readable?

Hmm, not sure I follow this.

skius Nov 2, 2023
Author

Thanks a lot! Subscribed to the bug report.

Hmm, not sure I follow this.

It's possible I misunderstood you calling the OP solution "unreadable", but I'm saying that it does look exactly like the strongest postcondition solution, assuming we replace the 2nd and 4th instance of lq_karg$nnf_arg##k0##0##k0 with z (from k(z) := ...) - the two existentials would simplify to k(z) := (z=4) || (z=6). Of course, if we really are quantifying over z (meaning the 1st and 3rd occurrence are not a pretty-printing bug), then to me it would seem the whole expression simplifies to true which doesn't make sense to me.

ranjitjhala · 2023-11-02T14:41:55Z

ranjitjhala
Nov 2, 2023
Maintainer

Hi Neils - yes, indeed the existential quantification is over variables *other than* the “parameters” (z). In this case there are none, but in general the horn constraint “defining” K can have other binders which get existentially quantified out (analogous to the quantification of “old” values in the usual strongest postcondition rule) Ranjit

…

On Thu, Nov 2, 2023 at 4:02 AM Niels Saurer ***@***.***> wrote: Thanks a lot! Subscribed to the bug report. Hmm, not sure I follow this. It's possible I misunderstood you calling the OP solution "unreadable", but I'm saying that it does look exactly like the strongest postcondition solution, assuming we replace the 2nd and 4th instance of lq_karg$nnf_arg##k0##0##k0 with z (from k(z) := ...) - the two existentials would simplify to k(z) := (z=4) || (z=6). Of course, if we really are quantifying over z (and the 1st and 3rd occurrence are not a pretty-printing bug), then to me it would seem the whole expression simplifies to true which doesn't make sense to me. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/flux-rs/flux/discussions/546*discussioncomment-7455342__;Iw!!Mih3wA!AAnKWckUXosxFjSyyDSZ9xWRjeL8xdybMMdT94zTQhcuY9GGiq-JacS5JH7rSX8DU3S1aHd4UGQwn4ImBoe6MxiS$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OFYU6GDBLX2DXF5WKTYCN4TZAVCNFSM6AAAAAA6ZTQORWVHI2DSMVQWIX3LMV43SRDJONRXK43TNFXW4Q3PNVWWK3TUHM3TINJVGM2DE__;!!Mih3wA!AAnKWckUXosxFjSyyDSZ9xWRjeL8xdybMMdT94zTQhcuY9GGiq-JacS5JH7rSX8DU3S1aHd4UGQwn4ImBg1oMINq$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

1 reply

skius Nov 2, 2023
Author

Thanks for confirming!

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Dumping inferred types #546

{{title}}

Replies: 2 comments 6 replies

{{title}}

{{title}}

{{editor}}'s edit

{{editor}}'s edit

{{title}}

{{title}}

{{editor}}'s edit

{{editor}}'s edit

{{title}}

{{title}}

{{editor}}'s edit

{{editor}}'s edit

{{title}}

{{title}}

Select a reply

Dumping inferred types #546

skius Nov 1, 2023

Replies: 2 comments · 6 replies

nilehmann Nov 1, 2023 Maintainer

nilehmann Nov 1, 2023 Maintainer

nilehmann Nov 1, 2023 Maintainer

skius Nov 1, 2023 Author

nilehmann Nov 2, 2023 Maintainer

skius Nov 2, 2023 Author

ranjitjhala Nov 2, 2023 Maintainer

skius Nov 2, 2023 Author

skius
Nov 1, 2023

Replies: 2 comments 6 replies

nilehmann
Nov 1, 2023
Maintainer

nilehmann Nov 1, 2023
Maintainer

nilehmann Nov 1, 2023
Maintainer

skius Nov 1, 2023
Author

nilehmann Nov 2, 2023
Maintainer

skius Nov 2, 2023
Author

ranjitjhala
Nov 2, 2023
Maintainer

skius Nov 2, 2023
Author