[acl2-books] Svtv-run and non-boolean variables as inputs

[David L. Rager]

Hi SV Users,

I'd like to prove a theorem that describes a mux when the selector=1,
similar to the following:

(def-gl-thm mux-boolean-spec
:hyp (and (bitp sel)
(bitp in1)
(equal sel 1))
:concl (equal (cdr (assoc 'out (svtv-run (mux-test-vector)
`((in0 . ,in0)
(in1 . ,in1)
(sel . ,sel))
:boolvars t)))
(if (logbitp 0 sel)
in1
in0))
:g-bindings (GL::AUTO-BINDINGS (:NAT SEL 1)
(:NAT IN1 1)))

The key is that I'd like to omit in0 from the hyps and the g-bindings.
The theorem is provable in Esim, but such a thing seems unprovable in
SV without including in0 in the GL simulation bindings. Does this
strike anyone else as odd? I admit that it's probably more odd that I
could prove it in Esim in the first place.

You might notice that I'm trying to use :boolvars to do something, but
I'm pretty sure I'm using it wrong. In fact, whether it's included
seems not to affect the appearance of the error.

The relevant code is available at:

https://gist.github.com/ragerdl/f666b83c2317b6ce4433

Thanks,
David

[David L. Rager]

Hi,

Assuming I can't just leave in0 free in SV, is there a hypothesis and
g-binding I can give that would constrain in0 to an sv::4vec-p?

Thanks,
David

[Sol Swords]

Depending what exactly you want, there are a few approaches.  None of them are super easy.

I'm guessing you want to apply this as a rewrite rule to something that has in0 in the input alist.  If not, I'd suggest just leaving in0 out.  This implicitly sets it to X.

In esim, 4v-sexprs are strictly monotonic and therefore setting something to X is as good as universally quantifying it.  SV/svex almost has this property as well; the only construct that violates this monotonicity is ===, which may simply not occur in your SVTV.  (The book sv/svex/lattice.lisp has some theorems pertaining to this.)  You could write a function svex-collect-fnsyms (would need to be memoized) and check using (member 'sv::=== (sv::svexlist-collect-fnsyms (alist-vals (sv::svtv->outexprs (my-svtv)))).  Then you could prove by induction

(implies (and (not (member '=== (svex-collect-fnsyms x)))

              (svex-env-[= al1 al2))

         (4vec-[= (svex-eval x al1) (svex-eval x al2)))

(see svex/lattice.lisp for the meanings of the [= functions.)  Then this basically says that for your svexes, since they don't contain ===, binding a variable to X (or not binding it at all) can only give you a result "worse than" (4vec-[=) a result you get when you bind it to something non-X.  Then you'd have to work this through the definition of svtv-run (it's a pretty thin wrapper around svexlist-eval).

Another alternative is to say in0 is a 4vec of a certain size -- its .upper and .lower fields are both (say) signed-byte 32.  A 4vec is either an integer (in which case .upper and .lower are the same) or (cons upper lower).  So a way to get such a binding in GL would be something like

(g-ite (g-boolean a)
       (g-int b c 32)

    (cons (g-int d e 32) (g-int f g 32))).

It might take some doing to prove the coverage obligation but it should be possible.

-Sol

--
--
ACL2-books help:
  To post new messages: acl2-...@googlegroups.com
  To unsubscribe: acl2-books-...@googlegroups.com
  More options: http://groups.google.com/group/acl2-books?hl=en

---
You received this message because you are subscribed to the Google Groups "acl2-books" group.
To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[David L. Rager]

Hi Sol,

Thanks for the ideas. I think your second and third suggestions are
quite applicable. Here's a subtlety related to the first suggestion:

> I'm guessing you want to apply this as a rewrite rule to something that has
> in0 in the input alist. If not, I'd suggest just leaving in0 out. This
> implicitly sets it to X.

Right, unfortunately we need to simulate the case where the input is
one of 0, 1, or X -- my impression is that this is different from just
the cases where the input is X. Maybe this is crazy talk, but thus
far, my little example (which I wish I could share) showcases the
subtlety. I don't think this violates the lattice properties, but
that discussion currently confuses me a bit.

If my push back surprises you, I would be eager to see if I can get
this other little example that's already public to clarify the issue
-- maybe that exercise would even show my an error of my thinking.

Best,
David

[David L. Rager]

Hmm, I thought these bindings would work, but to no avail -- I'm still
getting the error about "some bits assumed to be Boolean were not."
I've constrained in0 to be a bitp in this particular case. Anyone see
a meaningful typo?

:g-bindings `((sel (:G-NUMBER (0 1)))
(in0 (:g-number (2 3)))
(in1 ,(gl::g-ite '(:g-boolean . 10)
'(:g-number (11 12))
(cons '(:g-number (13 14))
'(:g-number (15 16))))))

[David L. Rager]

Got it! The above :g-binding seems to be fine.

Thanks to your answering of my query from a whlie ago, I had updated
the esim-to-sv documentation to state that I should be using :boolvars
nil (not t). Once I did that in both my svtv-run calls, the GL
simulation problem went away.

I haven't yet determined the necessity of the 4vec-p gl-binding -- I
can imagine that it's necessary to prevent some class of false
counterexamples, but the ones I'm currently getting back are verified
as valid by SV/GL/ACL2.

[David L. Rager]

Hi People-familiar-with-GL-coverage-proofs,

Any idea how to prove this GL coverage obligation? My next intent is
to start looking at shape-spec-obj-in-range and see if I can figure
out how GL figures this out. This is the simple integerp case for
in0, so I think I have a hope for being able to do so.

(IMPLIES
(AND (SV::4VEC-P IN0)
(INTEGERP IN0)
(<= 0 IN0)
(< IN0 2))
(GL::SHAPE-SPEC-OBJ-IN-RANGE '(:G-ITE ((:G-BOOLEAN . 4) :G-NUMBER (5 6))
(:G-NUMBER (7 8))
:G-NUMBER (9 10))
IN0))

I'll mention that I do have a work-around for this thread, but I'm
trying to see how far I can push the technology as it is without using
the work-around.

Thanks,
David

[Sol Swords]

Looks like you're on the right track. You probably want to prove
something like this as a rewrite rule (see the similar ones in
gl/shape-spec.lisp, such as shape-spec-obj-in-range-backchain-integer-1)
and use :cov-theory-add to enable it during the coverage proof phase.
To prove it should be just a matter of letting shape-spec-obj-in-range
and possibly shape-spec-obj-in-range-iff open up once or twice. An even
nicer higher-level rule would be one about 4vec-p and 4vec-sized-p (or
whatever you called it) rather than integerp and a range, and then you'd
want to say :do-not-expand (4vec-p 4vec-sized-p) as well.

[David L. Rager]

Hi Sol,

Beautiful, thanks!

For my own record, I'll mention that a second coverage proof goal came
up that required a lemma about another case of 4vec-p, which required
enabling 4vec-p to prove that lemma. I'd still like to prove the more
general rule, but this will do nicely for now.

w00t,
David