Module smt 

The IR’s meaning as an SMT-LIB obligation: two graphs compute the same values for every input, and for every meaning of the ops neither pins down.

eval runs a graph on numbers; this module runs it on terms. Every tensor a step starts with is an array of unknown values. A primitive that only moves values — a head slice, a row taken, rows gathered, a transpose, a join, rows written into a table — is the index map it is. Every other primitive is a function nothing is known of but that it is one: of its operands’ values, the same for every op of the same shape. An operand is read whole or as a part of every unit, a result lands in its own buffer or in rows or units of a table, and a fused op runs its parts and keeps what it writes outside itself, exactly as the evaluator does. Every array is zero past its length, so two arrays are equal exactly when their values are.

Terms are shared: two graphs that compute a value by the same ops in the same way compute the same term, and that equality needs no solver. Two terms that are one open function of operands that pair up are equal when the operands are; what is left are the pairs that differ in more — a part read in place where a copy was read, a result stored into a table’s rows where a row write copied it — and each is a lemma asking that the two be equal arrays, every subterm both share standing for any values. The indices a step reads rows by are assumed in range where the program it was lifted from reads them, and so is every interval the program proves of an integer it starts with; the rewritten graph’s own reads must then be in range too.

An Obligation is SMT-LIB 2 text, printed the same way every time from the same two graphs: the tensors compared, and lemmas whose premises a solver finds satisfiable and whose goals make them unsatisfiable exactly when the rewrite keeps the meaning. A proof checked once is pinned by the text’s digest and re-checked without a solver until the graphs change.

Structs

Lemma

One step of a proof a solver checks: SMT-LIB 2 premises — the terms it reads and the facts it assumes — and a goal asserting that two terms differ, or that a read strays out of range. The premises are satisfiable, so nothing follows from them vacuously; with the goal they are not, exactly when the step holds.

Obligation

What two graphs give a solver. A tensor both keep that the two graphs compute by one term needs no proof; one they compute by different terms is equal when the open functions are applied to equal operands, down to the pairs of terms that differ in more than their operands — an index map, a store, a value only one side computes. Each such pair is a lemma, its terms defined down to the subterms both share, which stand for any values; so is every read of the rewritten graph that its facts must keep in range.

Enums

SmtError

Why two graphs give no obligation.

Functions

identity

The obligation that two programs compute every tensor both keep alike when their products, elementwise sums and products and scales are computed exactly — an algebraic identity at the shapes the programs declare. Every other op is left open as obligation leaves it.

obligation

The obligation that rewritten means what reference means: for every input and every meaning of the ops the meaning leaves open, wherever the reference’s reads are in range, the rewritten graph’s are too and every tensor both keep holds the same values. A tensor of one name is the same tensor in both.