mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
200 lines
6.7 KiB
Text
200 lines
6.7 KiB
Text
import Semantics.ReceiptCore
|
|
|
|
/-!
|
|
# Agent Swarm Template Alignment
|
|
|
|
This module translates external agent/swarm template patterns into the local
|
|
AGENTS.md contract:
|
|
|
|
* finite node kinds instead of open prompt routing;
|
|
* explicit evaluation and receipt gates;
|
|
* fail-closed `HOLD` when evidence is missing;
|
|
* invalid receipts force `BLOCKED`.
|
|
|
|
It does not import external template code and it does not claim that any web
|
|
demo is proof-bearing. It only captures the admissibility surface needed before
|
|
such a template can influence the Research Stack.
|
|
-/
|
|
|
|
namespace Semantics.AgentSwarmTemplateAlignment
|
|
|
|
/-- Finite local classes for externally observed template shapes. -/
|
|
inductive TemplateClass where
|
|
| singleAgent
|
|
| supportTriage
|
|
| researchReport
|
|
| codeReviewPipeline
|
|
| retrievalEvaluation
|
|
| contentModeration
|
|
deriving Repr, BEq, DecidableEq
|
|
|
|
/-- Finite node kinds admitted by the local adapter. -/
|
|
inductive TemplateNodeKind where
|
|
| input
|
|
| classifier
|
|
| retriever
|
|
| generator
|
|
| evaluator
|
|
| approver
|
|
| synthesizer
|
|
| output
|
|
deriving Repr, BEq, DecidableEq
|
|
|
|
/-- Promotion state for a translated template. -/
|
|
inductive TemplateStatus where
|
|
| HOLD
|
|
| CANDIDATE
|
|
| REVIEWED
|
|
| BLOCKED
|
|
deriving Repr, BEq, DecidableEq
|
|
|
|
/-- A local, finite representation of one external template pattern. -/
|
|
structure TemplateGraph where
|
|
templateClass : TemplateClass
|
|
nodes : List TemplateNodeKind
|
|
requiresApproval : Bool
|
|
hasEvaluationGate : Bool
|
|
targetId : String
|
|
deriving Repr, BEq
|
|
|
|
/-- Every translated graph must have input and output boundaries. -/
|
|
def hasBoundary (graph : TemplateGraph) : Bool :=
|
|
graph.nodes.contains .input && graph.nodes.contains .output
|
|
|
|
/-- Any template that can affect users, code, or claims must include an evaluator. -/
|
|
def needsEvaluation (templateClass : TemplateClass) : Bool :=
|
|
match templateClass with
|
|
| .singleAgent => false
|
|
| .supportTriage => true
|
|
| .researchReport => true
|
|
| .codeReviewPipeline => true
|
|
| .retrievalEvaluation => true
|
|
| .contentModeration => true
|
|
|
|
/-- Human approval is mandatory for user-visible operational actions. -/
|
|
def needsApproval (templateClass : TemplateClass) : Bool :=
|
|
match templateClass with
|
|
| .supportTriage => true
|
|
| .contentModeration => true
|
|
| _ => false
|
|
|
|
/-- Required receipts for promotion beyond HOLD. -/
|
|
def requiredReceiptKinds (templateClass : TemplateClass) : List ReceiptCore.ReceiptKind :=
|
|
match templateClass with
|
|
| .singleAgent => [.sourceAudit]
|
|
| .supportTriage => [.sourceAudit, .humanReview]
|
|
| .researchReport => [.sourceAudit, .humanReview]
|
|
| .codeReviewPipeline => [.leanBuild, .sourceAudit]
|
|
| .retrievalEvaluation => [.benchmark, .sourceAudit]
|
|
| .contentModeration => [.sourceAudit, .humanReview, .wardenEmission]
|
|
|
|
/-- Structural lawfulness before receipts are considered. -/
|
|
def graphStructurallyLawful (graph : TemplateGraph) : Bool :=
|
|
hasBoundary graph
|
|
&& (!needsEvaluation graph.templateClass || graph.hasEvaluationGate)
|
|
&& (!needsApproval graph.templateClass || graph.requiresApproval)
|
|
|
|
/-- Receipt gate for CANDIDATE promotion. -/
|
|
def hasPromotionReceipts
|
|
(graph : TemplateGraph)
|
|
(receipts : List ReceiptCore.Receipt) : Bool :=
|
|
ReceiptCore.hasAllReceiptKinds receipts graph.targetId (requiredReceiptKinds graph.templateClass)
|
|
|
|
/-- Fail-closed status assignment. -/
|
|
def classifyTemplate
|
|
(graph : TemplateGraph)
|
|
(receipts : List ReceiptCore.Receipt) : TemplateStatus :=
|
|
if ReceiptCore.isBlocked receipts graph.targetId then
|
|
.BLOCKED
|
|
else if !graphStructurallyLawful graph then
|
|
.HOLD
|
|
else if hasPromotionReceipts graph receipts then
|
|
.CANDIDATE
|
|
else
|
|
.HOLD
|
|
|
|
/-- External templates never self-promote to REVIEWED in this adapter. -/
|
|
theorem classifyTemplateNeverReviewed (graph : TemplateGraph) (receipts : List ReceiptCore.Receipt) :
|
|
classifyTemplate graph receipts != TemplateStatus.REVIEWED := by
|
|
unfold classifyTemplate
|
|
by_cases hBlocked : ReceiptCore.isBlocked receipts graph.targetId = true
|
|
· simp [hBlocked]
|
|
rfl
|
|
· by_cases hNotLawful : (!graphStructurallyLawful graph) = true
|
|
· simp [hBlocked, hNotLawful]
|
|
rfl
|
|
· by_cases hReceipts : hasPromotionReceipts graph receipts = true
|
|
· simp [hBlocked, hNotLawful, hReceipts]
|
|
rfl
|
|
· simp [hBlocked, hNotLawful, hReceipts]
|
|
rfl
|
|
|
|
/-- Missing receipts keep a structurally valid template in HOLD. -/
|
|
theorem noReceiptsHold (graph : TemplateGraph)
|
|
(hLawful : graphStructurallyLawful graph = true) :
|
|
classifyTemplate graph [] = TemplateStatus.HOLD := by
|
|
unfold classifyTemplate hasPromotionReceipts
|
|
cases graph with
|
|
| mk templateClass nodes requiresApproval hasEvaluationGate targetId =>
|
|
cases templateClass <;>
|
|
simp [ReceiptCore.isBlocked, ReceiptCore.hasAllReceiptKinds,
|
|
ReceiptCore.hasReceiptOfKind, hLawful, requiredReceiptKinds]
|
|
|
|
/-- Any invalid receipt for the target blocks the template. -/
|
|
theorem invalidReceiptBlocks (graph : TemplateGraph) (kind : ReceiptCore.ReceiptKind) :
|
|
classifyTemplate graph
|
|
[{ kind := kind
|
|
, targetId := graph.targetId
|
|
, summary := "failed validation"
|
|
, valid := false
|
|
, authority := "alignment_check"
|
|
, timestamp := 0 }] = TemplateStatus.BLOCKED := by
|
|
unfold classifyTemplate ReceiptCore.isBlocked
|
|
simp
|
|
|
|
/-- A code-review pipeline with build and source-audit receipts becomes CANDIDATE. -/
|
|
def codeReviewGraph : TemplateGraph :=
|
|
{ templateClass := .codeReviewPipeline
|
|
, nodes := [.input, .generator, .evaluator, .output]
|
|
, requiresApproval := false
|
|
, hasEvaluationGate := true
|
|
, targetId := "agentswarms.code_review_pipeline" }
|
|
|
|
def codeReviewReceipts : List ReceiptCore.Receipt :=
|
|
[ ReceiptCore.leanBuildReceipt codeReviewGraph.targetId true
|
|
, { kind := .sourceAudit
|
|
, targetId := codeReviewGraph.targetId
|
|
, summary := "external template mapped to finite local node kinds"
|
|
, valid := true
|
|
, authority := "agent_swarm_alignment"
|
|
, timestamp := 1 } ]
|
|
|
|
theorem codeReviewGraphCandidate :
|
|
classifyTemplate codeReviewGraph codeReviewReceipts = TemplateStatus.CANDIDATE := by
|
|
native_decide
|
|
|
|
/-- A support triage graph without human approval fails closed. -/
|
|
def unsafeSupportGraph : TemplateGraph :=
|
|
{ templateClass := .supportTriage
|
|
, nodes := [.input, .classifier, .generator, .evaluator, .output]
|
|
, requiresApproval := false
|
|
, hasEvaluationGate := true
|
|
, targetId := "agentswarms.support_triage" }
|
|
|
|
theorem unsafeSupportGraphHeld :
|
|
classifyTemplate unsafeSupportGraph [] = TemplateStatus.HOLD := by
|
|
native_decide
|
|
|
|
#eval graphStructurallyLawful codeReviewGraph
|
|
-- Expected: true
|
|
|
|
#eval classifyTemplate codeReviewGraph []
|
|
-- Expected: HOLD
|
|
|
|
#eval classifyTemplate codeReviewGraph codeReviewReceipts
|
|
-- Expected: CANDIDATE
|
|
|
|
#eval classifyTemplate unsafeSupportGraph []
|
|
-- Expected: HOLD
|
|
|
|
end Semantics.AgentSwarmTemplateAlignment
|