Requirement Evaluation Trees (RET)

A Simple Vista

Què: Àlgebra de requisits binària i tri-valuada amb un primitiu de llindar explícit Per què: Fer que la lògica de porta sigui explícita, auditable i determinista - sense regles ocultes Qui: Desenvolupadors i operadors que redacten requisits de porta complexos Requisits previs: Comprensió bàsica de les condicions (vegeu condition_authoring.md)

Backend Baixat/AOT (RET)

RET ara proporciona un backend additiu rebaixat/AOT a ret-logic:

Compila una vegada: Requirement<P> -> CompiledRequirement<K>
Avalua les vies ràpides en temps d’execució:
- CompiledRequirement::eval
- CompiledRequirement::eval_block
- CompiledRequirement::eval_tristate (+ variant de traç)
Exporta les dependències deterministes de claus de predicat:
- CompiledRequirement::predicate_keys()
Calcula vistes residuals i de progrés orientades a l’explicació:
- Requirement::residual
- CompiledRequirement::residual
Conserva la compatibilitat:
- Tree-walk Requirement::eval* es manté suportat i sense canvis.

Això és independent del domini: els dominis subministren un mapeig de claus determinista (PredicateRegistry) i una execució de claus en temps d’execució (PredicateRuntime). L’explicació residual/progrés requereix addicionalment implementacions de progrés a nivell de condició o predicat a través de ConditionProgressEval i PredicateProgressRuntime.

Ingesta en temps de compilació vs en temps d’execució

La ingesta de fonts (RON, JSON, DSL, càrregues MCP, etc.) no canvia la semàntica de RET. La diferència és el cicle de vida:

Ingesta en temps de compilació/càrrega: analitzar + validar + compilar una vegada, emmagatzemar l’artifacte compilat.
Ingesta en temps d’execució: analitzar + validar + compilar quan arriba la porta, després executar l’artifacte compilat.

Ambdós camins convergeixen en el mateix comportament d’àlgebra i avaluador compilat quan els requisits d’entrada són equivalents.

Per què RET?

Problema: Com es poden combinar múltiples verificacions d’evidència en una única decisió de porta?

Escenari d’exemple: “Vull desplegar a producció si:

L’entorn és ‘producció’ I
Les proves han passat I
La cobertura és superior al 85% I
Almenys 2 de 3 revisors han aprovat

Sense RET: El codi personalitzat pot seguir sent determinista i revisable, però cada implementació ha d’establir independentment la seva llei, identitat de versió, semàntica de traç i conformitat. El flux de control és més difícil d’inspeccionar i comparar com una àlgebra tancada.

Amb RET: Expreseu la lògica com una estructura d’arbre:

{
  "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" }
          ]
        }
      }
    ]
  }
}

Beneficis:

Explícit: La lògica és visible en l’especificació de l’escenari
Inspeccionable: La llei dels requisits és dades explícites en lloc de flux de control ocult.
Determinista: El mateix requisit validat i l’assignació de veritat exacta de fulla produeixen el mateix resultat RET.
Reavaluable: La llei canònica de requisits retinguda i les entrades de fulla poden ser avaluades fora de línia sense tornar a consultar els proveïdors. Aquesta propietat RET no estableix per si sola la reproducció semàntica completa de Decision Gate, la història de compromisos acceptats, l’autenticitat de l’evidència o la no-repudiació.

[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 auditar/exportar només evidència.

Model Mental: Arbre d’Avaluació RET

Aquí teniu com es valora un arbre de requisits:

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)

Ordre d’avaluació:

Les condicions de fulla s’avaluen en un estat de tres valors (veritable/fals/desconegut)
Els nodes operadors combinen resultats fills mitjançant lògica de tres estats
L’outcome del node arrel determina el resultat de la porta

Tri-State Outcomes

RET utilitza lògica de tres estats (no només veritable/fals):

true: Passis d’accés (tots els requisits satisfets)
false: La porta falla (requisits contradits)
unknown: Retencions de porta (requisits inconclusos)

Per què tri-estat? Les portes fallan tancades: una porta només es permet passar quan el requisit s’avalua com a true. Els resultats unknown impedeixen que les portes passin fins que l’evidència estigui completa.

Exemple:

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)

Operadors Bàsics

I

Semàntica: Tots els nens han de ser true

Taula de veritat (2 operands):

Esquerra	Dreta	Resultat
true	true	true
true	false	false
true	unknown	unknown
false	(qualsevol)	false
unknown	true	unknown
unknown	unknown	unknown

Exemple:

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

Cas d’ús: Tant les proves com la cobertura han de passar

Comportament:

Tot true -> true (passis de porta)
Any false -> false (la porta falla)
Altrament -> unknown (la porta es manté)

O bé

Semàntica: Qualsevol fill pot ser true

Taula de veritat (2 operands):

Esquerra	Dreta	Resultat
true	(qualsevol)	true
false	false	false
false	unknown	unknown
unknown	false	unknown
unknown	unknown	unknown

Exemple:

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

Cas d’ús: O bé sobreescriptura manual O bé proves automatitzades han de passar

Comportament:

Any true -> true (passos de porta)
Tot false -> false (la porta falla)
Altrament -> unknown (la porta es manté)

No

Semàntica: Invertir l’outcome del fill

Taula de veritat:

Entrada	Resultat
true	false
false	true
unknown	unknown

Exemple:

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

Cas d’ús: Les proves han de passar I la llista negra NO ha de ser activada

Comportament:

true -> false
false -> true
unknown -> unknown (fail-closed: no es pot confirmar l’absència)

RequireGroup (Quorum)

Semàntica: Almenys N de M nens han de ser true

Paràmetres:

min: Nombre mínim de resultats true requerits
reqs: Array de requisits fills

Exemple:

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

Cas d’ús: Almenys 2 de 3 revisors han d’aprovar

Comportament:

Comptar resultats true
Si el compte >= min -> true (quorum assolit)
Si count + unknowns < min -> false (quòrum impossible)
Altrament -> unknown (quorum pendent)

Exemples de taules de veritat:

Resultats	mínim	Resultat	Raó
[true, true, false]	2	true	2 certs >= mínim (quòrum assolit)
[true, unknown, unknown]	2	unknown	1 cert, no es pot assolir mínim encara
[true, false, false]	2	false	1 cert, el màxim possible és 1 < mínim
[true, true, unknown]	2	true	2 certs >= mínim (ja assolit)
[false, false, false]	2	false	0 certs, impossible

[Desenvolupador]: Vegeu ret-logic crate per a la implementació. RequireGroup compta veritable/fals de manera independent (desconegut no és ni veritable ni fals).

Condició (Fulla)

Semàntica: Referència a una condició per clau

Exemple:

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

Cas d’ús: Porteria simple amb una única condició

Comportament:

Avalua el resultat tri-estat de la condició
La condició ha d’existir a RawScenarioSpec.conditions

Regles de Propagació Tri-Estat

Com es propaguen els resultats unknown a través dels operadors:

I Propagació

Operands	Resultat	Raó
`And(true, true, true)`	true	Tots els requisits estan satisfets
`And(true, false, true)`	false	Un falla -> And falla
`And(true, unknown, true)`	unknown	No es pot confirmar que tots siguin certs encara
`And(false, unknown)`	false	Un falla (curtcircuit)
`And(unknown, unknown)`	unknown	Evidència pendent

Regla: false domina; tot true dóna true; altrament unknown

O Propagació

Operands	Resultat	Raó
`Or(false, false, false)`	false	Tots els requisits han fallat
`Or(true, false, false)`	true	Un té èxit -> Or té èxit
`Or(false, unknown, false)`	unknown	No es pot confirmar que tots siguin falsos encara
`Or(true, unknown)`	true	Un té èxit (curtcircuit)
`Or(unknown, unknown)`	unknown	Evidència pendent

Regla: true domina; tot false dóna false; altrament unknown

RequireGroup Propagation

Resultats	mínim	comptatge de certs	comptatge d’unknown	Resultat
[T, T, F]	2	2	0	true (mínim assolit)
[T, U, U]	2	1	2	unknown (màxim 3, necessiten 2)
[T, F, F]	2	1	0	false (màxim 1 < mínim)
[U, U, U]	2	0	3	unknown (màxim 3, necessiten 2)
[F, F, F]	2	0	0	false (impossible)

Regla:

Si true_count >= min -> true (quòrum assolit)
Si true_count + unknown_count < min -> false (quòrum impossible)
Altrament -> unknown (quorum pendent)

[LLM Agent]: Quan RequireGroup retorna unknown, necessites més proves. Comprova quines condicions són desconegudes i treballa per satisfer-les.

Casos d’ús pràctics

Requisit Simple: Ambdues Condicions

Escenari: Desplegar si les proves han passat I la cobertura és superior al 85%

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

Requisit de Quòrum: 2 de 3 Revisors

Escenari: Fusionar PR si almenys 2 de 3 revisors han aprovat

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

Requisit d’Exclusió: NO a la Llista Negra

Escenari: Desplegar si NO està a la llista negra

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

Requisit Complex: (A I B) O C

Escenari: Desplegar si (les proves han passat I la cobertura és correcta) O sobreescriptura manual

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

RET en Topologia Monotone-DAG

La topologia de l’escenari no és un router d’outcomes. Cada etapa no arrel porta una llei de requisit RET monòtona sobre IDs d’etapa completades. Aquests àtoms són la única font dels seus costats de dependència entrants. Per exemple, ship esdevé preparat després que build i security_review o operator_override hagin completat:

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

Els requisits de topologia i les lleis de completament d’escenari accepten només el refinament monòton RET: sense negació i sense expressió que pugui esdevenir falsa a mesura que el conjunt d’etapes completades creix. Els requisits de completament d’etapa mantenen el RET complet, incloent la negació legal, perquè avaluen una observació d’evidència en lloc del progrés del gràfic monòton.

Quan una completació fa que diversos germans estiguin preparats, tots romanen independentment ready_unopened. L’operador pot obrir qualsevol o tots ells. Obrir un no tria una branca exclusiva ni cancel·la, assigna o reserva un altre.

Modes de Lògica

La construcció actual de MCP utilitza el valor per defecte de ControlPlaneConfig de Strong Kleene. La biblioteca RET subjacent i la configuració del pla de control programàtic també admeten Bochvar. Per tant, la identitat de l’evaluador/modus de lògica és part de l’entrada semàntica i s’ha de mantenir per a qualsevol reclam de reproducció.

Propietats clau de Strong Kleene:

Propertats clau:

And(true, unknown) -> unknown (no es pot confirmar que tot sigui cert)
Or(false, unknown) -> unknown (no es pot confirmar que tot sigui fals)
Not(unknown) -> unknown (no es pot invertir la incertesa)

Bochvar fa que unknown sigui infecciós per a And i Or, incloent casos que Strong Kleene pot resoldre mitjançant un valor absorbent. RequireGroup utilitza la mateixa regla de comptatge/límits en ambdós modes actuals.

Per què Strong Kleene és el valor per defecte actual:

Més intuïtiu per a proves parcials
Curt-circuits quan sigui possible (And(false, unknown) -> false)
Els equilibris fallen tancats amb usabilitat

[Desenvolupador]: Vegeu crates/ret-logic/src/lib.rs per a l’algorisme d’avaluació.

Casos d’ús

Primari: Portes complexes que requereixen combinacions booleanes (I, O, quòrum) Secundari: Portes simples amb condicions úniques (només node de condició) Antipatró: No anideu RETs massa profundament - preferiu condicions enfocades i arbres plans

Solució de problemes

Problema: Porta enganxada en `unknown`

Síntomes: La porta mai passa, sempre retorna unknown

Causa: Una o més condicions s’estan avaluant com a unknown

Solució:

Comproveu el rastre de la porta per veure quines condicions són unknown
Solucioneu els problemes de condicions subjacents (vegeu condition_authoring.md)
Causes habituals:
- cap candidat d’evidència va ser admès per a una condició requerida;
- els candidats estaven presents però no van complir amb l’assegurament, la frescor, l’acord o la política de quòrum;
- l’adquisició local va fallar operativament i per tant no va crear cap evidència.

Un error de tipus/predicate de post-validació és una fallada d’integritat, no un unknown semàntic.

Problema: RequireGroup Mai Passa

Síntomes: RequireGroup sempre retorna false o unknown

Causa: min és massa alt, o massa condicions estan fallant

Solució:

Comprovar el valor min en comparació amb el nombre de condicions
Verifiqueu els resultats de condició en el rastre de la porta
Assegureu-vos que almenys min condicions poden ser true simultàniament

Exemple:

// 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" }
    ]
  }
}

Problema: Un germà preparat no s’ha obert automàticament

Símptomes: Completar un pare fa que diversos fills estiguin preparats, però cap comença a treballar.

Causa: La preparació i l’obertura són deliberadament separades. DG deriva la frontera preparada canònica; no tria la política d’operador ni implica la ramificació.

Solució: Seleccioneu una etapa ready_unopened explícita i truqueu a scenario_open_stage amb el cap acceptat exacte. Un arnés de coordinació pot seleccionar diversos germans, però l’assignació, els lloguers, l’exclusivitat i l’afinitat d’agents són autoritats separades.

Consells d’autoria

1. Mantingueu les claus de condició estables i descriptives

Utilitzeu tests_ok no pred1
Les claus es referencien en runpacks per a auditoria

2. Utilitzeu RequireGroup per a comprovacions de tipus quorum

Exemple: “2 de 3 revisors”, “3 de 5 comprovacions de datacenter”
Alternativa: Múltiples condicions And (però menys flexibles)

3. Preferir arbres més petits amb condicions enfocades

Més fàcil d’auditar i entendre
Més fàcil de depurar quan fallen les portes

4. Validar l’estructura RET durant la definició de l’escenari

La Decision Gate valida els RETs en el moment de scenario_define
Fallida ràpida si l’estructura és invàlida (per exemple, referenciant condicions inexistents)

5. Mantingueu les lleis de topologia i evidència distintes

Utilitzeu el RET d’ID d’etapa monòtona per a requisits previs i completament d’escenari.
Utilitzeu el RET d’ID de condició completa per a la llei de completament d’evidència d’una etapa.
No reclameu el routatge d’outcomes ordinari false o unknown.
Revisa aquesta guia només després que la decisió de transició bloquejant es tanqui i existeixi evidència d’implementació.

Camins d’Aprenentatge de Referència Creuada

Camí de Nou Usuari: getting_started.md -> condition_authoring.md -> AQUESTA GUIA -> integration_patterns.md

Camí de Lògica Avançada: AQUESTA GUIA -> evidence_flow_and_execution_model.md -> Entendre com s’integren els RETs en el pipeline d’avaluació

Camí de Seguretat: AQUESTA GUIA -> security_guide.md -> Apreneu com la lògica explícita evita portes enrere

Glossari

I: Operador que requereix que tots els nens siguin true.

Porta: Punt de decisió en un escenari, avaluat mitjançant RET contra proves.

O: Operador que requereix que qualsevol fill sigui true.

Nota: Operador que inverteix el resultat del fill (true <-> false).

Condició: Definició de comprovació d’evidències: consulta + comparador + valor esperat.

RequireGroup: Operador de quòrum que requereix almenys N de M fills per ser true.

RET: Arbre d’Avaluació de Requisits: semàntica tri-valuada seleccionada d’And/Or/Not més un primitiu de llindar distint de RequireGroup per a portes.

TriState: Resultat de l’avaluació: true (aprovat), false (suspendre) o unknown (en espera).

Lògica Kleene Forta: Mode de lògica de tres estats on And(true, unknown) -> unknown.

Requirement Evaluation Trees (RET)

A Simple Vista

Backend Baixat/AOT (RET)

Ingesta en temps de compilació vs en temps d’execució

Per què RET?

Model Mental: Arbre d’Avaluació RET

Tri-State Outcomes

Operadors Bàsics

I

O bé

No

RequireGroup (Quorum)

Condició (Fulla)

Regles de Propagació Tri-Estat

I Propagació

O Propagació

RequireGroup Propagation

Casos d’ús pràctics

Requisit Simple: Ambdues Condicions

Requisit de Quòrum: 2 de 3 Revisors

Requisit d’Exclusió: NO a la Llista Negra

Requisit Complex: (A I B) O C

RET en Topologia Monotone-DAG

Modes de Lògica

Casos d’ús

Solució de problemes

Problema: Porta enganxada en unknown

Problema: RequireGroup Mai Passa

Problema: Un germà preparat no s’ha obert automàticament

Consells d’autoria

Camins d’Aprenentatge de Referència Creuada

Glossari

Problema: Porta enganxada en `unknown`