Research and design StarIntel proof-carrying ingest #115

Merged

lost-rob0t merged 2 commits from agent/starintel-proof-verification-design into main

2026-08-15 14:52:56 +00:00

lost-rob0t commented

2026-08-15 14:31:12 +00:00

(Migrated from github.com)

What changed

Adds STAR-LANG-RESEARCH-024 defining proof obligations for StarIntel documents, actor protocol conformance, poison-message termination, and bounded deadlock/livelock verification.
Adds STAR-SERVER-033 turning that research into a StarIntel-specific domain-ingest and actor-runtime design.

Why

StarIntel needs precise, testable verification guarantees for document ingest and actor execution without creating a second runtime or overstating what a proof artifact establishes.

The design focuses on four guarantees:

documents conform to the pinned Star-Lang schema and StarIntel domain invariants;
actors only receive and emit message types declared by their pinned protocol manifest;
deterministic poison deliveries leave the active processing path through a one-way terminal disposition;
declared actor/domain-server topologies avoid protocol deadlock and retry livelock under the supported waiting semantics.

Key decisions

Introduces a scoped star.verify.certificate/1 concept rather than a generic proved=true flag.
Separates evidence, checked conformance, lifecycle verification, bounded model checking, solver certificates, and theorem artifacts by assurance class.
Treats schema/domain validity separately from factual truth.
Requires Star-Lang actor asks to use split-phase semantics rather than synchronously occupying the mailbox while waiting on another actor.
Requires blocking ports to be explicit and finite, with static wait-for graph rejection of hard cycles.
Uses bounded protocol model checking as a promotion/audit layer, recording assumptions and bounds instead of claiming an unrestricted theorem.
Requires terminal poison to reject/dead-letter/quarantine without automatic routing back to the active ingest path.
Preserves the one-authority rule: no second dispatcher, lifecycle, actor runtime, ingest framework, or proof database.

Validation

Confirmed the research and design numbering was unused before publication.
Aligned the new nodes with existing Star-Lang research on specification/domain servers, lifecycle semantics, deterministic dispatch, transport settlement, and logic derivations.
Re-read both published files from the branch after creation.
Documentation/research/design only; no runtime implementation is changed in this PR.

## What changed - Adds `STAR-LANG-RESEARCH-024` defining proof obligations for StarIntel documents, actor protocol conformance, poison-message termination, and bounded deadlock/livelock verification. - Adds `STAR-SERVER-033` turning that research into a StarIntel-specific domain-ingest and actor-runtime design. ## Why StarIntel needs precise, testable verification guarantees for document ingest and actor execution without creating a second runtime or overstating what a proof artifact establishes. The design focuses on four guarantees: 1. documents conform to the pinned Star-Lang schema and StarIntel domain invariants; 2. actors only receive and emit message types declared by their pinned protocol manifest; 3. deterministic poison deliveries leave the active processing path through a one-way terminal disposition; 4. declared actor/domain-server topologies avoid protocol deadlock and retry livelock under the supported waiting semantics. ## Key decisions - Introduces a scoped `star.verify.certificate/1` concept rather than a generic `proved=true` flag. - Separates evidence, checked conformance, lifecycle verification, bounded model checking, solver certificates, and theorem artifacts by assurance class. - Treats schema/domain validity separately from factual truth. - Requires Star-Lang actor asks to use split-phase semantics rather than synchronously occupying the mailbox while waiting on another actor. - Requires blocking ports to be explicit and finite, with static wait-for graph rejection of hard cycles. - Uses bounded protocol model checking as a promotion/audit layer, recording assumptions and bounds instead of claiming an unrestricted theorem. - Requires terminal poison to reject/dead-letter/quarantine without automatic routing back to the active ingest path. - Preserves the one-authority rule: no second dispatcher, lifecycle, actor runtime, ingest framework, or proof database. ## Validation - Confirmed the research and design numbering was unused before publication. - Aligned the new nodes with existing Star-Lang research on specification/domain servers, lifecycle semantics, deterministic dispatch, transport settlement, and logic derivations. - Re-read both published files from the branch after creation. - Documentation/research/design only; no runtime implementation is changed in this PR.