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
6 changes: 3 additions & 3 deletions docs/design-node-identity-channels.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
|---|---|---|---|---|
| **Brand identity** (A3/A4 nominal distinctness) | `binding_id` field | #4581 authority-direct stamping at type-env registration / resolve | **YES** — it *is* semantic identity; excluding it would re-open the spelling-collision false-accept | building (#4581 — the linchpin) |
| **Reference** (use→def; callee; the dependency classifier's `BindsTo`) | **no new field** — a substrate fact carried on the `binding_id` channel (the T-9 rider: resolve materializes the use→def relation against the def's `binding_id`) | resolve, same seam as stamping | participates **as structure** (it is an edge/fact, not a field exclusion question) | queued immediately behind #4581 |
| **Provenance** (source anchoring) | opaque occurrence id field | parse, allocator-issued (PROV wave 1) | **NO** — bookkeeping, never identity; two occurrences of `1 + 1` stay structurally equal | held (PROV operator scoping) |
| **Provenance** (source anchoring) | opaque `occurrence_id` field (`OccurrenceId` in `v4.std.node`; sole mint `v4.std.occurrence_id.alloc_occurrence_id`) | parse, allocator-issued (PROV wave 1); off-tree `SpanIndex` carries `OriginEvent` (design-provenance-span.md §4.5) | **NO** — bookkeeping, never identity; two occurrences of `1 + 1` stay structurally equal | building (PROV A-pivot Phase 0 model — field on `Node` lands Phase 1+2 atomically with #4604 span revert) |

## Rules

Expand All @@ -28,8 +28,8 @@
immediately after). PROV's occurrence-id allocator copies the *pattern* but is a distinct
id space — provenance ids and binding ids never share an allocator or a field.
2. **One landing order, one field-moment each:** `binding_id` (#4581) → T-9 rider →
occurrence id (only at PROV GO; the held lane reserves its row here, not a field in the
tree).
`occurrence_id` (PROV GO 2026-06-10; Phase 0 lands substrate types + allocator; the
`Node` field lands Phase 1+2 atomically with #4604 span revert).
3. **Equality participation is implemented in exactly two places** — the Rust `Value::eq`
authority (v2 interpreter; the #4564 single-equality discipline) and the `.dag`
structural-equality predicate (`exact_structural_equality_zip_fold`) — each citing this
Expand Down
7 changes: 7 additions & 0 deletions src/v4/std/node.dag
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,13 @@
module v4.std.node
type Symbol
type Hash
// PROV A-pivot (design-node-identity-channels.md, design-provenance-span.md §4.1):
// opaque occurrence identity; sole mint via v4.std.occurrence_id.alloc_occurrence_id.
// Distinct id space from binding_id (#4581). Excluded from structural equality / content hash.
// Node.occurrence_id field lands atomically with #4604 span revert (Phase 1+2).
type OccurrenceId {
value: Int
}
// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL.
type Connective
= Atom { identity: Symbol }
Expand Down
28 changes: 28 additions & 0 deletions src/v4/std/occurrence_id.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
// src/v4/std/occurrence_id.dag
// Scope: per-compile occurrence identity allocator (PROV A-pivot wave-1).
// Anchor: design-provenance-span.md §4.1; design-node-identity-channels.md (distinct id space from binding_id).
// Status: Phase 0 model — sole mint path for OccurrenceId; Node field stamping lands Phase 1+2.

module v4.std.occurrence_id

import v4.std.node { OccurrenceId }

type OccurrenceIdAllocator {
next_id: Int
}

fn occurrence_id_allocator_initial() -> OccurrenceIdAllocator {
OccurrenceIdAllocator { next_id: 0 }
}

// SOLE MINT — OccurrenceId { value: ... } constructed only here (#4615 BindingId parity).
fn alloc_occurrence_id(alloc: OccurrenceIdAllocator) -> (OccurrenceId, OccurrenceIdAllocator) {
(
OccurrenceId { value: alloc.next_id },
OccurrenceIdAllocator { next_id: alloc.next_id + 1 }
)
}

fn occurrence_id_eq(left: OccurrenceId, right: OccurrenceId) -> Bool {
left.value == right.value
}
67 changes: 64 additions & 3 deletions src/v4/std/provenance.dag
Original file line number Diff line number Diff line change
@@ -1,14 +1,26 @@
// src/v4/std/provenance.dag
// Scope: source-text → Node byte-range provenance (T-8 producer substrate).
// Status: Layer-3/4 — span on Node (v4.std.node) + parse stamp (v4.compiler.parse).
// Scope: source-text provenance substrate (T-8 / PROV A-pivot).
// Status: transitional — on-tree Node.span (#4604) dissolves Phase 1+2; off-tree SpanIndex
// (OccurrenceId → OriginEvent) is the A-pivot target (design-provenance-span.md §4.5).

module v4.std.provenance

import v4.std.artifact { Artifact, NodeArtifactProvenance }
import v4.std.artifact { Artifact, GeneratorId, NodeArtifactProvenance }
import v4.std.collection {
Absent,
List,
Map,
Present,
empty_map,
map_get,
map_insert
}
import v4.std.diagnostic {
Accepted,
ByteRange,
Diagnostic,
ExternalContractUnknown,
Locus,
Outcome,
Rejected,
Textual,
Expand All @@ -17,6 +29,7 @@ import v4.std.diagnostic {
diagnostics_merge,
outcome_accepted,
outcome_rejected,
port_locus,
rejected_with_pending
}
import v4.std.node {
Expand All @@ -25,6 +38,7 @@ import v4.std.node {
Node,
NodeFold,
NodeSpan,
OccurrenceId,
SourceSpan,
Symbol,
Unanchored,
Expand All @@ -35,6 +49,53 @@ import v4.std.node {
node_span_same_file,
source_span_byte_extent_admits
}
import v4.std.witness { Holds, Violates, Witness }

// --- A-pivot off-tree provenance (design-provenance-span.md §4.5) ---

type OriginEvent
= FromSource { locus: Locus }
| DerivedBy { producer: Symbol, from: List<OccurrenceId> }
| GeneratedBy { generator: GeneratorId, from: List<OccurrenceId> }

fn origin_event_from_source(locus: Locus) -> OriginEvent {
FromSource { locus: locus }
}

type SpanIndex {
events: Map<OccurrenceId, OriginEvent>
}

fn span_index_empty() -> SpanIndex {
SpanIndex { events: empty_map() }
}

fn span_index_record(index: SpanIndex, id: OccurrenceId, event: OriginEvent) -> SpanIndex {
SpanIndex { events: map_insert(m: index.events, key: id, value: event) }
}

data span_index_occurrence_absent: Symbol = span_index_occurrence_absent

fn span_index_occurrence_absent_diagnostic() -> Diagnostic {
Diagnostic {
reason: span_index_occurrence_absent,
at: port_locus(port: ^span_index_lookup_port),
correction: Unavailable { reason: ExternalContractUnknown }
}
}

fn span_index_lookup(index: SpanIndex, id: OccurrenceId) -> Witness<OriginEvent> {
match map_get(m: index.events, key: id) {
Accepted { value: opt, diagnostics: _ } =>
match opt {
Present { value: event } => Holds { value: event }
Absent => Violates { diagnostic: span_index_occurrence_absent_diagnostic() }
}
Rejected { diagnostics: d } => Violates { diagnostic: d.head }
}
}

// --- Transitional on-tree span (#4604; dissolves Phase 1+2) ---

data provenance_span_file_mismatch: Symbol = provenance_span_file_mismatch
data provenance_invalid_source_span: Symbol = provenance_invalid_source_span
Expand Down