Answers with proofs

Read first: Fixpoints and worklists, Summarising a PERFORM

A model asked to read the source and answer gives prose: plausible, uncheckable, and sometimes drawn from what it remembers about a well-known program rather than from the program in front of it. This page keeps the model, but takes away its pen. It may only write rules. The answer is whatever those rules derive from the facts, and each row comes with the steps that derived it.

The example is a real question about CardDemo's transaction-add program, COTRN02C: before it writes a new transaction record to the transaction file, which fields typed on its screen does it check, and what kind of check is each? Count a check only if one of its outcomes can stop the write.

The pipeline

flowchart LR
    S["COBOL, JCL, CSD, BMS"] -->|parse and analyse| F["facts: CFG, byte flows, definitions, sinks, links"]
    Q["question in English"] --> A["model, blind to the source"]
    D["what each relation's columns mean"] --> A
    A -->|rules only| C["checker"]
    C -->|accepted| E["Soufflé"]
    F --> E
    E --> R["answer rows"]
    E -->|explain| P["a derivation per row"]

• Facts. The analysis's outputs are written out as typed rows: the control-flow graph's nodes and edges, the atoms of each test, which bytes each statement reads and writes, which definitions reach each use, which bytes go to a file, a screen or another program. They are written once, as relations, and never by the model.
• The model sees the question and the relations' documentation, not the source. It writes rules, runs them, reads the rows back and refines them.
• The checker refuses named constants. A quoted string in a rule is refused if the facts use it as the name or id of a program, node, paragraph, field, record, dataset, origin or sink, unless it is also one of the facts' fixed words, such as an edge kind. The one way in is a fact ground("phrase", value), and the phrase has to occur in the question: ground("transaction file", "TRANSACT") is allowed because the question says "transaction file". Any other fact, any .input and any #include but the schema's are refused too. Three things are not checked: the value in a ground fact, so ground("fields", v) passes for any field v; how much of the question the phrase is, so "t" passes; and numbers, so a rule can pick a node by its source line. A rule can therefore still keep or drop a row by name, through ground, or by number. Those were left to the reviewer; the final rules ground only the program and the transaction file.
• Every rule cites its reason. The model is told to put a line above each rule: // Q: and the words of the question it encodes, or // R: and the documentation of the relation it relies on. The checker does not enforce this; a reviewer reads it.

The rules the model wrote for this question split it into four parts, plus rules of the same shape for two more kinds of check, call and lookup:

The answer is 28 rows of (field, kind), for example (TRNAMTI, numeric), (TRNAMTI, value), (CARDNINI, lookup).

One row's derivation

Soufflé can print, for any row, the rule that produced it and the rows that rule used, down to facts. Here is (TRNAMTI, numeric), taken from the renamed run described below, with the names mapped back, node names shortened and the source lines added. The test is the second WHEN of the amount check:

           EVALUATE TRUE
               WHEN TRNAMTI OF COTRN2AI(1:1) NOT EQUAL '-' AND '+'
               WHEN TRNAMTI OF COTRN2AI(2:8) NOT NUMERIC        <- t
               ...
                   MOVE 'Y'     TO WS-ERR-FLG                  <- m
                   ...
                   PERFORM SEND-TRNADD-SCREEN

checks(TRNAMTI, numeric)
├─ tested(TRNAMTI, t)          t reads TRNAMTI's bytes,
│                              filled by the map receive
├─ kind_of(t, numeric)         t's atom: CLASS NUMERIC
└─ stopping(t)
   ├─ outcome(t, next)         edge t → next WHEN, TRUE
   ├─ write_node(w)            FILE sink, file 'TRANSACT'
   ├─ reach(next, w)
   ├─ outcome(t, m)            edge t → m, FALSE
   └─ doomed(m)
      ├─ write_node(w)
      ├─ not write_node(m)
      └─ not reach(m, w)

w is WRITE-TRANSACT-FILE/0. The facts hold the test as IS NUMERIC; the source's NOT shows up in which edge is TRUE, so TRUE (numeric) goes on to the next WHEN and FALSE goes to the error branch. The rows without a note have derivations of their own, folded here; the two not rows have none.

Read bottom-up, it is the argument a reviewer would make by hand. If the amount's digits are numeric, control goes on to the next WHEN, which can still reach the write. If not, it goes to the MOVE 'Y', from which nothing reaches the write: the error branch performs SEND-TRNADD-SCREEN, which ends with EXEC CICS RETURN, so that PERFORM never comes back (see a paragraph that always leaves some other way). Every step is either a fact or a rule applied to rows above it.

The two leaves marked not are different in kind. Every other leaf is a row the analysis wrote down. A not leaf is a fact that is absent: no derivation of reach(m, …) exists. Datalog reads a missing fact as false, so this leaf is only as good as the completeness of the control-flow edges.

What the proof proves

Soufflé does not make derivations up. A row is output only if a derivation exists, so the proof is real: given these facts, these rules yield (TRNAMTI, numeric). Nobody has to trust the model about that.

What the proof does not show is that stopping means "one of its outcomes can stop the write". That is the model's reading of the question, written as a rule. So the review moves. One no longer checks the answer row by row against the source. One checks a handful of definitions against the question's words, and the citation line above each definition says which words it claims to encode. The derivation then shows, for each row, exactly which definitions it depended on.

Checking the rules

For this question, four checks were run:

• An answer key from the source alone, written before the model ran and compared row for row. The final run's 28 rows matched it exactly.
• Breaks. Fourteen one-rule mutations, each a plausible mistake: drop the reach condition from stopping, let any constant count as empty, follow PERFORM edges as plain flow. Nine of them changed the answer. Five did not, which says this program does not exercise those rules. Several different rule sets give the same answer here.
• Renamed facts. Every corpus name in the facts became Z and five digits, the same name everywhere. That removes the names a model could recognise CardDemo by. It leaves the values: literals and screen text such as 'Thank you for using CardDemo application...', 'Mainframe Modernization', 'Tran Amount' and ' must be numeric.' are still in the facts as written. The final run above is the renamed one.
• An adversarial hunt by a second agent, which was allowed to read the source, looking for a row that is wrong or a check that is missed. It found none, but found rules that were right only because of how this program happens to be laid out.

Where this shows up

• Questions people actually ask about legacy code are of this shape: where does this balance come from, which checks guard this write, which programs can a user reach from this menu. Each is a join over control flow, data flow and the resource definitions, which Datalog states directly.
• The same idea on the Java side. Program analysers such as Doop write points-to analysis as Datalog over facts extracted from bytecode, and CodeQL queries are a Datalog dialect over a database of the code. The difference here is who writes the query: a model, from an English question, under a checker that lets corpus names in only through ground facts whose phrase is in the question.

What goes wrong

• A missing fact turns a not leaf true. If the control-flow graph lacked an edge, say a handler a CICS condition jumps to, reach(m, …) would fail for a node that can in fact reach the write. doomed(m) would hold, and the answer would gain a check that does not stop the write, with a derivation Soufflé is happy to print. Rules that only add rows are safe against missing facts: they miss rows but add none. They are not safe against facts that claim too much, and some of cobble's do on purpose: a paragraph's end has a RETURN edge to the statement after every PERFORM of it, and a PERFORM whose range end no edge reaches keeps its edge to the next statement. A rule that follows those edges can derive a row no run gives. Rules with negation are only right if the relation they negate is complete. The remedy is for each relation to say what it leaves out.
• A gap in the facts can hide behind a right answer. The facts do not record which field a CICS READ uses as its key. The model's lookup rule stood in for it with "a screen value moved into the record the read fills". On this program that gives the right rows, because the key fields sit inside that record. On a program whose key is held elsewhere, the same rule would lose the row. The facts also drop reference modification: both amount tests above, on TRNAMTI(1:1) and TRNAMTI(2:8), are recorded as reading all twelve bytes of TRNAMTI, and the numeric test's text is plain IS NUMERIC. A rule cannot tell which part of a field a test looks at.
• The reading of the question is not proved. The answer key itself had to be corrected. Under the question's literal wording, a test counts only if one outcome reaches the write and another cannot. Two tests the key had first counted fail that. In one, the outcome that looks like a failure goes on to further tests that can still reach the write. The other runs only once the write is already ruled out, so neither of its outcomes can reach it. The rules were right, and the key was wrong.
• Facts computed elsewhere are trusted, not proved. Some relations are results of analysis, not syntax: the bytes each statement moves where, and which definitions reach each use, come from the analysis's own fixpoint. A derivation that uses them starts from those results and takes them on trust. For this question the model rebuilt reaching definitions itself, in rules, from the per-statement byte flows, so that part is inside the proof and only the flows are trusted. Rebuilding more of the analysis in rules brings more inside the proof, at the cost of speed.

In cobble

The facts stage (cobble-experimental-datalog-facts --run RUN_DIR --out FACTS_DIR) writes every relation as a Soufflé facts file, with a schema that declares them. A question is a .dl file that includes that schema, adds its rules and asks for its outputs. Running it is a plain Soufflé call, and adding -t explain opens the prompt where explain checks("TRNAMTI", "numeric") prints the derivation above. The blind model, the checker and the four checks are an experiment around the stage, not part of it.