Exercise 19. A digital receipt

An exercise for the evidence page. The page’s policy admits the issue desk’s paper receipt. The archive launched a portal, and returns are now confirmed also by the portal’s digital receipt, verified by the same registry.

Setup. Extend the policy: a “digital receipt” document issued by the portal and verified by the registry is admitted as return support. The same digital receipt issued by the issue desk is not admitted: each document kind has its own publisher.

Hint. A document’s soundness and a support’s admission are two different rules, with the publisher in both conditions. A new document kind means a new soundness rule and a new admission rule, not editing the old ones.

Below is the solution. Try it yourself first.

Solution

The header and norm from the page, transport relations unchanged:

Arxo Law

language "law.core" version "0.2";
package tutorial.archive version "0.11.1";
namespace "urn:law:tutorial:archive";

entity Person;
entity ReturnReceipt;

relation document_lent(p: Person) kind empirical;
relation document_returned(p: Person) kind empirical;
relation loan_closed(p: Person) kind institutional;

rule LoanClosed strict {
    for p: Person;
    when document_lent(p) and document_returned(p);
    then loan_closed(p);
}

relation ev_edge(edge: Text, document: Text, link: Text) kind empirical;
relation ev_issuer(document: Text, issuer: Text) kind empirical;
relation ev_available(document: Text) kind empirical;
relation ev_authentic(document: Text, verifier: Text, outcome: Text) kind empirical;
relation doc_kind(document: Text, kind: Text) kind empirical;
relation doc_reader(document: Text, reader: Person) kind empirical;
relation edge_reader(edge: Text, reader: Person) kind empirical;
relation edge_is_return(edge: Text) kind empirical;
relation sound_receipt(document: Text) kind institutional;
relation sound_portal_receipt(document: Text) kind institutional;
relation accepted_support(edge: Text) kind institutional;

const ARCHIVE_DESK: Text = "urn:tutorial:archive:reading-desk";
const ARCHIVE_PORTAL: Text = "urn:tutorial:archive:portal";
const ARCHIVE_REGISTRY: Text = "urn:tutorial:archive:registry";

The page’s rules plus a portal pair:

Arxo Law

rule SoundReceipt strict {
    for d: Text;
    when ev_available(d)
      and ev_issuer(d, ARCHIVE_DESK)
      and ev_authentic(d, ARCHIVE_REGISTRY, "verified");
    then sound_receipt(d);
}

rule AcceptReturnReceipt strict {
    for edge: Text;
    for d: Text;
    for p: Person;
    when ev_edge(edge, d, "supports")
      and edge_is_return(edge)
      and edge_reader(edge, p)
      and sound_receipt(d)
      and doc_kind(d, "return_receipt")
      and doc_reader(d, p);
    then accepted_support(edge);
}

rule SoundPortalReceipt strict {
    for d: Text;
    when ev_available(d)
      and ev_issuer(d, ARCHIVE_PORTAL)
      and ev_authentic(d, ARCHIVE_REGISTRY, "verified");
    then sound_portal_receipt(d);
}

rule AcceptDigitalReceipt strict {
    for edge: Text;
    for d: Text;
    for p: Person;
    when ev_edge(edge, d, "supports")
      and edge_is_return(edge)
      and edge_reader(edge, p)
      and sound_portal_receipt(d)
      and doc_kind(d, "digital_receipt")
      and doc_reader(d, p);
    then accepted_support(edge);
}

The policy lists all four rules:

Arxo Law

evidence policy ArchiveReturnEvidence {
    profile "law.core.evidence-policy/0.1";
    accepts accepted_support;
    protects document_returned;
    input edge      ev_edge;
    input issuer    ev_issuer;
    input available ev_available;
    input authentic ev_authentic;
    field kind   doc_kind;
    field reader doc_reader;
    arg 0 edge_reader;
    target document_returned edge_is_return;
    rule SoundReceipt, AcceptReturnReceipt, SoundPortalReceipt, AcceptDigitalReceipt;
}

The first test is the portal’s digital receipt:

Arxo Law

test "электронная квитанция портала проверена реестром — возврат установлен" {
    given {
        context {
            decision_time @2026-04-10T09:00:00+05:00;
            knowledge_time @2026-04-10T09:00:00+05:00;
            legal_time @2026-04-10;
            timezone "Asia/Almaty";
            evidence_policy ArchiveReturnEvidence;
        }
        assert document_lent(entity_ref("urn:tutorial:ivanova")) {
            id "assert-lent";
            origin case_input;
        }
        evidence ERECEIPT: ReturnReceipt {
            id "doc-ereceipt";
            status verified;
            issuer "urn:tutorial:archive:portal";
            observed_at @2026-04-02T15:00:00+05:00;
            recorded_at @2026-04-02T15:00:05+05:00;
            valid [@2026-04-02, infinity);
            content_hash "sha256:2222222222222222222222222222222222222222222222222222222222222222";
            kind "digital_receipt";
            reader entity_ref("urn:tutorial:ivanova");
        }
        verification VERECEIPT {
            evidence ERECEIPT;
            document_hash "sha256:2222222222222222222222222222222222222222222222222222222222222222";
            verifier "urn:tutorial:archive:registry";
            outcome verified;
            recorded @2026-04-03T10:00:00+05:00;
        }
        support ERECEIPT supports document_returned(entity_ref("urn:tutorial:ivanova"));
    }
    evaluate truth(document_returned(entity_ref("urn:tutorial:ivanova")));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}

The test name reads: “The portal’s digital receipt is registry-verified — return is established.”

Check

Two tests in tests/49-exercise-evidence.lawtest: the portal receipt admitted; the same receipt with the “issue desk” publisher not admitted, return not established. The second test is the task’s point: a document kind and its publisher are linked by the soundness rule, and a right-kind document from a wrong publisher is declined silently, without error.

What the exercise teaches. An evidence policy does not “trust the publisher” at large: it lists rules, each binding a document kind to who may issue and who may verify it. Extending a policy means adding rules and entering them in the list, not loosening the old ones’ conditions.