Who Reported It and What It Confirms

In the last chapter the information about behaviour was already present in the case. We asked what follows from it and how it bears on the duty. Now take one step back: why should the starting assertion be accepted at all?

Imagine an employee asking to be reimbursed for a purchase. He presents an approval, a receipt, and a bank confirmation. At first glance everything is in place. But the confirmation concerns another purchase. The document may be genuine, its content truthful, and yet it may leave the payment we need to establish unconfirmed.

The purchase we are checking

Take the study package expense-evidence. It states a rule for a hypothetical organization: an expense meets the reimbursement conditions if the purchase is approved, its amount and payment are established, the employee who incurred the expense is known, and the amount does not exceed 10,000 roubles[^chapter-11-package].

A purchase has the type Purchase, an employee Employee, and a monetary amount the type Money, which pairs an amount with a currency. The rule looks like this:

rule Reimbursement strict {
    for p: Purchase;
    for e: Employee;
    for a: Money;
    when approved(p)
      and expense_amount(p, a)
      and paid(p)
      and incurred_by(p, e)
      and a <= REIMBURSEMENT_CAP;
    then reimbursable(p, e);
}

REIMBURSEMENT_CAP is a constant with the value 10000 RUB. The relation incurred_by(p, e) links the purchase to the employee. Three other premises speak of approval, amount, and payment: approved, expense_amount, paid.

The conclusion reimbursable(p, e) means the expense matches the recorded reimbursement conditions. It does not report that the money has already been transferred to the employee. As in the last chapter, the ground for acting and the act itself differ.

In our example the purchase has the identifier urn:demo:purchase:42, the employee urn:demo:employee:7. For brevity we will call them purchase 42 and employee 7. The link between them is recorded with an ordinary assert incurred_by(...). Approval, amount, and payment require documentary grounds.

A document is not yet a payment confirmation

Consider the bank document B92 from the right-payment scenario. Inside given it is described by a separate block:

evidence B92: BankConfirmation {
    id "doc-B92";
    status verified;
    issuer "urn:demo:issuer:bank-alpha";
    observed_at @2026-02-06T08:00:00Z;
    recorded_at @2026-02-06T08:00:04Z;
    valid [@2026-02-06, infinity);
    content_hash "sha256:9292929292929292929292929292929292929292929292929292929292929292";
    kind "bank_confirmation";
    purchase entity_ref("urn:demo:purchase:42");
    employee entity_ref("urn:demo:employee:7");
    amount 10000 RUB;
}

After evidence come the name B92 and the evidence kind BankConfirmation. The body lists its particulars. id states the entry’s persistent identifier, issuer names the document’s issuer, content_hash holds the fingerprint of its content. The dates say when the information was observed and recorded; valid states the period during which the document is in effect.

The last four fields describe the content: a bank confirmation, purchase 42, employee 7, the amount of 10,000 roubles. That is the study document’s structured entry; no scanned text is recognized in this example. The hashes are left in their original form so the excerpts can be matched exactly against the files.

The document already carries status verified: it is marked as checked. But that one field is not enough for acceptance. The verification result is recorded separately:

verification VB92 {
    evidence B92;
    document_hash "sha256:9292929292929292929292929292929292929292929292929292929292929292";
    verifier "urn:demo:verifier:audit-desk";
    outcome verified;
    recorded @2026-02-10T10:00:03Z;
}

verification VB92 refers to B92 and names the verifier through verifier. outcome states the positive result, recorded the moment of recording. The document_hash value must match the document’s content_hash. That is how the verification result is tied to particular content.

The model works with the supplied verification result: it does not itself call the bank or certify the signature. Besides the hash match, what counts is whether the verification record was available at the knowledge time. The admissible verifier is named by the package’s rules[^chapter-11-verification].

Now state what B92 is offered as evidence for:

support B92 supports paid(entity_ref("urn:demo:purchase:42"));

This declares a support link for the paid assertion about purchase 42. After support comes the document; after supports, the assertion it is offered to support. So far we have only proposed the link: “this document is offered to confirm this purchase’s payment”. Whether to admit or reject such a support is still to be decided.

We now have three separate entries: what the document says, the result of verifying it, and the assertion it is offered to support. Because they are separate, each link can be examined on its own.

How a support link is admitted

The package holds an evidence-admission policy, ExpenseEvidenceV1. A policy here means a declared set of requirements for admissible supports. The scenario chooses it in the context:

context {
    legal_time @2026-03-01;
    decision_time @2026-03-01T00:00:00Z;
    knowledge_time @2026-03-01T00:00:00Z;
    timezone "UTC";
    evidence_policy ExpenseEvidenceV1;
}

Leave the dates as in the original example. The new line evidence_policy ExpenseEvidenceV1 says which admission policy applies in this calculation.

In the policy declaration’s body there are two lines stating its main task. An excerpt follows:

accepts accepted_support;
protects approved, expense_amount, paid;

protects lists the protected relations. Under the chosen policy they cannot be confirmed by an ordinary assert entry: an admitted support is needed. accepts names the relation expressing the admission decision. If the policy’s rules conclude accepted_support for the given support, it is allowed to back the assertion.

For such rules to read the document, the policy binds its fields and the support’s properties to relations in its own vocabulary. In the full declaration the lines input, field, arg, and target serve that purpose. Here an edge is the support link itself. Use the following table as a map while reading the next two rules; the names fall into four groups:

First the document itself is checked:

rule SoundDocument strict {
    for d: Text;
    when ev_available(d)
      and ev_current(d)
      and ev_status(d, "verified")
      and ev_authentic(d, TRUSTED_VERIFIER, "verified");
    then sound_document(d);
}

It must be available at the knowledge time, be valid on the chosen date, carry the verified status and a verification result from TRUSTED_VERIFIER. In this package the constant names the audit-desk verifier. The document’s status is one of the premises; it does not replace the other three.

Then the document’s link to the payment is considered:

rule AcceptPayment strict {
    for edge: Text;
    for d: Text;
    for p: Purchase;
    for a: Money;
    for e: Employee;
    when ev_edge(edge, d, "supports")
      and edge_is_paid(edge)
      and edge_purchase(edge, p)
      and sound_document(d)
      and doc_kind(d, "bank_confirmation")
      and doc_issuer_ok_bank(d)
      and doc_purchase(d, p)
      and doc_amount(d, a)
      and claim_amount(p, a)
      and doc_employee(d, e)
      and claim_employee(p, e);
    then accepted_support(edge);
}

The variable edge denotes the support’s address, d the document’s. The first three premises establish that the document is tendered as confirmation of the payment for purchase p. The next ones check its validity, kind, and issuing bank.

Then comes the crucial match. The variable p in doc_purchase(d, p) is the same variable as in edge_purchase(edge, p). So the purchase in the document must coincide with the purchase in the assertion. Likewise one variable a links the amounts, and e the employee. Both amount and employee must also match those established for this purchase by the receipt.

Only once all conditions hold does the rule conclude accepted_support(edge). A particular support is admitted: one and the same document may serve for one assertion and not for another.

A genuine document about someone else’s purchase

In the wrong-payment scenario, approval A17, receipt R25, and bank confirmation B91 are tendered. The first two documents concern purchase 42. B91 carries a positive verification result, but its purchase field states purchase 99. And the support offers it to confirm paid for purchase 42.

The AcceptPayment rule fails at the purchase match: doc_purchase(d, p) cannot hold for purchase 42 because B91 names purchase 99. The B91 support is not admitted. The paid(42) assertion stays NEITHER, as does the reimbursement conclusion. A mismatched document does not prove the payment never happened.

In right-payment, B92 about the needed purchase is added. Its support passes the rule. Now the payment receives TRUE_ONLY, and together with the remaining premises it lets us conclude reimbursable(42, 7).

The package’s demonstration shows each support’s admission and the refusal’s reason. Start it from the reader companion directory:

python3 packs/demo/expense-evidence/run_demo.py

In the first scene find B91 and the mismatched doc_purchase. In the second, the admitted B92 support. The following scenes show the confirmation’s removal and the case where, after one document’s removal, another matching support survives.

The tests themselves start like this:

law engine test packs/demo/expense-evidence/tests/reimbursement.lawtest --program \
  packs/demo/expense-evidence/clir/expense-evidence.lawir.json --imports \
  contexts/expense-evidence.json

For a separate explanation, keep in a copy the file header and one test right-payment. Replace the reimbursement question with the payment question:

evaluate truth(paid(entity_ref("urn:demo:purchase:42")));

expect result_kind == PROPOSITION;
expect truth_status == TRUE_ONLY;
expect evaluation_status == COMPUTED;

Hand that copy to the explain command with the same program. The output’s start will be as follows; further grounds are omitted here:

paid(42): TRUE_ONLY
  support_admission  paid(42)

Author’s paraphrase of the engine output above (the package declares no English labels, so the output holds bare identifiers; what follows is the author’s free retelling): payment for purchase 42 is established (TRUE_ONLY); the support_admission node marks the support’s admission — the tendered bank confirmation passed the AcceptPayment rule with its premises, including the entries from the bank confirmation and the receipt.

The path to paid(42) therefore runs through both the tendered document and the rule that admits its support[^chapter-11-admission].

When confirmation is missing or conflicts

Delete from the right-payment copy only verification VB92. B92 itself and its support stay. Even the status verified inside the document survives. Yet SoundDocument now lacks the separate verification record, and the payment returns to NEITHER.

The third starting test tries to establish the payment directly, with no bank confirmation:

assert paid(entity_ref("urn:demo:purchase:42")) {
    id "assert-bare-paid";
    origin adjudicated;
}

Even origin adjudicated does not replace an admitted support for a protected relation. In this case paid and the reimbursement stay NEITHER. The policy imposes requirements on the grounds, and this assertion is subject to them too.

A conflict is also possible. The rule AcceptPaymentReversal from the same package admits a bank document of the bank_reversal kind as a refutation of payment. For such a link refutes is recorded instead of supports. If both supports are admitted for one purchase, paid receives BOTH.

That is this package’s way of presenting a payment’s reversal. The model keeps both supports of one assertion; the events’ order and the later state’s choice are not described here. So a refutation’s appearance does not automatically delete the earlier confirmation.

In the last row the reimbursement rule’s positive premise paid(p) is not established without contradiction. Not deriving the conclusion does not amount to denying reimbursable. We return to the familiar four states, but now we can trace them to documents.

Try checking the ground

Start each trial with a fresh right-payment copy, keeping the file header and the remaining documents.

1. Delete verification VB92, keeping the old TRUE_ONLY expectation. Account for the mismatch. Then check the expected NEITHER separately for payment and reimbursement.
2. Restore the verification and delete only the support B92 line. Why does the document with correct particulars no longer establish the payment?
3. Add a separate document about a payment reversal of the bank_reversal kind, with its own name, address, and matching verification record. Keep the purchase, amount, and employee. Use AcceptPaymentReversal as your checklist: check its document and matching premises, including the verifier and the hash linking the verification to the new document. Tender it through refutes for paid. Predict both result lines: the payment and the reimbursement conditions. Then delete B92 with its verification and support: which state remains for the payment?
4. Return to Kafka’s facts with evidence VDG_1915_TEXT, such as the assertion that the man requested entry. They state evidence but hold no policy decision shown here about admitting a support. Which links would have to be described to check such a fact’s grounds in a similar way?

The number of documents does not replace checking their content. Each support must answer its own question and pass the stated admission conditions. One more link remains to be considered in detail: exactly where in the source we can find the text that supports the model. That is the subject of the next chapter.

[^chapter-11-package]: The organization’s conditional example: the package description and the Reimbursement rule in expense-evidence.law. The money limit and conditions are stated for this teaching case only. [^chapter-11-verification]: The Arxo specification, §78.2.2–78.2.4: tying a verification result to a document’s content, knowledge time, and admission policy. The external verification result enters the model as input information. [^chapter-11-admission]: The whole SoundDocument, AcceptPayment, and AcceptPaymentReversal rules are in the package model; the document compositions in the scenarios. The admission report and its grounds are described in §78.2.6–78.2.9.