;; 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))))
;; The same, for a loop whose extent the program works out rather than the compiler.
;;
;; `span` and `far` are values here and not numbers. The pass that asks this has a trip count it
;; cannot evaluate, so it builds the two of them in the preheader out of that count and puts the
;; result on the hoisted check as an operand, and what it has to say about them can only be said as
;; a hypothesis inside the formula rather than as a guard on the numbers.
;;
;; The three hypotheses are the three things the pass promises about what it built. `far` and
;; `reach` added do not wrap, `span` is at least that sum, and `delta` is somewhere between zero and
;; `far`. The first two are what the pass establishes by bounding the arithmetic before it emits
;; any of it: the count comes from a value narrower than the arithmetic, the step and the reach are
;; numbers, and the largest the whole thing can be is worked out in wider arithmetic and refused if
;; it does not fit. The third is the same statement about which iteration as in the rule above.
;;
;; No four gigabyte limit, because there is no `i128` reading of these to part company with the
;; solver's. Everything about `span` and `far` that the pass knows is written above, and the
;; solver's arithmetic on them is the machine's.
(rule (discharge (swept.sym.i64 (value.i64 at)
(value.i64 span)
(value.i64 far)
(iconst.i64 reach)
(value.i64 delta)))
(if (>= reach 0))
(iconst.i64 1)
(spec (= (ite (or (bvugt at (bvadd at span))
(bvult (bvadd far reach) far)
(bvult span (bvadd far reach))
(bvugt delta far)
(and (bvuge (bvadd at delta) at)
(bvule (bvadd (bvadd at delta) reach) (bvadd at span))))
1
0)
(result))))