Requirement Evaluation Trees (RET)

At a Glance

What: Binary and tri-valued requirement algebra with an explicit threshold primitive Why: Make gate logic explicit, auditable, and deterministic - no hidden rules Who: Developers and operators authoring complex gate requirements Prerequisites: Basic understanding of conditions (see condition_authoring.md)

Lowered/AOT Backend (RET)

RET now provides an additive lowered/AOT backend in ret-logic:

Compile once: Requirement<P> -> CompiledRequirement<K>
Evaluate fast paths at runtime:
- CompiledRequirement::eval
- CompiledRequirement::eval_block
- CompiledRequirement::eval_tristate (+ trace variant)
Export deterministic predicate-key dependencies:
- CompiledRequirement::predicate_keys()
Compute explanation-oriented residual/progress views:
- Requirement::residual
- CompiledRequirement::residual
Preserve compatibility:
- Tree-walk Requirement::eval* stays supported and unchanged.

This is domain-agnostic: domains supply deterministic key mapping (PredicateRegistry) and runtime key execution (PredicateRuntime). Residual/progress explanation additionally requires condition- or predicate-level progress implementations through ConditionProgressEval and PredicateProgressRuntime.

Compile-Time vs Runtime Ingestion

Source ingestion (RON, JSON, DSL, MCP payloads, etc.) does not change RET semantics. The difference is lifecycle:

Compile-time/load-time ingestion: parse + validate + compile once, store compiled artifact.
Runtime ingestion: parse + validate + compile when the gate arrives, then execute compiled artifact.

Both paths converge to the same algebra and compiled evaluator behavior when input requirements are equivalent.

Why RET?

Problem: How do you combine multiple evidence checks into a single gate decision?

Example scenario: “I want to deploy to production if:

Environment is ‘production’ AND
Tests passed AND
Coverage is above 85% AND
At least 2 of 3 reviewers approved”

Without RET: Bespoke code can still be deterministic and reviewable, but each implementation must independently establish its law, version identity, trace semantics, and conformance. The control flow is harder to inspect and compare as one closed algebra.

With RET: You express the logic as a tree structure:

{
  "requirement": {
    "And": [
      { "Condition": "env_is_prod" },
      { "Condition": "tests_ok" },
      { "Condition": "coverage_ok" },
      {
        "RequireGroup": {
          "min": 2,
          "reqs": [
            { "Condition": "alice_approved" },
            { "Condition": "bob_approved" },
            { "Condition": "carol_approved" }
          ]
        }
      }
    ]
  }
}

Benefits:

Explicit: Logic is visible in the scenario spec
Inspectable: The requirement law is explicit data rather than hidden control flow.
Deterministic: The same validated requirement and exact leaf truth assignment produce the same RET result.
Re-evaluable: Retained canonical requirement law and leaf inputs can be evaluated offline without re-querying providers. This RET property does not by itself establish complete Decision Gate semantic replay, accepted commit history, evidence authenticity, or nonrepudiation.

[Security]: Explicit gate logic narrows the hidden-control-flow surface; it does not prove that provider, comparator, admission, policy, transition, or dispatch behavior is benign. Current runpacks provide bounded integrity and audit/export evidence only.

Mental Model: RET Evaluation Tree

Here’s how a requirement tree is evaluated:

RET EVALUATION TREE (simplified)

Gate Requirement (tree structure)
  And
  |-- Pred(A) -> true
  |-- Pred(B) -> unknown
  |-- Not(C) -> false
  `-- RequireGroup (min: 2)
      |-- Pred(D) -> true
      |-- Pred(E) -> true
      `-- Pred(F) -> false

Strong Kleene Logic: And(true, unknown, true, true) -> unknown
(gate holds)

Evaluation order:

Leaf conditions evaluate to tri-state (true/false/unknown)
Operator nodes combine child outcomes via tri-state logic
Root node outcome determines gate result

Tri-State Outcomes

RET uses tri-state logic (not just true/false):

true: Gate passes (all requirements satisfied)
false: Gate fails (requirements contradicted)
unknown: Gate holds (requirements inconclusive)

Why tri-state? Gates fail closed: a gate only passes when the requirement evaluates to true. unknown outcomes prevent gates from passing until evidence is complete.

Example:

Gate: And(tests_ok, coverage_ok)
Conditions:
- tests_ok: true (tests passed)
- coverage_ok: unknown (coverage report missing)

Outcome: unknown (gate holds until coverage is available)

Core Operators

And

Semantics: All children must be true

Truth table (2 operands):

Left	Right	Result
true	true	true
true	false	false
true	unknown	unknown
false	(any)	false
unknown	true	unknown
unknown	unknown	unknown

Example:

{
  "requirement": {
    "And": [
      { "Condition": "tests_ok" },
      { "Condition": "coverage_ok" }
    ]
  }
}

Use case: Both tests and coverage must pass

Behavior:

All true -> true (gate passes)
Any false -> false (gate fails)
Otherwise -> unknown (gate holds)

Or

Semantics: Any child may be true

Truth table (2 operands):

Left	Right	Result
true	(any)	true
false	false	false
false	unknown	unknown
unknown	false	unknown
unknown	unknown	unknown

Example:

{
  "requirement": {
    "Or": [
      { "Condition": "manual_override" },
      { "Condition": "tests_ok" }
    ]
  }
}

Use case: Either manual override OR automated tests must pass

Behavior:

Any true -> true (gate passes)
All false -> false (gate fails)
Otherwise -> unknown (gate holds)

Not

Semantics: Invert child outcome

Truth table:

Input	Result
true	false
false	true
unknown	unknown

Example:

{
  "requirement": {
    "And": [
      { "Condition": "tests_ok" },
      { "Not": { "Condition": "blocklist_hit" } }
    ]
  }
}

Use case: Tests must pass AND blocklist must NOT be hit

Behavior:

true -> false
false -> true
unknown -> unknown (fail-closed: can’t confirm absence)

RequireGroup (Quorum)

Semantics: At least N of M children must be true

Parameters:

min: Minimum number of true outcomes required
reqs: Array of child requirements

Example:

{
  "requirement": {
    "RequireGroup": {
      "min": 2,
      "reqs": [
        { "Condition": "alice_approved" },
        { "Condition": "bob_approved" },
        { "Condition": "carol_approved" }
      ]
    }
  }
}

Use case: At least 2 of 3 reviewers must approve

Behavior:

Count true outcomes
If count >= min -> true (quorum reached)
If count + unknowns < min -> false (quorum impossible)
Otherwise -> unknown (quorum pending)

Truth table examples:

Outcomes	min	Result	Reason
[true, true, false]	2	true	2 true >= min (quorum reached)
[true, unknown, unknown]	2	unknown	1 true, can’t reach min yet
[true, false, false]	2	false	1 true, max possible is 1 < min
[true, true, unknown]	2	true	2 true >= min (already met)
[false, false, false]	2	false	0 true, impossible

[Developer]: See ret-logic crate for implementation. RequireGroup counts true/false independently (unknown is neither).

Condition (Leaf Node)

Semantics: Reference a condition by key

Example:

{
  "requirement": { "Condition": "tests_ok" }
}

Use case: Simple gate with single condition

Behavior:

Evaluates to the condition’s tri-state outcome
Condition must exist in RawScenarioSpec.conditions

Tri-State Propagation Rules

How unknown outcomes propagate through operators:

And Propagation

Operands	Result	Reason
`And(true, true, true)`	true	All requirements satisfied
`And(true, false, true)`	false	One fails -> And fails
`And(true, unknown, true)`	unknown	Can’t confirm all true yet
`And(false, unknown)`	false	One fails (short-circuit)
`And(unknown, unknown)`	unknown	Pending evidence

Rule: false dominates; all true yields true; otherwise unknown

Or Propagation

Operands	Result	Reason
`Or(false, false, false)`	false	All requirements failed
`Or(true, false, false)`	true	One succeeds -> Or succeeds
`Or(false, unknown, false)`	unknown	Can’t confirm all false yet
`Or(true, unknown)`	true	One succeeds (short-circuit)
`Or(unknown, unknown)`	unknown	Pending evidence

Rule: true dominates; all false yields false; otherwise unknown

RequireGroup Propagation

Outcomes	min	true count	unknown count	Result
[T, T, F]	2	2	0	true (min reached)
[T, U, U]	2	1	2	unknown (max 3, need 2)
[T, F, F]	2	1	0	false (max 1 < min)
[U, U, U]	2	0	3	unknown (max 3, need 2)
[F, F, F]	2	0	0	false (impossible)

Rule:

If true_count >= min -> true (quorum reached)
If true_count + unknown_count < min -> false (quorum impossible)
Otherwise -> unknown (quorum pending)

[LLM Agent]: When RequireGroup returns unknown, you need more evidence. Check which conditions are unknown and work to satisfy them.

Practical Use Cases

Simple Requirement: Both Conditions

Scenario: Deploy if tests passed AND coverage is above 85%

{
  "And": [
    { "Condition": "tests_ok" },
    { "Condition": "coverage_ok" }
  ]
}

Quorum Requirement: 2 of 3 Reviewers

Scenario: Merge PR if at least 2 of 3 reviewers approved

{
  "RequireGroup": {
    "min": 2,
    "reqs": [
      { "Condition": "alice_approved" },
      { "Condition": "bob_approved" },
      { "Condition": "carol_approved" }
    ]
  }
}

Exclusion Requirement: NOT Blocklisted

Scenario: Deploy if NOT blocklisted

{
  "Not": { "Condition": "blocklist_hit" }
}

Complex Requirement: (A AND B) OR C

Scenario: Deploy if (tests passed AND coverage OK) OR manual override

{
  "Or": [
    {
      "And": [
        { "Condition": "tests_ok" },
        { "Condition": "coverage_ok" }
      ]
    },
    { "Condition": "manual_override" }
  ]
}

RET in Monotone-DAG Topology

Scenario topology is not an outcome router. Each non-root stage carries one monotone prerequisite RET law over completed stage IDs. Those atoms are the sole source of its incoming dependency edges. For example, ship becomes ready after build and either security_review or operator_override have completed:

{
  "kind": "requires",
  "requirement": {
    "And": [
      { "Condition": "build" },
      {
        "Or": [
          { "Condition": "security_review" },
          { "Condition": "operator_override" }
        ]
      }
    ]
  }
}

Topology prerequisites and scenario completion laws accept only the monotone RET refinement: no negation and no expression that can become false as the completed-stage set grows. Stage completion requirements retain full RET, including lawful negation, because they evaluate an evidence observation rather than monotone graph progress.

When one completion makes several siblings ready, all remain independently ready_unopened. The operator may open any or all of them. Opening one neither chooses an exclusive branch nor cancels, assigns, or reserves another.

Logic Modes

The current MCP construction uses the ControlPlaneConfig default of Strong Kleene. The underlying RET library and programmatic control-plane config also support Bochvar. Evaluator/logic-mode identity is therefore part of the semantic input and must be retained for any replay claim.

Strong Kleene key properties:

Key properties:

And(true, unknown) -> unknown (can’t confirm all true)
Or(false, unknown) -> unknown (can’t confirm all false)
Not(unknown) -> unknown (can’t invert uncertainty)

Bochvar makes unknown infectious for And and Or, including cases that Strong Kleene can resolve through an absorbing value. RequireGroup uses the same count/bounds rule in both current modes.

Why Strong Kleene is the current default:

More intuitive for partial evidence
Short-circuits when possible (And(false, unknown) -> false)
Balances fail-closed with usability

[Developer]: See crates/ret-logic/src/lib.rs for the evaluation algorithm.

Use Cases

Primary: Complex gates requiring boolean combinations (And, Or, quorum) Secondary: Simple gates with single conditions (Condition node only) Anti-pattern: Don’t nest RETs too deeply - prefer focused conditions and flat trees

Troubleshooting

Problem: Gate Stuck in `unknown`

Symptoms: Gate never passes, always returns unknown

Cause: One or more conditions are evaluating to unknown

Solution:

Check gate trace to see which conditions are unknown
Fix the underlying condition issues (see condition_authoring.md)
Common causes:
- no evidence candidate was admitted for a required condition;
- candidates were present but failed assurance, freshness, agreement, or quorum policy;
- local acquisition failed operationally and therefore minted no evidence.

A post-validation predicate/type mismatch is an integrity failure, not semantic unknown.

Problem: RequireGroup Never Passes

Symptoms: RequireGroup always returns false or unknown

Cause: min is too high, or too many conditions are failing

Solution:

Check min value vs number of conditions
Verify condition outcomes in gate trace
Ensure at least min conditions can be true simultaneously

Example:

// BAD: min is 3, but only 2 conditions
{
  "RequireGroup": {
    "min": 3,
    "reqs": [
      { "Condition": "a" },
      { "Condition": "b" }
    ]
  }
}

// GOOD: min <= number of conditions
{
  "RequireGroup": {
    "min": 2,
    "reqs": [
      { "Condition": "a" },
      { "Condition": "b" },
      { "Condition": "c" }
    ]
  }
}

Problem: A Ready Sibling Was Not Opened Automatically

Symptoms: Completing a parent makes several children ready, but none starts work.

Cause: Readiness and opening are deliberately separate. DG derives the canonical ready frontier; it does not choose operator policy or imply fan-out.

Solution: Select an explicit ready_unopened stage and call scenario_open_stage with the exact accepted head. A coordination harness may select several siblings, but assignment, leases, exclusivity, and agent affinity are separate authority.

Authoring Tips

1. Keep condition keys stable and descriptive

Use tests_ok not pred1
Keys are referenced in runpacks for audit

2. Use RequireGroup for quorum-style checks

Example: “2 of 3 reviewers”, “3 of 5 datacenter checks”
Alternative: Multiple And conditions (but less flexible)

3. Prefer smaller trees with focused conditions

Easier to audit and understand
Easier to debug when gates fail

4. Validate RET structure during scenario definition

Decision Gate validates RETs at scenario_define time
Fails fast if structure is invalid (e.g., referencing non-existent conditions)

5. Keep topology and evidence laws distinct

Use monotone stage-ID RET for prerequisites and scenario completion.
Use full condition-ID RET for one stage’s evidence completion law.
Do not claim ordinary false or unknown outcome routing.
Revisit this guidance only after the blocking transition decision closes and implementation evidence exists.

Cross-Reference Learning Paths

New User Path: getting_started.md -> condition_authoring.md -> THIS GUIDE -> integration_patterns.md

Advanced Logic Path: THIS GUIDE -> evidence_flow_and_execution_model.md -> Understand how RETs fit into the evaluation pipeline

Security Path: THIS GUIDE -> security_guide.md -> Learn how explicit logic prevents backdoors

Glossary

And: Operator requiring all children to be true.

Gate: Decision point in a scenario, evaluated via RET against evidence.

Or: Operator requiring any child to be true.

Not: Operator inverting child outcome (true <-> false).

Condition: Evidence check definition: query + comparator + expected value.

RequireGroup: Quorum operator requiring at least N of M children to be true.

RET: Requirement Evaluation Tree: selected tri-valued And/Or/Not semantics plus a distinct RequireGroup threshold primitive for gates.

TriState: Evaluation outcome: true (pass), false (fail), or unknown (hold).

Strong Kleene Logic: Tri-state logic mode where And(true, unknown) -> unknown.

Requirement Evaluation Trees (RET)

At a Glance

Lowered/AOT Backend (RET)

Compile-Time vs Runtime Ingestion

Why RET?

Mental Model: RET Evaluation Tree

Tri-State Outcomes

Core Operators

And

Or

Not

RequireGroup (Quorum)

Condition (Leaf Node)

Tri-State Propagation Rules

And Propagation

Or Propagation

RequireGroup Propagation

Practical Use Cases

Simple Requirement: Both Conditions

Quorum Requirement: 2 of 3 Reviewers

Exclusion Requirement: NOT Blocklisted

Complex Requirement: (A AND B) OR C

RET in Monotone-DAG Topology

Logic Modes

Use Cases

Troubleshooting

Problem: Gate Stuck in unknown

Problem: RequireGroup Never Passes

Problem: A Ready Sibling Was Not Opened Automatically

Authoring Tips

Cross-Reference Learning Paths

Glossary

Problem: Gate Stuck in `unknown`