nsaspy/prolog-rlm

Fork 0

[EPIC][expert] VERIFY expert: evidence plans, independent validation, proof-carrying outcomes, and exact Frozen-Spec acceptance #414

New issue

Open

opened 2026-09-08 01:29:21 +00:00 by nsaspy · 5 comments

nsaspy commented

2026-09-08 01:29:21 +00:00

Owner

Parent: #376
Depends on: #377, #378
Consumes: #56, #93 VERIFY, #380, #381

Goal

Add the canonical VERIFY Expert responsible for deciding whether the exact Frozen Spec is satisfied by current observable evidence.

This expert is the acceptance boundary for the closed loop. Planner, Write, Repair, model output, test prose, or worker self-report cannot declare success on its behalf.

Outcome vocabulary

Preserve at least:

satisfied(Evidence)
violated(Evidence)
unknown(Reason, Evidence)
blocked(Reason, Evidence)
error(Reason)

Missing evidence is not failure; failure is not success; a model saying “done” is not evidence.

Responsibilities

inspect exact Frozen Spec fingerprint/version;
map each requirement to required evidence classes/verifiers;
determine which evidence is already current and admissible;
request missing evidence from Project Knowledge / Retrieval / Git experts or typed plan-native validation operations;
select and compose deterministic verifiers;
evaluate requirement predicates/constraints against evidence;
preserve proof/evidence provenance per requirement;
identify violations and unknowns precisely enough for Repair Expert;
reject stale/partial/ambiguous evidence when the requirement demands current definitive evidence;
produce aggregate acceptance only when all mandatory obligations satisfy their acceptance semantics.

Verification planning

The expert may construct a verification plan, but actual runnable deterministic operations such as run/1 remain plan-native under #355.

Example:

requirement: exported predicate exists
  -> Project Knowledge evidence

requirement: tests pass
  -> plan-native run(test_profile)
  -> structured observed test result

requirement: no stale source facts
  -> current snapshot/freshness evidence

requirement: repository head contains expected change
  -> Git Expert evidence

Trust/evidence model

Compose with #56. Preserve distinction between:

claim/proof structure
source observation
runtime/test observation
trusted verifier result
model/worker assertion

A valid proof over untrusted premises is not automatically accepted evidence.

Model-generated claims may guide what to check, but they do not satisfy requirements unless the requirement explicitly treats a model result as the required observation.

Symbolic verification

Use Prolog and constraint solvers where appropriate:

fact/rule queries;
graph/reachability predicates;
closed schemas;
CLP(FD)/CLP(Q/R) constraints;
set/cardinality relations;
temporal/order constraints;
source/project provenance predicates;
exact hash/generation checks;
deterministic verifier adapters.

Normal verification should support zero model calls.

An optional review/model fallback may help formulate or interpret fuzzy evidence only when explicitly enabled; any material acceptance decision still requires admissible structured evidence.

Independent acceptance

Write Expert cannot self-verify its mutation. Repair Expert cannot weaken acceptance. Planner cannot drop failed obligations.

Verification should be re-run against fresh post-effect state whenever the relevant evidence generation changed.

Explainability

For each requirement expose:

status
verifier/decision rule
supporting evidence refs
conflicting evidence refs
missing evidence
freshness/provenance
reason for acceptance/rejection/unknown

Aggregate completion should provide a requirement-by-requirement evidence map.

Acceptance

Verifies a deterministic multi-requirement fixture with zero model calls.
Distinguishes satisfied/violated/unknown/blocked structurally.
Stale Project Knowledge cannot satisfy a current-source requirement.
Worker/model self-report alone cannot satisfy an observable-state requirement.
run/1 remains plan-native; Verify Expert may request/select it but does not become its executor.
Test success is bound to observed run identity/result, not model prose.
All requirements are checked against the same exact Frozen Spec fingerprint.
A failed requirement produces precise evidence/gap data consumable by Repair Expert.
Aggregate success requires every mandatory requirement to meet its acceptance semantics.
Cancellation/error/partial verification cannot become success.
Optional model fallback usage is separately traced/metered and cannot replace required evidence.

Non-goals

No implementation repair.
No Frozen Spec mutation.
No second verifier/evidence system parallel to #56/#93.

Refs #376 #377 #378 #56 #93 #380 #381 #355

Parent: #376 Depends on: #377, #378 Consumes: #56, #93 VERIFY, #380, #381 ## Goal Add the canonical **VERIFY Expert** responsible for deciding whether the exact Frozen Spec is satisfied by current observable evidence. This expert is the acceptance boundary for the closed loop. Planner, Write, Repair, model output, test prose, or worker self-report cannot declare success on its behalf. ## Outcome vocabulary Preserve at least: ```text satisfied(Evidence) violated(Evidence) unknown(Reason, Evidence) blocked(Reason, Evidence) error(Reason) ``` Missing evidence is not failure; failure is not success; a model saying “done” is not evidence. ## Responsibilities - inspect exact Frozen Spec fingerprint/version; - map each requirement to required evidence classes/verifiers; - determine which evidence is already current and admissible; - request missing evidence from Project Knowledge / Retrieval / Git experts or typed plan-native validation operations; - select and compose deterministic verifiers; - evaluate requirement predicates/constraints against evidence; - preserve proof/evidence provenance per requirement; - identify violations and unknowns precisely enough for Repair Expert; - reject stale/partial/ambiguous evidence when the requirement demands current definitive evidence; - produce aggregate acceptance only when all mandatory obligations satisfy their acceptance semantics. ## Verification planning The expert may construct a **verification plan**, but actual runnable deterministic operations such as `run/1` remain plan-native under #355. Example: ```text requirement: exported predicate exists -> Project Knowledge evidence requirement: tests pass -> plan-native run(test_profile) -> structured observed test result requirement: no stale source facts -> current snapshot/freshness evidence requirement: repository head contains expected change -> Git Expert evidence ``` ## Trust/evidence model Compose with #56. Preserve distinction between: ```text claim/proof structure source observation runtime/test observation trusted verifier result model/worker assertion ``` A valid proof over untrusted premises is not automatically accepted evidence. Model-generated claims may guide what to check, but they do not satisfy requirements unless the requirement explicitly treats a model result as the required observation. ## Symbolic verification Use Prolog and constraint solvers where appropriate: - fact/rule queries; - graph/reachability predicates; - closed schemas; - CLP(FD)/CLP(Q/R) constraints; - set/cardinality relations; - temporal/order constraints; - source/project provenance predicates; - exact hash/generation checks; - deterministic verifier adapters. Normal verification should support zero model calls. An optional review/model fallback may help formulate or interpret fuzzy evidence only when explicitly enabled; any material acceptance decision still requires admissible structured evidence. ## Independent acceptance Write Expert cannot self-verify its mutation. Repair Expert cannot weaken acceptance. Planner cannot drop failed obligations. Verification should be re-run against fresh post-effect state whenever the relevant evidence generation changed. ## Explainability For each requirement expose: ```text status verifier/decision rule supporting evidence refs conflicting evidence refs missing evidence freshness/provenance reason for acceptance/rejection/unknown ``` Aggregate completion should provide a requirement-by-requirement evidence map. ## Acceptance - [ ] Verifies a deterministic multi-requirement fixture with zero model calls. - [ ] Distinguishes satisfied/violated/unknown/blocked structurally. - [ ] Stale Project Knowledge cannot satisfy a current-source requirement. - [ ] Worker/model self-report alone cannot satisfy an observable-state requirement. - [ ] `run/1` remains plan-native; Verify Expert may request/select it but does not become its executor. - [ ] Test success is bound to observed run identity/result, not model prose. - [ ] All requirements are checked against the same exact Frozen Spec fingerprint. - [ ] A failed requirement produces precise evidence/gap data consumable by Repair Expert. - [ ] Aggregate success requires every mandatory requirement to meet its acceptance semantics. - [ ] Cancellation/error/partial verification cannot become success. - [ ] Optional model fallback usage is separately traced/metered and cannot replace required evidence. ## Non-goals - No implementation repair. - No Frozen Spec mutation. - No second verifier/evidence system parallel to #56/#93. Refs #376 #377 #378 #56 #93 #380 #381 #355

nsaspy commented

2026-09-08 01:46:47 +00:00

Author

Owner

Machine Spirit #401B handoff — execution monitoring does not weaken VERIFY

Depth 4B adds monitored procedures, but this issue remains the sole success boundary.

Required clarification:

Procedure monitors may request/check fresh evidence during execution to decide whether guards/invariants/branches remain valid.
Those checkpoint observations are ordinary evidence records and may be reused by final VERIFY only if they satisfy the exact Frozen-Spec verifier/freshness requirements.
Predicted operator outcomes, expected state, planner belief, selected method, branch choice, or successful continuation are never themselves verification evidence.
A monitor deciding safe_to_continue is not equivalent to VERIFY deciding the goal/spec is satisfied.
Temporal/resource validity may expire while execution/planning proceeds; final verification uses current admissible evidence, not the plan's original assumptions.
Unexpected observations remain evidence for #385 diagnosis and cannot be silently normalized into the predicted state.

Full rationale and adversarial fixtures: #401 Depth-4B.

## Machine Spirit #401B handoff — execution monitoring does not weaken VERIFY Depth 4B adds monitored procedures, but this issue remains the sole success boundary. Required clarification: - Procedure monitors may request/check fresh evidence during execution to decide whether guards/invariants/branches remain valid. - Those checkpoint observations are ordinary evidence records and may be reused by final VERIFY only if they satisfy the exact Frozen-Spec verifier/freshness requirements. - Predicted operator outcomes, expected state, planner belief, selected method, branch choice, or successful continuation are **never** themselves verification evidence. - A monitor deciding `safe_to_continue` is not equivalent to VERIFY deciding the goal/spec is satisfied. - Temporal/resource validity may expire while execution/planning proceeds; final verification uses current admissible evidence, not the plan's original assumptions. - Unexpected observations remain evidence for #385 diagnosis and cannot be silently normalized into the predicted state. Full rationale and adversarial fixtures: #401 Depth-4B.

nsaspy commented

2026-09-08 01:46:48 +00:00

Author

Owner

Machine Spirit #404B / CITADEL-EPOCH handoff

When VERIFY outcomes are used as evidence for learning/promotion, add a noninterference boundary:

freeze the exact Frozen-Spec fingerprint, verifier/version, evidence-admission policy and relevant observation generation before candidate evaluation;
candidate-authored tests/verifier changes are generation/selection evidence, not independent validation by default;
if the candidate can mutate/influence the verifier, oracle, evidence policy or benchmark inputs, the affected metric/evaluation lane is tamper-exposed and cannot be the sole promotion gate;
changing verifier/spec/evidence policy starts a fresh evaluation generation rather than retroactively validating the candidate;
fresh VERIFY success proves the exact task requirement under that verifier/evidence contract; it does not by itself prove reusable-policy/rule generalization.

Refs #404B / CITADEL-EPOCH fixtures B9-B14, B34, B40.

## Machine Spirit #404B / CITADEL-EPOCH handoff When VERIFY outcomes are used as evidence for learning/promotion, add a **noninterference boundary**: - freeze the exact Frozen-Spec fingerprint, verifier/version, evidence-admission policy and relevant observation generation before candidate evaluation; - candidate-authored tests/verifier changes are generation/selection evidence, **not independent validation by default**; - if the candidate can mutate/influence the verifier, oracle, evidence policy or benchmark inputs, the affected metric/evaluation lane is tamper-exposed and cannot be the sole promotion gate; - changing verifier/spec/evidence policy starts a fresh evaluation generation rather than retroactively validating the candidate; - fresh VERIFY success proves the exact task requirement under that verifier/evidence contract; it does **not by itself prove reusable-policy/rule generalization**. Refs #404B / CITADEL-EPOCH fixtures B9-B14, B34, B40.

nsaspy commented

2026-09-08 01:46:48 +00:00

Author

Owner

Machine Spirit #404C handoff — verifier portability is conditional

When VERIFY receipts are exported as learning/promotion evidence, expose stable fingerprints/versions for Frozen Spec, verifier semantics, evidence-admission policy and relevant observation generation. A foreign satisfied receipt authenticates a source evaluation only; it does not satisfy target VERIFY.

Target compatibility should classify source verification guarantees as preserved|translated|weakened|invalidated|unknown|noncomposable. Same verifier name with a different fingerprint is non-equivalent. A stricter target verifier keeps its unmet obligations even if the source verifier passed. Full design: #404C.

## Machine Spirit #404C handoff — verifier portability is conditional When VERIFY receipts are exported as learning/promotion evidence, expose stable fingerprints/versions for Frozen Spec, verifier semantics, evidence-admission policy and relevant observation generation. A foreign `satisfied` receipt authenticates a source evaluation only; it does **not** satisfy target VERIFY. Target compatibility should classify source verification guarantees as `preserved|translated|weakened|invalidated|unknown|noncomposable`. Same verifier name with a different fingerprint is non-equivalent. A stricter target verifier keeps its unmet obligations even if the source verifier passed. Full design: #404C.

nsaspy commented

2026-09-08 01:46:48 +00:00

Author

Owner

MACHINE-SPIRIT #404D / CLOCKWORK handoff

Promotion-oriented validation must freeze an immutable EvaluationSnapshot before consuming validation evidence. At minimum bind the exact Frozen-Spec fingerprint, verifier/version, evidence-admission policy, metric/hard-guard contract, candidate/version, baseline, task/environment epoch and relevant dependency generations.

VERIFY remains the acceptance authority for the exact obligation it checks, but VERIFY is not the statistical/generalization promoter. A successful VERIFY receipt is typed evidence consumed by #404 policy. Candidate/verifier/evidence-policy mutation after snapshot freeze makes the promotion evaluation stale/invalid rather than stronger.

Conformance handoff: source retraction/verifier generation changes racing with promotion must be detected through exact snapshot/dependency-generation checks; candidate-authored or candidate-mutated verification cannot count as independent validation by default. Refs #397 #404 #395.

## MACHINE-SPIRIT #404D / CLOCKWORK handoff Promotion-oriented validation must freeze an immutable **EvaluationSnapshot** before consuming validation evidence. At minimum bind the exact Frozen-Spec fingerprint, verifier/version, evidence-admission policy, metric/hard-guard contract, candidate/version, baseline, task/environment epoch and relevant dependency generations. VERIFY remains the acceptance authority for the exact obligation it checks, but **VERIFY is not the statistical/generalization promoter**. A successful VERIFY receipt is typed evidence consumed by #404 policy. Candidate/verifier/evidence-policy mutation after snapshot freeze makes the promotion evaluation stale/invalid rather than stronger. Conformance handoff: source retraction/verifier generation changes racing with promotion must be detected through exact snapshot/dependency-generation checks; candidate-authored or candidate-mutated verification cannot count as independent validation by default. Refs #397 #404 #395.

nsaspy commented

2026-09-08 01:46:48 +00:00

Author

Owner

#405B AEGIS-MS VERIFY handoff: VERIFY needs an acceptance dependency/influence closure in addition to ordinary evidence refs. A strong acceptance must reject forbidden self-dependence (candidate/result influences its verifier, metric, evidence selector, test set, endorsement/control rule), stale verifier/control/identity/redaction/authority generations, and effect observations that are not admissibly tied to the intended attempt/object/generation. verified must identify verifier implementation/config/trusted-base generation; it is not an unqualified truth bit. This does not move authority into VERIFY or create a second verifier system; it hardens #384's existing acceptance boundary. See #405B B7-B12, B24-B28, B41-B44.

#405B AEGIS-MS VERIFY handoff: VERIFY needs an **acceptance dependency/influence closure** in addition to ordinary evidence refs. A strong acceptance must reject forbidden self-dependence (candidate/result influences its verifier, metric, evidence selector, test set, endorsement/control rule), stale verifier/control/identity/redaction/authority generations, and effect observations that are not admissibly tied to the intended attempt/object/generation. `verified` must identify verifier implementation/config/trusted-base generation; it is not an unqualified truth bit. This does not move authority into VERIFY or create a second verifier system; it hardens #384's existing acceptance boundary. See #405B B7-B12, B24-B28, B41-B44.