;; The discharge rules.
;;
;; `spec/safe-memory/07-check-elimination.md` section 7.7 asks for every elimination of a safety
;; check to be data in a `safety/` namespace rather than a condition somebody wrote inside a pass,
;; and gives the reason: an unsound elimination produces a correct answer on every test and an
;; undetected vulnerability in production, and nothing observes it. A rule a solver has to agree
;; with before the build finishes is the only mechanism in the specification that catches that
;; class, and it only catches it if the rule is written before the pass rather than fitted to it
;; afterwards.
;;
;; These are not rewrite rules and this table is not matched against the IR. A pattern here is a
;; question, built by `crate::discharge` out of what its walk over the dominator tree has worked
;; out, and a rule that fires is the answer yes. That is why the kind is `discharge` and not
;; `simplify`: a table of these in the simplifier would be matched against instructions, and there
;; is no instruction here to match.
;;
;; # What is proved and what is not
;;
;; Section 7.7 splits it, and the split is the design rather than a shortcut. The walk that
;; establishes the context is ordinary code: which check dominates which, which pointer was
;; computed from which, and how far apart the two addresses are. Nothing here proves any of that,
;; and section 7.7 says as much, that the analysis is the weak point and that the differential
;; check accounting of section 14.3 is what covers it. What is proved is the step from the context
;; to the removal, which is the part that is arithmetic and is therefore the part a person gets
;; wrong quietly and stays wrong about.
;;
;; So the obligation a rule here discharges reads: given an access that has been checked, and a
;; second access a constant distance further along whose size the compiler has in hand as a number,
;; the second access's bytes are inside the first access's bytes. What the pass may then conclude,
;; and this step is document 07 section 7.3's rather than a rule's, is that a check which passed on
;; the first range cannot refuse the second, because a bounds check asks whether the bytes it is
;; about lie inside one storage instance and a subset of those bytes lies inside the same instance.
;;
;; # Why the guard carries bounds that look unnecessary
;;
;; A guard is read twice. The compiler reads it in `i128`, where adding two byte counts does not
;; wrap, and the solver reads it in the sixty four bits the rule runs in, where it does. The two
;; agree while the numbers stay small and part company at the ends of the type, and a rule proved
;; under the solver's reading and run under the compiler's is a rule proved about arithmetic that
;; is not happening. So each distance and each size is bounded, at four gigabytes, which is past
;; any access a real program makes and far short of anywhere the two readings differ. An access
;; beyond it is not refused: it is not discharged, and its check stays.
;; A bounds check on bytes a dominating bounds check has already covered.
;;
;; `at` and `span` are the address and the size of the access that was checked, `delta` is how far
;; past that address the one being asked about starts, and `reach` is its size. The guard is
;; containment of one interval in another, in byte counts, which is the arithmetic the pass does.
;; The claim is containment of one byte range in another, in addresses, which is what document 07
;; section 7.3 writes the removal condition in. Proving that the first implies the second at sixty
;; four bits is the whole of what this rule is for, and it is not the guard said twice: an interval
;; inside another interval says nothing on its own about two address ranges, either of which could
;; run off the end of the address space.
(rule (discharge (covered.i64 (value.i64 at)
(iconst.i64 span)
(iconst.i64 delta)
(iconst.i64 reach)))
(if (and (>= delta 0) (<= delta 4294967296)
(>= reach 0) (<= reach 4294967296)
(>= span 0)
(<= (+ delta reach) span)))
(iconst.i64 1)
(spec (= (ite (or (bvugt at (bvadd at span))
(and (bvuge (bvadd at delta) at)
(bvule (bvadd (bvadd at delta) reach) (bvadd at span))))
1
0)
(result))))
;; A bounds check inside a loop whose bytes one check in front of the loop has already covered.
;;
;; `at` and `span` are the address and the size of the check the pass is about to put in the
;; preheader, `far` is how far past that address the last iteration reads, and `reach` is the size
;; of the access inside the loop. `delta` is which iteration, and it is the one thing here the
;; compiler does not have as a number, which is the point: the rule is asked once and the answer
;; covers every iteration.
;;
;; The guard is the same containment in byte counts the rule above is guarded by, and it is the same
;; because it is the same question asked of the furthest iteration. What the rule adds is that the
;; furthest one fitting is enough for all of them, and that is the step the pass would otherwise be
;; making on its own with nobody checking it.
;;
;; The bounds on the numbers are there for the reason the file comment gives. Four gigabytes is past
;; the extent of any loop a real program writes and far short of where the compiler's `i128` reading
;; of the guard and the solver's sixty four bit reading part company. A loop that sweeps further
;; than that keeps its check.
(rule (discharge (swept.i64 (value.i64 at)
(iconst.i64 span)
(iconst.i64 far)
(iconst.i64 reach)
(value.i64 delta)))
(if (and (>= far 0) (<= far 4294967296)
(>= reach 0) (<= reach 4294967296)
(>= span 0)
(<= (+ far reach) span)))
(iconst.i64 1)
(spec (= (ite (or (bvugt at (bvadd at span))
(bvugt delta far)
(and (bvuge (bvadd at delta) at)
(bvule (bvadd (bvadd at delta) reach) (bvadd at span))))
1
0)
(result))))