Evaluation

Generated from the module documentation of crates/canon/src/eval/mod.rs.

Deterministic evaluation of a case under a compiled protocol (design § 8, § 13).

evaluate_with is a pure function of a compiled protocol (Ir), a canon-case/1 case snapshot, a set of canon-evidence/1 records and the inputs a caller supplies (Supplied): canon-authority/1 authority decisions (--authority), the evaluation instant (--at) and canon-decisions/1 explicit decisions (--decisions). evaluate is the same with nothing supplied. It reads nothing else: no clock, network, filesystem, credentials or implicit latest. Its result is a canon-decision/1 Decision giving every declared claim the value true, false or unknown, each declared obligation open or discharged, each declared action admissible, approval-required or blocked, and each declared outcome legitimate or blocked (the sections below), or a Refusal when the inputs do not fit the protocol. render is the decision's one serialization: canonical JSON, the serialization canon-ir/1 uses.

Three-valued claims

A claim's value is its true_when predicate's value over the evidence set:

• An evidence match reads the records of its kind. One that names a subject reads only the records about that artifact: a record about another artifact, even at that artifact's current revision, is not of the match and neither establishes nor contradicts it (CANON-EVIDENCE-003). One that names no subject reads records about any artifact. One that demands independence (independent_on: [D, ...]) reads only the records that name a producer the case's independence map lists on every dimension D: any other record of its kind and subject is not of the match, whatever its result, so it neither establishes nor contradicts it (CANON-INDEPENDENCE-001, independence.rs). "Records of the kind" below are the records the match reads.
• An evidence match without a result is true when a record of the kind exists and unknown when none does.
• An evidence match with a result is unknown when no record of the kind exists, false when records of the kind exist and none has the result, true when every record of the kind has that result, and unknown when records of the kind disagree (some with the result, some without): conflicting evidence neither establishes the predicate nor by itself contradicts it.
• all is false when a member is false, otherwise true when every member is true (an empty all is true), otherwise unknown.
• any is true when a member is true, otherwise false when every member is false (an empty any is false), otherwise unknown.
• not swaps true and false and keeps unknown.
• A claim reference is three-valued: {claim: c} and {claim: c, is: true} are c's own value, and {claim: c, is: false} is not of it, so a claim built on c is unknown exactly when the evidence leaves c unknown and is never false for want of evidence. {claim: c, is: unknown} asks whether c is undecided, and is itself decided: true when c is unknown, false otherwise.
• An input test {input: s, in: [...]} is true when the case's value of the input s is one it lists and false otherwise. A case gives every input the protocol declares a value (the case check refuses one that does not), so an input test is never unknown: inputs are configuration fixed when the case opens, not evidence.
• An order form, {first: {kind: K, result: R}}, {before: {first: K1, then: K2}}, {after: {first: K1, then: {kind: K2, result: R}}} or {since: {last: K1, then: {kind: K2, result: R}}}, reads the evidence history instead: every record of its kinds (about its subject when it names one) the evidence check accepted, the records the exclusion stages set aside included, ordered by observed_at. first is whether the first record of K has result R; before whether the first record of K1 was observed strictly before the first of K2; after whether a record of K2 with result R was observed strictly after the first record of K1; since whether a record of K2 with result R, at the subject revision of the latest record of K1, was observed after it. Each is unknown while the order it reads is not established, as with no record or a compared record without observed_at; the predicate's reference in protocol/1 gives every rule (CANON-ORDER-001, CANON-ORDER-002, CANON-ORDER-004). No record is listed in excluded_evidence because of an order form.
• The form over the child cases, {children: {in: [O, ...]}} (story:case-composition), reads every case_outcome record the evidence check accepted, as the order forms read the history, one per child case: its child_case names the child and its result the child's outcome, open while the child runs. It is unknown with no record, false when a record's outcome is neither listed nor open (a child that ended outside the set), otherwise unknown while a child is open and true when every child ended with a listed outcome (CANON-COMPOSE-001). No record is listed in excluded_evidence because of it.

unknown and false are never collapsed, and only true satisfies a positive requirement.

Refusals

Inputs are checked before any claim is evaluated, in this order, and the first problem found is the refusal: the compiled protocol's depth (a predicate nested more than MAX_IR_DEPTH levels, itself or along the claims it tests, as predicate-too-deep, and claims that test each other in a cycle as claim-cycle; see "Depth" below), the case snapshot's format, its identifiers (case id, protocol id, the case revision when given, then each artifact id and revision in the order written), its protocol against the compiled protocol's, each artifact it lists (declared by the protocol, listed once), each artifact the protocol declares (listed by the case), each case input it gives, in the order written (its id and value identifiers, then declared by the protocol, else undeclared-input, given once, else duplicate-identifier, and its value declared by the input, else undeclared-input-value, naming the input and the value), each input the protocol declares (given by the case, else missing-input, naming it), each producer its independence map lists, in the order written (an identifier, listed once, else duplicate-identifier, and each dimension listed for it an identifier, listed once for it, else duplicate-identifier, and declared by the protocol, else undeclared-dimension, naming the producer and the dimension); then each evidence record in the order given: its format, its identifiers (id, kind, subject, subject revision, then each upstream artifact and revision in upstream_revisions, then its producer and its child_case when given), its observed_at when given (an instant, a fraction of one to nine digits allowed, else invalid-instant), its id (used once in the set), its kind (declared by the protocol) and each upstream artifact (declared by the protocol, else undeclared-artifact, naming the record and the artifact; named once, else duplicate-identifier), then, for a case_outcome record, its child case (named, else missing-child-case) and its outcome (a result, else missing-child-outcome), and for a record of any other kind no child case (else misplaced-child-case); then, over the whole set, one case_outcome record per child case, whatever its revision (else duplicate-child-case, naming the least such child and its records in evidence-id order, citing each). A record's subject and subject revision are checked here as identifiers only; the revision-binding stage reads them. Every refusal of a record names it (evidence `e2` format is `canon-evidence/2`, expected `canon-evidence/1`, evidence `e2` kind identifier `k k` is empty or …), and cites it (Refusal::evidence), here and in the revision-binding stage below, so a caller that read the records from files can name the file of each (canon evaluate does).

A case snapshot or evidence record that is not a document of its format is refused when it is read (read_case, read_evidence), before any of this, as malformed-input; a required key left out is named (missing field `subject`), and an evidence record is named by its id when it has one (evidence `e2` is not a canon-evidence/1 document: missing field `subject`).

Then the supplied inputs are read, in this order: the authority decisions (--authority), the evaluation instant (--at) and the explicit decisions. The authority decisions are read by authority.rs as canon-authority/1, refused as the section "Authority decisions" below says. The instant is read by freshness.rs and refused as invalid-instant when it is not one. The explicit decisions are read by decisions.rs as canon-decisions/1, refused as the section "Explicit decisions" below says.

Then the exclusion stages run, in pipeline order: revision binding, freshness, invalidation. Each may refuse the inputs it reads. Revision binding checks each record in the order given: a record whose subject the protocol does not declare is refused as undeclared-artifact, naming the record and its subject (evidence `e1` is about artifact `x`, which the protocol does not declare), and a record bound to a revision of its subject that is not the case snapshot's current one is excluded as revision_mismatch. Freshness refuses a max_age it cannot read (invalid-max-age) and excludes a record older than its kind's max_age at the evaluation instant as expired. Invalidation refuses a rule whose upstream artifact the case snapshot does not name, which only an IR a caller builds can hold, as undeclared-artifact, and invalidates, for the claims each rule names and every claim built on one of them, the records that recorded a revision of the rule's upstream artifact other than the case snapshot's current one (invalidation.rs, CANON-INVALIDATION-001).

Then claims are evaluated.

Last, the outcomes section checks the case snapshot's termination: one naming an outcome the protocol does not declare is refused as undeclared-outcome, naming the outcome; then an explicit decision taken for an outcome the protocol does not declare is refused as undeclared-outcome, and one taken for a declared outcome that does not require a decision of its name as undeclared-decision, each naming the decision and the outcome; and a termination naming a declared outcome that is blocked as illegitimate-termination, naming the outcome and its status (CANON-OUTCOME-001).

Depth

read_ir refuses an IR whose arrays and objects nest deeper than MAX_IR_DEPTH (4096) before parsing it. Reading and claim evaluation recurse along the nesting of the predicates, so they run on a thread of their own with a stack sized for that bound (DEEP_STACK): an IR at the bound reads and evaluates from any caller's thread.

Claim evaluation also recurses through each claim test into the predicate of the claim it tests, so the bound applies to a claim's effective depth: a predicate is one level and each all, any or not around it one more, and a claim test at level n reaches n plus the effective depth of the claim it tests. evaluate_with takes any Ir a caller builds and checks the bound first, before any step recurses (depth.rs), computing each claim's effective depth once, after the claims it tests, without recursion. It refuses as predicate-too-deep an obligation, action, outcome or claim whose own predicate nests more than MAX_IR_DEPTH levels (claim `c` true_when nests predicates deeper than 4096), and a claim whose effective depth is more than MAX_IR_DEPTH, naming the claims of the chain that reaches it (claim `c1` true_when nests predicates deeper than 4096 through the claims it tests: c1 -> c2 -> c3). Claims that test each other in a cycle — which canon compile never produces, but a caller can build — have no effective depth and are refused there as claim-cycle, naming the claims from the first one reached again, in the order evaluation reaches them: claims test each other in a cycle: c -> d -> c. Each level of the JSON text is at least one predicate level, so read_ir's bound holds every predicate of an IR it returns within the bound; a chain of claims, each within it, can still exceed it, and canon compile compiles such a protocol, so an IR read_ir returns can still be refused here. Dropping a caller's IR is the caller's own recursion.

The pipeline

evaluate_with runs the same steps for every evaluation, each in the file that owns its concept; this module holds only the order:

1. check the compiled protocol's depth (depth.rs), the case snapshot (case.rs) and the evidence set (evidence.rs);
2. read the supplied inputs: authority decisions (authority.rs), the evaluation instant (freshness.rs) and explicit decisions (decisions.rs);
3. run the exclusion stages in order: revision binding (binding.rs), freshness (freshness.rs), invalidation (invalidation.rs). Each sees only the evidence the stages before it left. Revision binding and freshness return the records they exclude from every claim, with their reason; invalidation returns, for each claim, the records it keeps from that claim alone;
4. evaluate every claim over the evidence left (claims.rs), and its order forms and forms over the child cases over every record the evidence check accepted (order.rs, composition.rs), each in its own context: no evidence match in its evaluation reads a record invalidated for it, including the matches of every claim it tests, which are evaluated for that use without the records invalidated for either; the value reported for a tested claim is its own. Each claim's excluded_evidence lists, in evidence-id order, every excluded record of a kind the claim reaches: a kind an evidence match in its own predicate names, or one a claim it tests reaches, through any number of claim references. A match that names a subject reaches its kind only for records about that artifact: a record about another artifact does not match it, so it is not listed under a claim that reaches its kind only through such a match. A record excluded from a claim is excluded from every claim built on it. A record invalidated for a claim is listed under it, with the reason invalidated, when an evidence match the claim reaches reads it, and under no claim it was not invalidated for. Any other record is listed under a claim, with the reason not_independent, when an evidence match the claim reaches would read it by kind and subject and none of those matches accepts its producer (independence.rs): a match that demands independence keeps it out, and no match demanding less reads it. Each record is listed once, with the first of these reasons that applies;
5. the obligations, actions and outcomes sections (obligations.rs, actions.rs, outcomes.rs), then the explanation (crate::explain). Each section evaluates its predicates with the one evaluator claims use (claims::predicate): discharge and applicability predicates over the claim values, action preconditions and outcome requirements over the claim values and the evidence left after step 3 (their order forms and forms over the child cases over every record accepted), each with the case's input values, which every input test reads. The invalidation stage keeps a record from claims only, so these predicates' own evidence matches read it. An outcome that requires an explicit decision is decided by the explicit decisions instead.

Revision binding excludes a record bound to another revision as revision_mismatch, and freshness a record older than its kind's max_age at the evaluation instant as expired, each listed as excluded under each claim that reaches its kind through a match that reads it, as step 4 says. Invalidation keeps a record from the claims an invalidation rule names and every claim built on one of them, throughout their evaluation, as invalidated, listed under each of those claims that reaches a match reading it; every other claim, even one reading the same kind, reads the record and does not list it. The obligations, actions and outcomes sections are written as the next section says, and every decision carries an explanation (crate::explain).

Sections

A section is written only when the protocol declares something it reports on: a protocol that declares no obligation has no obligations key, and likewise for actions and outcomes.

• obligations is an array with one {"id": <obligation>, "status": <status>} entry per declared obligation, in identifier order. An obligation with an applicable_when predicate is not_applicable when it is false over the claim values and the case's inputs. Otherwise the status is discharged when the obligation's discharged_when predicate is true over the claim values, whatever its applicability; unknown and false both leave it open (CANON-OBLIGATION-001). An open obligation whose applicability is unknown has "reasons" naming what is unknown, written as an action's reasons are (CANON-INPUT-001).
• actions maps each declared action to its status and, unless it is admissible, the reasons that decide it. blocked when the precondition is not true: each claim test and evidence match that decides it is a reason, {"claim": <id>, "value": <the claim's value>} or {"evidence": <kind>, "present": <whether a record the match reads applies>}, with "subject": <artifact> added when the match names one (a record about another artifact is not read by it), then each input test that decides it, {"input": <id>, "value": <the case's value>}, then each order form that decides it, {"after": <kind>, "then": <kind>, "result": <result>, "value": <its value>}, {"before": <kind>, "then": <kind>, "value": <its value>}, {"first": <kind>, "result": <result>, "value": <its value>} or {"since": <kind>, "then": <kind>, "result": <result>, "value": <its value>}, with "subject" added when it names one, then each form over the child cases that decides it, {"children": [<outcome>, ...], "value": <its value>}, or {"requirement": "unsatisfiable"} when none does. blocked too when the precondition is true and the authority decisions deny a capability the action requires, each a reason {"capability": <id>, "decision": "denied"}. approval-required when the precondition is true, nothing is denied and some required capability is not decided, each a reason {"capability": <id>, "decision": "none"}. admissible when the precondition is true and every required capability is granted (CANON-AUTHORITY-001).
• outcomes maps each declared outcome to {"status": "legitimate"} when its requires predicate is true over the claim values and the evidence left, and otherwise to {"status": "blocked", "reasons": [...]}. Its reasons follow the one rule an action precondition's do, and are written the same way: in an all that is false, only its false members decide it, with polarity carried through not. An outcome that requires an explicit decision (requires: decision: <name>) is legitimate only when an explicit decision of that name, for that outcome, was taken at the case snapshot's revision, and its entry then records who decided (design § 37): {"status": "legitimate", "decided_by": {"decision": <name>, "principals": [...]}}, every principal whose decision applied, sorted by Unicode code point; otherwise it is blocked with the one reason {"decision": <name>, "present": false} (CANON-OUTCOME-002). The case snapshot's termination is checked against it, as the refusals above say (CANON-OUTCOME-001).
• explanation is written for every decision: what the decision was computed from (design § 37), and why each claim that is not true, each open obligation, each action that is not admissible and each blocked outcome has its status, down to the evidence records that applied or were excluded. Its shape is given by crate::explain (CANON-EXPLAIN-001).

Authority decisions

--authority names a canon-authority/1 document: a YAML (or JSON) list of decisions, each a capability and whether it is granted, - {capability: finding.publish, decision: granted} (or denied). An empty list decides nothing. Canon grants nothing and resolves no identity: the caller decides and passes the decisions in. Refused, in this order: text that is not such a list, or an entry with another key, another decision or a missing key, as malformed-input, naming the entry by its position, counting from 1, and a missing key by name (entry 2: missing field `capability`); then, entry by entry, a capability that is not an identifier as invalid-identifier, and a capability decided a second time as duplicate-identifier.

Explicit decisions

--decisions names a canon-decisions/1 document: a YAML (or JSON) list of decisions, each naming the decision, the outcome it was taken for, the principal who took it and the case revision it was taken at, - {decision: explicitly_inconclusive, outcome: inconclusive, principal: lead-investigator, case_revision: c2}. An empty list decides nothing. Canon decides nothing and resolves no identity: the caller passes in the decisions that were taken. A decision applies only while its case revision is the case snapshot's revision: one taken at a superseded revision, or given for a snapshot without a revision, applies to nothing. Refused, in this order: text that is not such a list, or an entry with another key or a missing one, as malformed-input, naming the entry by its position and a missing key by name (entry 1: missing field `case_revision`); then, entry by entry, a decision, outcome, principal or case revision that is not an identifier as invalid-identifier, and an entry that repeats an earlier one exactly as duplicate-identifier, naming it; then, in the outcomes section and at any case revision, a decision for an outcome the protocol does not declare as undeclared-outcome, and one for an outcome that does not require a decision of its name as undeclared-decision.