Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions dag/std/witness_purpose.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
module std.witness_purpose

import std.decl_ref { DeclarationRef }
import std.content_hash { ContentHash }
import std.measure { Millisecond, ByteSize }

type WitnessResourceBound
= EvalWallTimeBound { bound: Millisecond }
| EvalThreadCpuBound { bound: Millisecond }
| PeakMemoryBound { bound: ByteSize }

data witness_purpose_resource_contract_note: String = "ResourceContract bound is axis-typed: wall/cpu limits are Millisecond; peak memory is ByteSize (std.measure). A single Millisecond field on all axes was state-space conflation — PeakMemory with a millisecond bound was writable. Aligns with discrete_cost derivation section 10 bound: Measure; full Measure coproduct lands when the cost consumer derives bounds."

data witness_purpose_authority_note: String = "DECLARED witness purpose taxonomy (operator ruling 2026-08-04; DESIGN witness-cost-derives-from-purpose; discrete-cost-derivation section 10). What semantic fact the witness exists to prove — authored, not inferred from implementation. Cost and placement are DERIVED consequences on ScheduledWitnessEnvelope (std.realization_schedule SpanEnrolled), not here. Slice C-a lands only this stable vocabulary; placement and envelope derivation are separate slices."

data witness_purpose_terminating_one_shot_frontier_note: String = "TerminatingOneShot is NOT a writable WitnessPurpose arm in slice C-a. It demands a pinned subject, a mechanically checkable dissolution trigger, AND a typed deadline after which an undissolved survey REFUSES — without the deadline substrate every permanent witness can claim to be a one-shot. A NonEmptyStr deadline field that always routes to OneShotUnavailable is rung inflation: a named future capability wearing the clothes of a finished arm. TerminatingOneShotFrontier records honest unavailability until std.measure lands typed instant/deadline and completion-receipt carriers; then TerminatingOneShot joins WitnessPurpose and this frontier type deletes."

type WitnessPurpose
= BehavioralDiscriminator
| BoundaryCrossing { modeled_boundary: DeclarationRef, chosen_input: ContentHash }
| PopulationTotality { population: DeclarationRef }
| ExternalFidelity { effect: DeclarationRef }
| ResourceContract { bound: WitnessResourceBound }

type TerminatingOneShotFrontier
= TerminatingOneShotUnavailableDeadlineSubstrateAbsent
| TerminatingOneShotUnavailableCompletionSubstrateAbsent
150 changes: 150 additions & 0 deletions dag/test/claim/witness_purpose_taxonomy_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,150 @@
module test.claim.witness_purpose_taxonomy_witness

import std.decl_ref { decl_ref, DeclarationRef }
import std.content_hash {
ContentHash,
Fnv1a64,
Fnv1a64StructuralDigestHex,
structural_content_hash,
}
import std.measure { millisecond, byte_size, millisecond_count, byte_size_count }
import std.witness_purpose {
WitnessPurpose,
WitnessResourceBound,
BehavioralDiscriminator,
BoundaryCrossing,
PopulationTotality,
ExternalFidelity,
ResourceContract,
EvalWallTimeBound,
EvalThreadCpuBound,
PeakMemoryBound,
TerminatingOneShotFrontier,
TerminatingOneShotUnavailableDeadlineSubstrateAbsent,
TerminatingOneShotUnavailableCompletionSubstrateAbsent,
}

data witness_purpose_taxonomy_witness_note: String = "Slice C-a: stable WitnessPurpose vocabulary only — BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract. TerminatingOneShot is NOT a WitnessPurpose arm; TerminatingOneShotFrontier records honest deferral (deadline and completion substrates absent) until typed carriers land. No placement, envelope, or cadence logic — those are C-b/C-c slices."

fn fixture_subject_hash() -> ContentHash {
Fnv1a64(
structural_content_hash(digest: "deadbeefdeadbeef" as Fnv1a64StructuralDigestHex)
)
}

fn fixture_population_ref() -> DeclarationRef {
decl_ref(
module_path: "dag.test.claim.witness_purpose_taxonomy_witness",
decl_name: "witness_purpose_taxonomy_witness_note",
)
}

test fn behavioral_discriminator_is_stable_purpose_arm() -> Bool {
let purpose = BehavioralDiscriminator
match purpose {
BehavioralDiscriminator => true
BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
PopulationTotality { population: _ } => false
ExternalFidelity { effect: _ } => false
ResourceContract { bound: _ } => false
}
}

test fn boundary_crossing_carries_modeled_boundary_and_chosen_input() -> Bool {
let purpose = BoundaryCrossing {
modeled_boundary: fixture_population_ref(),
chosen_input: fixture_subject_hash(),
}
match purpose {
BoundaryCrossing { modeled_boundary: boundary, chosen_input: hash } =>
boundary == fixture_population_ref()
&& hash == fixture_subject_hash()
BehavioralDiscriminator => false
PopulationTotality { population: _ } => false
ExternalFidelity { effect: _ } => false
ResourceContract { bound: _ } => false
}
}

test fn population_totality_carries_population_ref() -> Bool {
let purpose = PopulationTotality { population: fixture_population_ref() }
match purpose {
PopulationTotality { population: population } =>
population == fixture_population_ref()
BehavioralDiscriminator => false
BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
ExternalFidelity { effect: _ } => false
ResourceContract { bound: _ } => false
}
}

test fn external_fidelity_carries_effect_ref() -> Bool {
let purpose = ExternalFidelity { effect: fixture_population_ref() }
match purpose {
ExternalFidelity { effect: effect } => effect == fixture_population_ref()
BehavioralDiscriminator => false
BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
PopulationTotality { population: _ } => false
ResourceContract { bound: _ } => false
}
}

test fn resource_contract_wall_bound_is_millisecond() -> Bool {
let purpose = ResourceContract {
bound: EvalWallTimeBound { bound: millisecond(count: 500) },
}
match purpose {
ResourceContract { bound: bound } =>
match bound {
EvalWallTimeBound { bound: ms } => millisecond_count(m: ms) == 500
EvalThreadCpuBound { bound: _ } => false
PeakMemoryBound { bound: _ } => false
}
BehavioralDiscriminator => false
BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
PopulationTotality { population: _ } => false
ExternalFidelity { effect: _ } => false
}
}

test fn resource_contract_peak_memory_bound_is_byte_size() -> Bool {
let purpose = ResourceContract {
bound: PeakMemoryBound { bound: byte_size(count: 1073741824) },
}
match purpose {
ResourceContract { bound: bound } =>
match bound {
PeakMemoryBound { bound: bytes } => byte_size_count(b: bytes) == 1073741824
EvalWallTimeBound { bound: _ } => false
EvalThreadCpuBound { bound: _ } => false
}
BehavioralDiscriminator => false
BoundaryCrossing { modeled_boundary: _, chosen_input: _ } => false
PopulationTotality { population: _ } => false
ExternalFidelity { effect: _ } => false
}
}

test fn terminating_one_shot_unavailable_records_deadline_substrate_absent() -> Bool {
let frontier = TerminatingOneShotUnavailableDeadlineSubstrateAbsent
match frontier {
TerminatingOneShotUnavailableDeadlineSubstrateAbsent => true
TerminatingOneShotUnavailableCompletionSubstrateAbsent => false
}
}

test fn witness_purpose_has_five_stable_arms_only() -> Bool {
let purposes = [
BehavioralDiscriminator,
BoundaryCrossing {
modeled_boundary: fixture_population_ref(),
chosen_input: fixture_subject_hash(),
},
PopulationTotality { population: fixture_population_ref() },
ExternalFidelity { effect: fixture_population_ref() },
ResourceContract {
bound: EvalThreadCpuBound { bound: millisecond(count: 1) },
},
]
length(xs: purposes) == 5
}
Loading