# Sd-keylist-find-skipped

Perform skip-detection for a single pattern within an expression.

- Signature
(sd-keylist-find-skipped x y ctx) → prob?

- Arguments
`x` — Guard (sd-keylist-p x).
`y` — Guard (sd-keylist-p y).
`ctx` — Guard (vl-context1-p ctx).
- Returns
`prob?` — Type (equal (sd-problem-p prob?) (if prob? t nil)), given the guard.

We expect that all of the keys in x and y have the same
pattern. In practice, assuming the original wire names are free of *
characters, this means that all keys throughout x and y should differ
only by their indices. More specifically, our expectation here is that the
keys in x have been generated from the wires in some particular
expression, while the keys in y were generated by looking at the entire
module.

Our goal is to investigate whether this expression uses "all but one" of
the wires of this pattern. That is, it would be suspicious for x to
mention all of foo1, foo2, foo3, and foo5, but not foo4. If there are a lot of
wires in x and y, then this is a very easy comparison. The hard
cases are when there aren't very many wires in the first place.

If there is only one wire that matches this pattern, then there are only two
cases -- the expression mentions the wire or it doesn't -- and neither of these
cases are suspicious.

If there are only two wires that share this pattern, then we might use none,
one, or both of them, and none of these cases are suspicious.

If there are three wires that share this pattern, and we only use two of
them, then this is starting to get slightly suspicious. We'll go ahead and
flag it.

Beyond that point, if we find that exactly one wire is missing, we flag it
with an alarm level equal to the number of wires that match the pattern.
In other words, the alarm level is somehow like a confidence indicator that
says how suspicious this omission is -- it's not too suspicious to omit one out
of three wires, but it's really suspicious to omit one out of ten.

### Definitions and Theorems

**Function: **sd-keylist-find-skipped

(defun sd-keylist-find-skipped (x y ctx)
(declare (xargs :guard (and (sd-keylist-p x)
(sd-keylist-p y)
(vl-context1-p ctx))))
(let ((__function__ 'sd-keylist-find-skipped))
(declare (ignorable __function__))
(b* ((ys (mergesort y))
(yl (len ys))
((unless (> yl 2)) nil)
(xs (mergesort x))
(missing (difference ys xs))
(nmissing (len missing))
((unless (= nmissing 1)) nil)
(linearp (sd-keylist-linear-increments-p ys))
(idx-min (sd-key->index (car ys)))
(idx-max (sd-key->index (car (last ys))))
(idx-missing (sd-key->index (car missing)))
(middlep (and linearp (natp idx-min)
(natp idx-max)
(natp idx-missing)
(< idx-min idx-missing)
(< idx-missing idx-max)))
(dupep (same-lengthp x ys))
(priority (cond ((and middlep dupep) 10)
(middlep 6)
(dupep 4)
(linearp 2)
(t 1))))
(make-sd-problem :type :skipped
:priority priority
:groupsize yl
:key (car missing)
:ctx ctx))))

**Theorem: **return-type-of-sd-keylist-find-skipped

(defthm return-type-of-sd-keylist-find-skipped
(implies (and (force (sd-keylist-p x))
(force (sd-keylist-p y))
(force (vl-context1-p ctx)))
(b* ((prob? (sd-keylist-find-skipped x y ctx)))
(equal (sd-problem-p prob?)
(if prob? t nil))))
:rule-classes :rewrite)