The Witnessed Execution Protocol (WEXP): Core Specification

Status of This Memo

This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79.¶

Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet-Drafts is at https://datatracker.ietf.org/drafts/current/.¶

Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress."¶

This Internet-Draft will expire on 15 February 2027.¶

Copyright Notice

Copyright (c) 2026 IETF Trust and the persons identified as the document authors. All rights reserved.¶

This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Code Components extracted from this document must include Revised BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Revised BSD License.¶

Table of Contents

1. Introduction

Software and AI systems produce logs, traces, approvals, tool-call records, attestations, provenance statements, and transparency receipts. These artifacts answer different questions and are often treated as if they were interchangeable. An authentic record can contain an unsupported claim; a provenance statement can identify origin without proving a runtime event; and an independently verifiable invocation remains evidence of invocation rather than execution.¶

WEXP provides a bounded appraisal layer. Given normalized findings about an exact action, a claimed content base, an evidence-producing boundary, and any applicable provenance or independent-verification evidence, WEXP determines the set of exact claims that the findings support. It then compares the asserted claim with that set and returns one of three verdicts. The result grades support for a claim. It does not certify correctness, safety, authority, policy compliance, or alignment.¶

The conceptual basis for this work is the Witnessability Model [WITNESSABILITY] under the Witnessability Conceptual Core [WCC-CORE]. This document is self-contained: conceptual publications are informative and are not required to implement the normative appraisal procedure.¶

carrier or evidence profile
        |
        | parse, authenticate, validate semantics,
        | bind findings to an exact target and base
        v
Normalized Appraisal Input
        |
        v
WEXP Appraisal Core
        |
        v
Witnessability Appraisal

2. Conventions and Terminology

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals, as shown here.¶

Action Target

The exact action, decision, invocation, execution, or observed event to which a claim and its supporting findings are bound. Core treats the target as opaque and defines no identifier format.¶

Content Base

The kind of action-related content asserted by a claim: observation, intent, invocation, or execution.¶

Qualifier

An additional property of evidence supporting an exact content claim. A qualifier does not change the content base.¶

Normalized Evidence Fact

A profile-produced finding with an exact target, an exact content base or qualifier role, an evaluation status, basis references, and limitations.¶

Boundary Ceiling

The strongest content base that the accepted evidence-producing boundary can warrant. It excludes stronger claims but never creates support.¶

Exact Support

Support established by the predicate for the same action target, content base, qualifier set, and evaluation context as the claim.¶

Witnessability Appraisal

The result produced by the Core procedure, including the supported claim set, verdict, reasons, evaluation gaps, limitations, boundary information, and evaluation context.¶

3. Conformance Classes

This document defines the Conformance Classes CC0 through CC5. A Conformance Class classifies the capability of an appraising implementation. It is orthogonal to the appraisal result: it scopes what an implementation assesses, and it never bounds, raises, or lowers the state a record is found to support.¶

A Conformance Class MUST NOT be used as an input to the appraisal procedure of Section 8, as a ceiling on a supported claim, or as a sort key over claims. Where an implementation lacks the capability required to assess a claim, the applicable fail-closed *_NOT_EVALUATED outcome of Section 8 applies; the implementation MUST NOT downgrade the appraisal result in place of reporting that it did not evaluate.¶

No capability bound on a verified state is defined by this document. A profile or deployment that requires a minimum Conformance Class states that requirement in its own terms; it does not thereby alter what any record supports.¶

4. Claim Model

observation < intent < invocation < execution

(observation, {})       (observation, {IV})
(intent, {})            (intent, {IV})
(invocation, {})        (invocation, {IV})
(execution, {})         (execution, {PROV})
(execution, {IV})       (execution, {PROV, IV})

(b1, A1) <= (b2, A2)  iff  b1 <= b2 and A1 is a subset of A2

5. Presentation and Display Projection

The authoritative form of a claim in this document is its typed state: the pair of a content base and a set of evidence qualifiers, written in the bracketed notation of Section 4. The bracketed notation is the canonical form for showing qualified states.¶

A carrier that also exposes a single bare display label MUST NOT emit a record in a qualified state without carrying that record's authoritative typed state alongside the label. A bare display label is a projection of the typed state; it is never the authority for it, and it is never a sort key.¶

Where a display label is produced, it MUST be produced by a declared projection with the following properties. The projection is profile-defined and justified: this document presumes no total order over typed states, and any projection into one requires justification by the profile that declares it. The projection is version-identifiable: a reader of a display value can determine which revision of which projection produced it. The projection never exceeds the typed state: the label denotes the greatest bare label that is less than or equal to the typed state under the declared projection.¶

Where the declared projection is ambiguous for the state consisting of the execution base with both the provenance and independent-verification qualifiers, the label denotes WL4. Both WL4 and WL5 are maximal bare labels below that state and neither exceeds the other, so the projection alone does not determine the value; this resolution is fixed by this document and is not left to the projection.¶

A display label MUST equal the value of the declared projection applied to the authoritative typed state. Consistency is defined against the projection, not against any tabular image of it. A divergence between a display label and the authoritative typed state is a fatal defect of the input: the record is rejected and no claim is appraised. The concrete error token for that condition is bound by the carrier (Section 11), not by this document.¶

A conforming reader is cautioned that a schema-valid record is not thereby a correctly projected record: schema validity concerns the integrity of the bytes, while a projection concerns semantic continuity between the label and the state. A reader of an earlier revision of this protocol should not assume that a bare label carried there denotes the same state under the projection declared here.¶

6. Normalized Appraisal Input

The set of inputs this document requires is exhaustive for WEXP Core: for each claimed state it is the complete set of Core-required inputs. A profile MAY require more; Core does not. Requirements are keyed on the authoritative typed state of Section 5, never on a display label.¶

Core does not require a commitment to the input at the execution level; a claim at the execution level therefore binds the execution, not the input. A profile that needs the input bound at that level MUST require it. Binding an input at the execution level would add a field, not a witness: the declaring sentence above and this deferring sentence are about one and the same object, and that is said here plainly rather than left to be inferred.¶

A mapping profile supplies the following logical input. This is an abstract contract, not a wire schema.¶

AppraisalInput = {
  semantics_version,       ; "wexp-core-1"
  target,
  asserted_claim,
  evaluation_context: {
    id,
    evaluated_at,
    trust_configuration,
    profile_identifiers[]  ; immutable profile revisions;
                           ; bind applicable registries
  },

  boundary_finding: {
    target,
    evaluation_context_ref,
    ? ceiling_base,         ; REQUIRED when status is supported;
                             ; ignored otherwise
    status,                 ; supported | unsupported | not-evaluated
    target_binding,         ; supported | unsupported | not-evaluated
    grounding,              ; asserted-only | attributed | attested |
                             ; not-evaluated
    basis_refs[],
    reasons[],
    limitations[]
  },

  base_findings[]: {
    target,
    evaluation_context_ref,
    base,
    target_binding,         ; supported | unsupported | not-evaluated
    semantic_validation,    ; supported | unsupported | not-evaluated
    basis_refs[],
    reasons[],
    limitations[]
  },

  qualifier_findings[]: {
    target,
    evaluation_context_ref,
    qualifier,              ; PROV | IV
    qualified_base,
    target_binding,
    semantic_validation,
    independence_validation, ; supported | unsupported |
                             ; not-evaluated | not-applicable
    basis_refs[],
    reasons[],
    limitations[]
  },

  recorder_relations[]: {
    profile_identifier,
    relation_token,
    subject_ref,
    object_ref,
    basis_refs[],
    limitations[]
  },
  counter_evidence[]: {
    status,                 ; not-supplied | not-evaluated |
                             ; resolved-no-defeat |
                             ; unresolved-material | defeating
    affected_claims[],      ; or all-admissible-claims
    basis_refs[],
    reasons[],              ; substantive-category profile tokens
    limitations[]
  },
  evaluation_scope,         ; initial-capability-name or
                             ; (profile_identifier, local_name) ->
                             ; evaluated | not-evaluated
  profile_evaluation_gaps[]: {
    target,
    evaluation_context_ref,
    token,
    ? current_scope_capability, ; authenticity | composition;
                                ; absent for inherited gaps
    affected_claims[],      ; or all-admissible-claims
    basis_refs[],
    limitations[]
  },
  inherited_limitations[],
  fatal_conditions[]
}

Every displayed top-level component is REQUIRED. The only semantics version defined by this document is wexp-core-1. Any other text-atom value is fatal and produces E_UNSUPPORTED_SEMANTICS_VERSION. An absent or non-text value is malformed under Section 6.2.¶

The mapping process MUST be claim-independent: it evaluates every available base material and every evidence role, not only the asserted base or asserted qualifiers. This permits an appraisal to report an incomparable supported alternative, such as PROV-supported execution when IV-supported execution was asserted.¶

A passing base or qualifier finding MUST state that the evidence was semantically validated, accepted under the evaluation context, and bound to the exact target and exact base named by the finding. Presence of a reference, a valid digest, a signature, or an artifact whose media type suggests provenance or attestation is insufficient.¶

A profile MUST distinguish unsupported, meaning the relevant assessment ran and failed, from not-evaluated, meaning the assessment was unavailable or outside the evaluation scope. It MUST preserve all applicable limitations and evaluation gaps.¶

All findings are explicitly scoped. The boundary finding, every base and qualifier aggregate, and every profile-gap entry have a target equal to the top-level target and an evaluation_context_ref equal to the top-level evaluation-context identifier. A foreign-scoped aggregate is not negative evidence for this appraisal; it violates the normalized-input cross-field contract and produces E_PROFILE_MAPPING_INVALID. Evidence that was safely evaluated but covers or binds a different target or base is represented by a correctly scoped aggregate with a non-passing status and, when applicable, E_EVIDENCE_COVERAGE_MISMATCH or E_EVIDENCE_NOT_BOUND. The boundary finding additionally requires supported target binding before its ceiling can be used.¶

A normalized input contains exactly one aggregated boundary finding, at most one aggregated base finding for each (target, base, evaluation_context) key, and at most one aggregated qualifier finding for each (target, qualifier, qualified_base, evaluation_context) key. A mapping profile combines multiple raw artifacts into that aggregate and preserves all basis references and limitations. Duplicate or conflicting aggregate findings are fatal and produce E_PROFILE_MAPPING_INVALID.¶

A boundary finding with status = supported MUST contain ceiling_base. Its absence is a profile-mapping failure and produces E_PROFILE_MAPPING_INVALID. A supported boundary has a grounding value of asserted-only, attributed, or attested that the evaluation context accepts. grounding = not-evaluated is valid only with status = not-evaluated; either field paired differently produces E_PROFILE_MAPPING_INVALID. When boundary status is unsupported or not-evaluated, a present ceiling_base is diagnostic carrier metadata only and is ignored by the Core algorithm.¶

A PROV aggregate is valid only when qualified_base = execution and independence_validation = not-applicable. An IV aggregate is valid only when qualified_base is one of the four content bases and independence_validation is supported, unsupported, or not-evaluated. PROV on another base, IV with not-applicable, or another recognized but disallowed qualifier-field combination produces E_PROFILE_MAPPING_INVALID. An unknown closed-enum member or wrong logical type is malformed. A mapper does not delete or repair an invalid qualifier aggregate. A valid qualifier contributes support only when its exact qualified base is independently in B.¶

counter_evidence is an entry set, not a single strongest status. When no counter-evidence was supplied it contains exactly one not-supplied entry with empty affected claims, basis references, reasons, and limitations. Otherwise not-supplied is absent and every entry names at least one admissible affected claim or all-admissible-claims. not-evaluated means supplied counter-evidence could not be assessed; resolved-no-defeat means it was assessed and does not defeat the named claims; unresolved-material means it is material but unresolved; and defeating means it affirmatively defeats the named claims. When the affected claims cannot be narrowed safely, affected_claims is all-admissible-claims. Entries with different affected-claim sets or statuses MUST NOT be collapsed into one status.¶

Every member of a counter entry's reasons set MUST be a token registered in the substantive category by a registry applicable to the mapping profile and MUST apply to that entry's affected claims. Fatal tokens are carried in fatal_conditions, and evaluation-gap tokens are carried in profile_evaluation_gaps; they MUST NOT appear in counter_evidence[].reasons. A non-Core token resolves uniquely, including category, through exactly one immutable registry revision identified by an applied profile_identifier; absence, ambiguity, or category disagreement produces E_PROFILE_MAPPING_INVALID. Entry reasons are explanatory and do not change the entry status or block a claim by themselves. Core-derived counter-status tokens are emitted in addition to, not instead of, applicable entry reasons.¶

Likewise, every token in reasons[] on a boundary, base, or qualifier finding MUST be registered in the substantive category and apply to that finding. A non-Core token resolves uniquely through an immutable registry revision identified by an applied profile_identifier. Fatal tokens belong in fatal_conditions, and evaluation-gap tokens belong in profile_evaluation_gaps. An absent, ambiguous, unregistered, or miscategorized finding reason is a profile-mapping failure and produces E_PROFILE_MAPPING_INVALID.¶

Every member of fatal_conditions MUST be a token registered in the fatal category by the Core registry or a registry applicable to the mapping profile. Core tokens are bound to the semantics_version; every non-Core token resolves uniquely through an immutable registry revision identified by an applied profile_identifier. An absent, ambiguous, unregistered, or miscategorized member is a profile-mapping failure; the appraiser returns E_PROFILE_MAPPING_INVALID instead of treating that member as fatal.¶

profile_evaluation_gaps carries structured gaps supplied by a mapping or composition profile that are not otherwise recoverable from a Core finding status. Every entry is scoped to the exact target and evaluation context and contains a token registered in the evaluation-gap category, at least one admissible affected claim or all-admissible-claims, basis references, and limitations. A non-Core token resolves uniquely through an immutable registry revision identified by an applied profile_identifier. The optional current_scope_capability is present only when the entry represents the current appraiser's unperformed authenticity or composition assessment; it names exactly that initial capability. The token registration also identifies that same capability: E_COMPOSITION_NOT_EVALUATED is initially registered for composition, while authenticity requires an exact profile token registered for authenticity assessment. A profile can register another evaluation-gap token for either capability. A marker-token capability mismatch produces E_PROFILE_MAPPING_INVALID. Absence of the marker means that the entry is inherited or otherwise diagnostic and does not determine a current capability status. A composition profile uses this field to preserve applicable upstream gaps after remapping them to the exact chain target. An entry with an empty affected-claim set, an absent, ambiguous, unregistered, or non-evaluation-gap token binding, an incorrect target or evaluation-context scope, an invalid current-scope marker, or malformed basis references or limitations is a profile-mapping failure. A valid entry whose affected claims include neither the asserted claim nor a member of SupportedClaims is unrelated to this appraisal and is not projected.¶

7. Boundary Ceiling

For every supported claim (b, A), b MUST NOT exceed the accepted boundary_finding.ceiling_base. Qualifiers do not alter this comparison.¶

supported_content_base <= accepted_boundary_ceiling

The Boundary Ceiling is an exclusion rule, not an evidence source. A boundary finding can prevent a base from being supported; it MUST NOT create a positive base finding. Observation itself requires a positive exact observation finding.¶

The result MUST preserve the boundary grounding status and its limitations. A string or structural descriptor asserted by a producer is at most asserted-only; a valid signature associated with an accepted identity can make it attributed; and an applicable boundary-grounding profile can make it attested. Attribution is not proof of actual boundary control.¶

boundary_finding.status = supported means that the boundary predicate required by the named evaluation context passed. The evaluation context MUST identify the minimum acceptable grounding. A profile MUST NOT mark a boundary supported merely because a boundary name or descriptor is present. An asserted-only or attributed finding can be supported only when the evaluation context explicitly accepts that grounding class; the result still reports the weaker grounding and its limitations.¶

The boundary status has deterministic precedence. When status = not-evaluated, no base is added and the appraiser records E_BOUNDARY_NOT_EVALUATED. When status = unsupported, no base is added and it records E_BOUNDARY_NOT_SUPPORTED. Only status = supported with target_binding = supported and matching target and context makes ceiling_base usable. A failed or unevaluated target binding prevents use of the ceiling and adds the corresponding profile reason or gap.¶

8. Appraisal Procedure

SupportedClaims = {
  (b, A) | b is in B, A is a subset of Q(b),
           and (PROV in A implies b == execution)
}

appraise(input):
  if input is not a logical record or
     semantics_version is absent or not a text atom:
      return rejected_result(E_MALFORMED_NORMALIZED_INPUT)
  if input.semantics_version != "wexp-core-1":
      return rejected_result(E_UNSUPPORTED_SEMANTICS_VERSION)
  if any required wexp-core-1 member, closed enum, logical type,
     set, entry, claim, token, or recorder relation is malformed:
      return rejected_result(E_MALFORMED_NORMALIZED_INPUT)
  if any cross-field invariant enumerated in input-validity fails:
      return rejected_result(E_PROFILE_MAPPING_INVALID)
  if input.fatal_conditions is not empty:
      return rejected_result(input.fatal_conditions)
  if input.asserted_claim is outside the admissible domain:
      return rejected_result(E_CLAIM_OUT_OF_DOMAIN)

  B = {}
  SupportEntries = {}
  for every base finding f, independently of the asserted claim:
      if f.target == input.target and
         f.evaluation_context_ref == input.evaluation_context.id and
         f.target_binding == supported and
         f.semantic_validation == supported and
         input.boundary_finding.status == supported and
         input.boundary_finding.target == input.target and
         input.boundary_finding.evaluation_context_ref ==
             input.evaluation_context.id and
         input.boundary_finding.target_binding == supported and
         f.base <= input.boundary_finding.ceiling_base:
          add f.base to B

  SupportedClaims = {}
  for b in B:
      Q = {}
      if b == execution and
         valid_PROV_finding(input.target, b,
                            input.evaluation_context.id):
          add PROV to Q
      if valid_IV_finding(input.target, b,
                          input.evaluation_context.id):
          add IV to Q
      for every admissible (b, A), A subset of Q:
          add (b, A) to SupportedClaims
          add support_entry((b, A), exact premises, basis,
                            limitations)
              to SupportEntries

  MaximalSupportedClaims = maximal members of SupportedClaims
  asserted_claim_supported = input.asserted_claim in SupportedClaims
  fatal_reasons = {}
  reasons = {}
  GapEntries = {}

  for every row of the claim-required diagnostic matrix:
      if that row's exact predicate is true:
          if the row is substantive:
              add its token to reasons
          else:
              add its exact Core gap entry to GapEntries

  for every boundary, base, or qualifier finding that is the
      asserted role or an exact premise of a SupportEntry:
      add its registered substantive reasons to reasons

  for every profile gap entry whose affected claims include
      the asserted claim, a member of SupportedClaims, or
      all-admissible-claims:
      add that exact entry to GapEntries

  for c in applicable_counter_entries(
         input.counter_evidence, input.asserted_claim):
      reasons = reasons union c.reasons
      if c.status == not-evaluated:
          add gap_entry(E_COUNTER_EVIDENCE_NOT_EVALUATED,
                        input.target, input.evaluation_context.id,
                        c.affected_claims,
                        c.basis_refs, c.limitations)
              to GapEntries
      if c.status == unresolved-material:
          add E_COUNTER_EVIDENCE_UNRESOLVED to reasons
      if c.status == defeating:
          add E_COUNTER_EVIDENCE_DEFEATING to reasons

  gaps = token projection of GapEntries
  limitations = the applicable union defined in supported-claims

  if asserted_claim_supported and not counter_blocks(
         input.counter_evidence, input.asserted_claim):
      verdict = accept
  else:
      verdict = downgrade

  return Appraisal with every required component

rejected_result(fatal_tokens):
  return Appraisal with verdict = reject,
         semantics_version = "wexp-core-1",
         fatal_reasons = fatal_tokens,
         substantive_reasons = {}, evaluation_gaps = {},
         evaluation_gap_entries = {},
         supported_claims = {}, maximal_supported_claims = {},
         support_entries = {}, support_relations = {},
         asserted_claim_supported = false,
         boundary_ceiling = unavailable,
         boundary_grounding = unavailable,
         target = unavailable, asserted_claim = unavailable,
         recorder_relations = unavailable,
         counter_evidence = unavailable,
         inherited_limitations = unavailable,
         evaluation_context = unavailable,
         evaluation_scope = unavailable

Appraisal = {
  semantics_version,
  verdict,
  fatal_reasons[],
  target,
  asserted_claim,
  asserted_claim_supported,
  support_entries[],
  supported_claims,
  maximal_supported_claims,
  support_relations,
  boundary_ceiling,
  boundary_grounding,
  recorder_relations[],
  substantive_reasons[],
  evaluation_gaps[],
  evaluation_gap_entries[],
  counter_evidence[],
  inherited_limitations[],
  evaluation_context,
  evaluation_scope
}

9. Composition

Composition-profile mapping and Core appraisal are separate conformance surfaces. Core consumes only an ordinary normalized input for the exact chain target; it does not consume raw segments, adjacency records, or warrants and does not infer a chain finding. A Core appraiser can implement the complete Core procedure without implementing a composition profile. An implementation that separately claims composition-profile conformance identifies the immutable composition-profile revision and satisfies the additional mapping obligations in this section.¶

A chain claim MUST NOT be derived by numeric minimum, by a display label, or by a meet of segment states alone. A composition profile MUST identify:¶

• the exact chain target;¶

• the exact segment claims used as premises;¶

• the validated adjacency bindings;¶

• the composition warrant mapping those premises to the chain claim; and¶

• the evaluation context shared by the premises; and¶

• the independence of the independent-verification roots relied on by the premises.¶

The identified composition-profile revision defines the logical types and predicates for premises, adjacency bindings, warrants, their exact identity, and their target and context equality. The profile evaluates those values and emits ordinary normalized base and qualifier findings for the exact chain target. The ordinary Core algorithm then appraises those findings; composition is not a second Core appraisal algorithm.¶

A chain base finding is supported only if every named premise is exactly supported and every required binding and warrant evaluates to supported under that immutable profile. An absent or unsupported required adjacency binding produces no positive chain finding; the profile places substantive E_CHAIN_UNBOUND on the correctly scoped non-passing chain-role aggregate. It does the same with E_COMPOSITION_WARRANT_MISSING for an absent or unsupported warrant. Where two premises rely on the same independent-verification root, that root is not independent for the purposes of this warrant, and the profile places substantive E_SHARED_VERIFICATION_ROOT on the correctly scoped non-passing chain-role aggregate. Correctness of the composition operator is not itself a warrant; the warrant consists of the binding, the coverage of the inter-segment link, and the independence of the verification roots. A required assessment that was not performed is represented by a structured E_COMPOSITION_NOT_EVALUATED profile-gap entry affecting the exact chain claim. These are safely interpretable support failures and lead to downgrade when the chain claim is not otherwise supported. If a malformed or internally contradictory chain description still permits a structurally usable Core input, the profile supplies fatal E_CHAIN_DESCRIPTION_INVALID; otherwise the upstream failure produces no Core appraisal under Section 6.2. Individual segment appraisals are unaffected.¶

An inherited PROV qualifier requires exact PROV support for every required segment plus provenance coverage of every required inter-segment binding. An inherited IV qualifier requires exact IV support at the relevant base for every required segment, covered chain bindings, and a passing chain independence assessment. Alternatively, a profile can establish a new chain-level PROV or IV qualifier from a separate exact chain-level finding and explicit warrant; that finding is evaluated by the ordinary qualifier rules and cannot be inferred from segment depth alone.¶

A composed input MUST inherit the set union of recorder relations and of unresolved limitations, freshness and revocation limits, coverage limits, and trust-context restrictions of its premises unless a named warrant explicitly resolves a specific item. Applicable upstream evaluation gaps are remapped to the exact chain target and affected chain claims and carried as structured profile_evaluation_gaps entries with their original basis references and limitations. A warrant that resolves a gap names the exact entry and records the resolving basis; it cannot silently delete all gaps of the same token.¶

Counter-evidence entries from all premises and chain-level findings are retained separately. Entries can be coalesced only when status and affected-claim set are identical; their basis references, reasons, and limitations are then set-unioned. Statuses, affected-claim sets, or reason sets across different scopes MUST NOT be collapsed or promoted by precedence. If any evaluator cannot narrow affected claims safely, that entry uses all-admissible-claims. The composed set contains one not-supplied entry only when every premise and chain-level input reports not-supplied; otherwise all such sentinel entries are omitted.¶

A chain claim and a terminal-action claim are distinct. Support for a chain does not establish completion, terminal effect, or goal satisfaction. A terminal-action claim uses the terminal segment's exact support plus a validated binding to the selected terminal action.¶

The Core conformance evidence in Section 12 covers only the appraisal of normalized composition outputs unless a separate composition-profile claim is declared. The C11 and C12 fixtures in Section 13 assume that an identified external composition profile has already emitted the stated ordinary finding. They test Core support construction and limitation carry-through, not premise discovery, adjacency validation, warrant evaluation, or composition-profile conformance.¶

10. Non-Inference and Coverage Rules

The limits in this section are an application of an invariant this protocol inherits rather than states. Quoting [WCC-CORE], part 4: "No transition, inference, transformation, aggregation, or composition may increase the Support Envelope without an explicit warrant and any additional premises or basis required by that warrant." Every downstream result inherits the relevant limitations of upstream materials and arguments unless those limitations are explicitly resolved. This document does not introduce that rule and claims no novelty for it; the material below that derives from it is cited, not restated. The composition warrant of Section 9 is this document's operational form of the warrant named in the quoted invariant.¶

The corresponding rule of this document is stated over claim strength: no transition, inference, transformation, aggregation, or composition may increase the strength of a supported claim without an explicit warrant and the premises that warrant requires. This document inherits the quoted invariant by intent and not by identity of objects; Support Envelope is not defined here, and remains the object of [WCC-CORE].¶

Provenance of this section: the W-I7 material here is a byte-exact, attributed quotation from [WCC-CORE] (SHA-256 382e3986…), which was demonstrably in hand when this section was authored. The underlying non-inflation principle appeared in the WEXP line — [I-D.sergeev-wexp-core-00], submitted 2026-07-05/06 — before the earliest provable carrier of the W-I7 twelve-pair formulation (2026-07-23); no WEXP text reproduces W-I7 wording other than as an attributed quotation.¶

The inherited invariant lands together with its third part, Preserved Incomparability, and not alone: a total order over typed states is not presumed, and a projection into one requires justification by the profile that declares it. A single maximum among supported states is not guaranteed, and monotonicity is not presumed.¶

Two boundaries of this landing are stated so that nothing is quietly raised by it. The Boundary Ceiling of Section 7 is untouched by this section and its status is not elevated by appearing beside an inherited invariant. The corollary that verifiability does not raise the captured level belongs to a different axis and is not merged with the rule above.¶

The following limits are normative:¶

• observation does not imply intent, invocation, or execution;¶

• intent does not imply authority, authorization validity, invocation, or execution;¶

• invocation does not imply execution, completion, or effect;¶

• execution does not imply completion of a larger process, durable external effect, goal satisfaction, correctness, safety, or policy compliance;¶

• a provenance artifact by itself does not establish runtime occurrence; a PROV-qualified WEXP claim presupposes separately established exact execution support, and IV does not imply PROV;¶

• a signature authenticates bytes under a key; it does not establish content truth or boundary control;¶

• a transparency receipt establishes registration or custody; it does not establish PROV, IV, or execution;¶

• presence of records does not establish completeness of coverage;¶

• absence of a record does not establish nonoccurrence;¶

• a sole counter_evidence entry with status = not-supplied does not establish absence of counter-evidence; and¶

• aggregation and transformation do not remove upstream limitations unless an explicit warrant resolves them.¶

11. Cross-Carrier Equivalence

Two carrier inputs are Core-equivalent when, under the same semantics version and evaluation context, they normalize under Section 6.1 to equal algorithm-relevant targets, asserted claims, finding statuses, scopes, and reason sets, boundary ceilings and grounding, recorder relations, basis references, profile-gap entries, evaluation scope, limitations, and fatal conditions. Counter-evidence equivalence includes every entry's status, affected claims, reasons, basis references, and limitations. Applied profile identifiers and their immutable revisions are part of that equality.¶

A conforming Core appraiser MUST return the same complete logical appraisal for Core-equivalent inputs. Carrier-specific parse, authentication, and transport metadata can differ without affecting Core equivalence only when they do not change a normalized component. Inputs that differ only in opaque basis-reference identifiers are not completely Core-equivalent; when all other normalized components are equal, their appraisals MUST nevertheless be identical except for those carried basis references and any carrier metadata that the result profile explicitly preserves.¶

12. Core Conformance and Evaluation Scope

A full Core-appraiser conformance claim is binary only for an exact declared revision and scope. The claim record identifies the Core document name and immutable source digest, semantics_version, reviewed Requirements Registry identifier and digest, required vector-package identifier and manifest digest, implementation and runner revisions, and the complete requirement and vector identifier sets in scope. These identities prevent a Core-00 result, a Snapshot-001 result, or a result from another Core-01 source from being presented as evidence for different bytes.¶

For that exact scope, PASS means that the implementation asserts every bound reviewed requirement, every required frozen vector was parsed under its identified non-normative harness, every complete logical appraisal equaled the independently frozen expected appraisal, and the execution recorded zero mismatch, not-run, and blocked cases. The normative authority remains this specification and its reviewed requirements; vector comparison is evidence, not the source of an expectation.¶

A full conformance record enumerates all reviewed Core-appraiser requirements and all required vectors for the identified revision. An implementation that supports a smaller surface lists the exact included and omitted requirement and vector identifiers and labels the result PARTIAL; it does not claim full Core conformance. Composition-profile conformance, carrier conformance, and result-carrier conformance are separate claims with separate immutable profile identities.¶

PASS is not certification, proof of correctness or completeness, proof of security, evidence of interoperability with an untested implementation or carrier, IETF acceptance, or authority to make policy decisions. No conformance record changes the specification-to-requirements-to-vectors-to-implementation authority direction.¶

evaluation_scope is an unordered map from capability names to exactly one of evaluated or not-evaluated. The following initial names are closed for wexp-core-1:¶

• carrier-mapping;¶

• authenticity;¶

• target-binding;¶

• boundary-grounding;¶

• observation-support;¶

• intent-support;¶

• invocation-support;¶

• execution-support;¶

• provenance-support;¶

• independent-verification;¶

• composition; and¶

• counter-evidence.¶

Every initial name MUST appear exactly once. An extension key is the logical pair (profile_identifier, local_name), where the immutable applied profile identifier occurs in evaluation_context.profile_identifiers and local_name is a non-empty name in that revision. The pair is its identity. Core ignores an extension status for support and gap derivation but preserves the exact pair and status in the result. An unbound, malformed, duplicate, or ambiguous extension key produces E_PROFILE_MAPPING_INVALID.¶

The scope map is a deterministic summary of the assessments represented by the normalized input. carrier-mapping is evaluated for every complete Core input. For each finding-backed or counter-evidence capability, evaluated means discovery of applicable material completed and every supplied assessment governed by that capability has a status other than not-evaluated; absence of an aggregate under that value means discovery completed and found no candidate evidence. not-evaluated means at least one applicable governed assessment could not be performed. When such an assessment is required by the asserted claim, that value is accompanied by the exact role aggregate with its relevant status set to not-evaluated.¶

The external authenticity and composition capabilities use a fully syntactic rule: their scope value is not-evaluated if and only if at least one profile-gap entry names that capability in current_scope_capability, and is evaluated if and only if no entry names it. A marked entry can affect any exact admissible claim; its projection into the result remains governed separately by the affected-claim rule. Core does not decide from profile-defined trust data whether an external assessment was required.¶

The governed status fields are: every finding's target_binding for target-binding; boundary status, binding, and grounding for boundary-grounding; the corresponding base aggregate's binding and semantic status for each base-support capability; PROV binding and semantic status for provenance-support; IV binding, semantic, and independence status for independent-verification; and counter-entry status for counter-evidence. A scope value of evaluated with a governed not-evaluated status, a required finding-backed not-evaluated capability without its aggregate, a current-scope marker whose capability is not not-evaluated, or an external capability value without the required marker presence or absence violates the cross-field contract and produces E_PROFILE_MAPPING_INVALID.¶

A profile_evaluation_gaps entry without current_scope_capability can preserve a gap from an upstream or composed premise under its own exact scope. Its presence does not change the current appraiser's capability status. Core determines current-scope consistency only from the explicit optional field and never interprets opaque basis references for that purpose.¶

An evaluation capability MUST NOT be used as evidence and MUST NOT create or structurally cap a claim. A role-specific Core gap entry is emitted only by the claim-required matrix when its aggregate is required by the asserted claim. A valid profile-gap entry is projected under its affected-claim rule. Otherwise the scope map alone records the unexercised capability and does not become a reason, gap, or substantive finding.¶

The cumulative CC0-CC5 scale from draft-sergeev-wexp-core-00 is not part of the Core appraisal algorithm in this revision. Producer capability declarations and carrier conformance belong to carrier profiles.¶

13. Normative Semantic Test Vectors

C01 through C16 are normative logical cases, not a wire format. A conformance record binds an executable representation through an exact manifest that identifies the source revision, reviewed requirement and case identifiers, non-normative harness schema, fixture bytes, and frozen expected logical appraisals. The representation and comparison procedure do not add a Core serialization requirement. A representation passes a case only when its complete decoded logical input and complete observed appraisal equal the normative input and expectation stated here.¶

The logical fixtures below are normative. Common input values are: semantics_version=wexp-core-1; target T; evaluation-context identifier C; a supported, target-bound, attributed boundary finding for T and C with basis bd and the stated ceiling; empty recorder relations, profile evaluation gaps, inherited limitations, and fatal conditions; counter-evidence consisting of one entry whose status is not-supplied and whose affected-claim, basis-reference, reason, and limitation sets are empty; and every initial evaluation-scope capability set to evaluated. Every supported base or qualifier finding has target T, context C, supported target binding and semantic validation, empty reasons and limitations, and a basis identifier matching its name. Supported IV additionally has supported independence validation; PROV uses not-applicable. A finding not stated in a row is absent.¶

P_COUNTER_FAIL is an opaque fixture token assumed to be registered in the substantive category by the fixture's mapping profile.¶

In the table, O, I, N, and E mean unqualified observation, intent, invocation, and execution. +P and +V mean PROV and IV. S is supported_claims, M is maximal_supported_claims, and A is asserted_claim_supported. For each member of S, support_entries contains exactly one entry whose basis is the union of bd, its base basis, and any qualifier bases; its limitations are the union of those premises. support_relations contains the displayed relation for each member of M. gaps={} also means evaluation_gap_entries={}. For accept and downgrade rows, fields not varied by a row equal the common input values and carry through to the output. A reject row instead uses the complete fixed projection in Section 8.4.¶

14. Security Considerations

WEXP limits inference; it does not make a dishonest or compromised witness honest. A false boundary assertion, malicious mapping profile, compromised signer, or colluding evidence evaluator can manufacture normalized findings unless the evaluation context independently constrains those actors.¶

Authenticity is not truth. A valid signature establishes that bytes verify under a key. Key-to-identity binding attributes the assertion. Neither establishes that the action occurred, that the signer controlled the claimed boundary, or that the signer was authorized.¶

Reference integrity is not semantic support. A digest can bind an appraisal input to artifact bytes. It does not establish the artifact's type, exact-action coverage, accepted root, or independence. Qualifier support requires the exact profile predicate in Section 6.¶

Boundary grounding. A declared boundary can be false. Appraisals preserve whether it was asserted, attributed, attested, or not evaluated. Relying parties MUST NOT erase this distinction.¶

Self-report. A self-report can support a report about what the actor asserted. It does not provide third-party non-repudiation merely because its content base is deep or its bytes are signed.¶

Independent verification. Independence is profile- and context-relative. Different keys or roots can remain under common administrative control, while a shared public root does not necessarily destroy operational independence. A passing IV finding needs an explicit assessment basis.¶

Counter-evidence. Unresolved material counter-evidence blocks acceptance. No supplied counter-evidence is not proof that none exists.¶

Coverage and nonoccurrence. A set of valid records can be incomplete. A missing record can reflect omission, capture failure, refusal to emit, loss, or an action that never occurred. WEXP Core does not distinguish those cases without positive profile-defined evidence.¶

Composition. Composition is a common inflation point. Exact premises, bindings, warrants, and limitation inheritance are required. A chain appraisal cannot be used as evidence for a terminal effect unless a separate predicate establishes that exact claim.¶

Evaluation context. Trust anchors, profile versions, policies, evaluation time, revocation state, and appraiser capabilities affect findings. The appraisal carries the evaluation context so that a result is not detached from those dependencies.¶

Privacy. Even opaque targets, basis references, reason codes, and timing information can enable correlation. Carrier and evidence profiles should minimize disclosure and state the confidentiality properties of any commitments they use.¶

15. IANA Considerations

This document requests creation of a "WEXP Appraisal Reason Codes" registry. The registration policy is Specification Required as defined by [RFC8126]. Each entry contains a token, category (fatal, substantive, or evaluation-gap), default verdict effect, and reference.¶

Initial entries are shown below; the reference for every initial entry is this document.¶

The appraiser derives E_MALFORMED_NORMALIZED_INPUT, E_UNSUPPORTED_SEMANTICS_VERSION, E_PROFILE_MAPPING_INVALID, and E_CLAIM_OUT_OF_DOMAIN through the ordered checks in Section 6.2; they are not valid supplied fatal conditions. The remaining initial fatal tokens can be supplied only under the exact meanings and structurally usable-input rule in that section. Carrier-specific parse or extension errors are outside this Core registry and are neither aliases nor automatic mappings to Core tokens.¶

The Designated Expert should require one unambiguous condition, deterministic category and default effect, and a stable public specification. A registration that would create claim support from an evaluation capability, display label, boundary name, or artifact presence should be rejected.¶

Appendix A. Changes Since draft-sergeev-wexp-core-00

• Separated carrier-neutral appraisal semantics from the Native Record format.¶

• Replaced scalar WL arithmetic with typed claims consisting of a content base and qualifier set.¶

• Made IV applicable to an exact claim at any supported base without raising that base.¶

• Replaced a singular verified level with an exact supported claim set and maximal supported alternatives.¶

• Made appraisal claim-independent and separated exact support from structural order.¶

• Fixed the verdict vocabulary to accept, downgrade, and reject.¶

• Replaced cumulative CC arithmetic with a non-evidentiary evaluation capability vector.¶

• Added normative semantic vectors, exact qualifier predicates, limitation inheritance, and explicit non-inference rules.¶

Appendix B. Disclosure

Portions of this document were developed with the assistance of generative AI tools under human editorial control. The listed authors are responsible for the resulting text.¶

Authors' Addresses