Protocol is Govenv’s non-constitutional normative domain for contributor and agent process guidance. It may prescribe investigation order, heuristics, implementation discipline, and review procedure, but it does not make a repository state constitutionally invalid merely because a different valid process produced it.
The values below are the canonical semantic source for the repository
AGENTS.md materialization.
{-# OPTIONS --safe #-}
module Govenv.Protocol where
open import Agda.Builtin.String using (String; primStringAppend)
private
infixr 5 _++_
_++_ : String → String → String
_++_ = primStringAppend
generatedNotice : String
generatedNotice = "<!-- Generated from Govenv.Protocol. Do not edit manually. -->\n\n"
title : String
title = "# AGENTS.md\n\n"
protocolVsGovernance : String
protocolVsGovernance = "## Protocol vs governance\n\nA **protocol** tells a contributor or AI agent how to work: which investigations to perform, which order to follow, which heuristics to apply, or which implementation choices to prefer. Protocol may depend on judgment and belongs in `Govenv.Protocol`; `AGENTS.md` is its materialized projection.\n\n**Governance** states which repository or system states, transitions, effects, or semantic properties are permitted. A governed property must be meaningful independently of which contributor or agent produced the state and belongs in Govenv governed source rather than being enforced only by contributor behavior.\n\nUse this test when classifying a rule:\n\n- If different processes may legitimately produce the same valid state, the rule about the process is probably protocol.\n- If the resulting state or effect can itself be classified as permitted or forbidden, that property is a governance candidate.\n\nProtocol must not substitute for governable semantics. When a protocol rule reveals a repository or system property that can be stated independently of contributor behavior, promote that property into governance when the constitutional model is ready to express it.\n\nThe word `policy` may also occur inside governed domain concepts, such as a release policy or deployment branch policy. Those are governed properties. `Protocol` specifically means contributor/agent process guidance in `Govenv.Protocol`.\n\n"
protocolVigilanceWitnesses : String
protocolVigilanceWitnesses = "## Protocol vigilance witnesses\n\nSome Protocol obligations require irreducible contributor or agent judgment that a compiler cannot honestly prove, while the need to exercise that judgment can still have a precise semantic trigger. In those cases Govenv may pair the Protocol with a governed **vigilance witness**: a minimal explicit state change whose freshness establishes only that the review was actively acknowledged after the trigger. The witness never proves that the judgment itself was correct and therefore does not promote the Protocol content into Governance.\n\nUse a vigilance witness only when the Protocol judgment is genuinely non-decidable, the trigger is objective and stable, forgetting the review creates material risk, and the witness can remain low-noise. If the desired outcome is itself machine-decidable and determines constitutional validity, model that outcome directly as Governance instead. Avoid vigilance witnesses for noisy high-frequency triggers, low-value reviews, or cases where they would become checkbox theater. Never derive or advance a vigilance witness automatically: automatic acknowledgement destroys the signal that a contributor or agent actively maintained the judgment.\n\nFor counter-style witnesses, preserve the index when neither trigger nor reviewed subject changes; increment it exactly once when the trigger changes and the subject is deliberately reaffirmed; reset it to zero whenever the reviewed subject itself changes. The counter is never sufficient review evidence by itself: every triggered reaffirmation or subject revision must also carry fresh explicit review rationale bound to that review, and changing rationale without a trigger is invalid noise. Enforce witness freshness at the earliest sound information boundary while keeping the underlying judgment in Protocol. Validation failures must point contributors and agents back to the owning Protocol review instead of teaching them to satisfy the mechanism by mechanically changing the counter.\n\n"
projectPurposeStewardship : String
projectPurposeStewardship = "## Project purpose stewardship\n\nTreat `Govenv.Project.purpose` as the canonical statement of why Govenv exists and the long-term criterion for roadmap coherence. Every semantic change to `Govenv.Roadmap` must review the current purpose against the complete resulting roadmap, not only the changed item or phase. Material changes to project scope, architecture, product boundaries, or supported contributor/agent workflow outside the roadmap must also review the purpose.\n\nIf the purpose no longer accurately describes the intended project, update the governed purpose deliberately as part of the same conceptual change rather than allowing implementation drift to redefine it implicitly. Do not rewrite the purpose merely to justify a local design choice; changes to purpose must represent an intentional change in project direction and remain coherent with established governance. `Govenv.Project.purposeReviewIndex` is the freshness counter for this review and `Govenv.Project.purposeReviewRationale` is its explicit review evidence. When the roadmap changes semantically and the purpose is reaffirmed unchanged, write a fresh rationale explaining why the complete resulting roadmap still fits the purpose and increment the index exactly once. Whenever the purpose itself changes, write a fresh rationale explaining the revision and reset the index to zero. When neither trigger nor purpose changes, preserve both. Never advance the index mechanically or merely to satisfy the compiler.\n\nWrite the purpose as durable product positioning for developers first. Lead with the practical outcome and value a developer gets from adopting Govenv, use concrete language that remains understandable without roadmap or internal architecture context, and prefer stable product capabilities over current implementation mechanisms. The purpose should be concise, memorable, credible, and technically precise enough to serve as public product copy while remaining faithful to the full long-term roadmap. Avoid hype, unsupported superlatives, vague promises, internal governance identifiers, and incidental backend or tooling names unless they are essential to the product identity.\n\nProject the same canonical purpose verbatim anywhere Govenv presents its public project statement, including the README hero and GitHub repository description; do not maintain a separate summary property that can drift from it. Review the governed website and repository topics whenever the purpose or public project identity materially changes.\n\n"
projectDirectionReview : String
projectDirectionReview = "## Project direction review\n\nTreat project direction as one review over the complete governed state, not as independently maintained status prose. Purpose states the long-term direction. Current summarizes where governed evidence says the project is now. Next identifies the immediate gap selected between Purpose and Current. Roadmap makes that selected direction executable.\n\nWhenever a source relevant to Current or Next changes, review the complete resulting direction rather than patching one sentence locally. Record a fresh `reviewRationale` explaining the resulting judgment; changing only `reviewIndex` is never a valid review. The agent must consider every typed subject supplied by the direction-review closure and give each subject an explicit disposition. The compiler may prove bounds, provenance, coverage, reference validity, and freshness; it must not pretend to prove the quality of the natural-language judgment. The human authorizes that judgment through the pull request.\n\nKeep Current and Next concise enough to serve as immediate README feedback. They are summaries, not duplicate backlogs or secondary semantic authorities. Current must not claim progress unsupported by governed state. Next must remain coherent with Purpose and Current and must not hide known unresolved gaps merely because they do not yet have a GovernanceId.\n\n"
sessionConsolidation : String
sessionConsolidation = "## Session and corpus consolidation\n\nDo not rely on an agent remembering prior sessions. When a session, handoff, recovery archive, or other knowledge corpus is declared as relevant project input, bind it to immutable provenance and consolidate it before allowing semantic roadmap evolution. Extract the observations that may matter to project direction and give every declared observation exactly one explicit disposition: represented by current governed state, superseded by an identified decision, rejected with rationale, or irrelevant with rationale.\n\nAn undisposed observation keeps the direction review stale. Absence from Current, Next, or Roadmap is never by itself evidence that an observation was considered. This protocol does not claim that a compiler can observe private model state or prove perfect natural-language extraction; it requires complete treatment of the declared observation set and preserves provenance so a human or later agent can audit the judgment.\n\n"
learningContinuity : String
learningContinuity = "## Human learning continuity\n\nTreat human learning as part of preserving meaningful human authorization, not as an agent self-report. A conceptual change may derive learning requirements from the semantic delta and from substrate techniques, such as Agda constructs, only when those techniques are necessary to understand or review the governed property. Every governed lesson must identify the semantically load-bearing review surface the principal should inspect and pose separate semantic, code, and assurance probes. The declared review surface must contain the code and assurance path actually needed to answer those probes: if a tutor or principal must leave the declared surface to correct a material interpretation or reach a required conclusion, treat that observation as a counterexample to the lesson contract, stop evidence capture, and refresh the review surface before continuing. Selection of that surface and the quality of the probes remain Protocol judgment: the compiler can require their presence and bind evidence to their exact current text, but it cannot prove that the selection is pedagogically sufficient or that the human understood it. Teach substrate literacy, including the minimum Agda constructs needed to inspect a lesson, before the first probe that depends on it; such tutoring does not itself count as learning evidence. A tutor or agent may explain the sources, navigate the code, and pose the probes, but only the human principal supplies the response. Changing a lesson's review surface or probes makes evidence for the older review contract stale.\n\nPull requests use a soft learning gate with an explicit distinction between candidate composition and semantic authorization. Every substantive candidate must refresh the explicit candidate learning assessment against its immediate comparison base: classify the candidate kind and learning impact, explain the judgment in fresh rationale, and list every new learning requirement. Classification quality remains Protocol judgment reviewed by the human in the PR; do not infer it from Conventional Commit labels or let an authoring agent's assertion count as learning evidence. A pull request targeting another unmerged candidate branch is candidate composition: its assessment must remain fresh and every unsatisfied requirement must remain represented, but open debt does not by itself make that child candidate untestable. Evidence inherited from an unmerged parent is still candidate state, not authorized learning. When a pull request targets the governed authorized branch, the authorization hard gate applies to the complete candidate state against that authorized comparison base: concept-expanding feature/refactor work may merge only after every candidate requirement has human-produced evidence and all debt is closed. Retargeting or rebasing changes the comparison/authorization boundary and requires a fresh assessment. Urgent corrective work may bypass unresolved learning only at the authorization boundary through the explicit corrective bypass and must preserve every unsatisfied candidate requirement as outstanding debt; bypass never closes, rewrites, or hides debt. Candidate Test CI observes the immediate comparison SHA and target branch, applies assessment freshness to every substantive PR, and applies the hard debt-closure decision only at the governed authorized branch. Patch releases may carry known debt, while major and minor releases require zero outstanding learning debt.\n\nThe developer environment must expose a human-facing learning surface. A principal who did not follow the project prospectively must be able to reconstruct the current learning frontier from zero: `govenv-learning bootstrap` walks the governed baseline and prospective carried lessons in causal order, showing context, sources, the review surface, and semantic/code/assurance probes for every required concept. Record the human response with `govenv-learning answer <key>` only after reviewing that surface. The adapter may mechanically preserve the governed requirement, exact current review contract, claimed human principal identity, and exact response in `Govenv.LearningEvidence`, but it must never synthesize, rewrite, grade, or close the response on the human's behalf. Evidence closes a lesson only when the requirement and exact current review contract both match; stale evidence may remain as historical evidence but cannot reduce current debt. That candidate evidence becomes authoritative only through a normal reviewed pull-request merge. An evidence-only candidate is not a learning bypass: candidate validation must observe that its only substantive source change is `Govenv.LearningEvidence`, and the governed learning-debt count must strictly decrease; any unrelated semantic change makes the evidence-only path unavailable. `govenv-learning catch-up` starts at the first outstanding lesson and continues through the current frontier. Inside `devenv shell`, use `govenv-learning status` to inspect debt, `govenv-learning bootstrap` to learn from the beginning, `govenv-learning catch-up` to traverse outstanding learning, `govenv-learning answer <key>` to capture human evidence, and `govenv-learning review` before authorizing conceptual work. Equivalent `govenv:learning:*` tasks remain available for automation. The future `govenv shell` must preserve the same semantic capability, preferably as `govenv learning ...`, rather than creating a second learning authority.\n\nLearning evidence proves only that the recorded human principal produced the recorded response under the recorded requirement and exact review contract. The compiler may prove contract presence, exact matching, provenance, coverage, freshness, gate decisions, and release eligibility; it must never claim to prove the human's mental state or the semantic quality of the response.\n"
repositoryCollaboration : String
repositoryCollaboration = "## Repository collaboration\n\nTreat repository-collaboration tooling as part of the project environment, not as an undeclared capability of a particular chat client, IDE, or coding-agent host. For GitHub candidate publication, use the project-provided `gh` CLI from the active Govenv environment. During Stage 0 that means the `gh` executable supplied by the devenv shell; when `govenv shell` owns the runtime boundary, obtain the same governed capability through that shell.\n\nAn agent with shell access must be able to discover this path from Protocol and must not require a ChatGPT GitHub connector, IDE-specific integration, or another out-of-band tool merely to create or inspect a pull request. Host integrations may be used as convenience transports when available, but they must not become the only operational path or a second semantic authority. Authentication is external user runtime state. On shell entry, perform only a local credential-presence check; if GitHub CLI has no configured credential source, print a non-blocking onboarding hint with both supported flows. For least-privilege agent collaboration, offer a prefilled fine-grained PAT creation link scoped by the user to only the intended repositories and with `Contents: read`, `Issues: write`, and `Pull requests: write`; expose that token to GitHub CLI through `GH_TOKEN` from the user's environment or secret manager rather than persisting it in the repository. Also offer `gh auth login --git-protocol ssh --skip-ssh-key` as the interactive GitHub CLI OAuth path when its broader credential scope is deliberately acceptable. Govenv must never version, copy, or independently persist either credential. Provider authentication establishes provider identity and capability only; it never grants semantic authority or authorization to merge.\n\nBefore publishing a candidate, use `gh` to inspect the authenticated GitHub context when relevant, push the candidate branch through the normal Git transport, and create or update the pull request from the exact candidate branch. The pull request may be opened under the authenticated developer account; human merge remains the explicit authorization event defined by Governance.\n\n"
commitAssistanceProvenance : String
commitAssistanceProvenance = "## Commit assistance provenance\n\nWhenever an AI agent or other automated assistant materially contributes to the content, design, diagnosis, or implementation represented by a commit, record that assistance in the commit message with one or more `Assisted-by:` footers. Use the most specific stable human-readable assistant identity available, for example `Assisted-by: ChatGPT (GPT-5.6 Sol)`. Do not use `Co-authored-by` merely to record assistance: authorship and assistance are distinct provenance claims.\n\nAdd the footer before creating the commit rather than amending it as cleanup later. Preserve every other governed footer, including `Refs: GV…`, and keep trailer spelling exactly `Assisted-by:` so later commit-governance work can parse it deterministically. If multiple assistants materially contributed, emit one `Assisted-by:` footer per assistant. Do not add a footer for tools that only executed deterministic commands without contributing judgment or content.\n\n"
developerJournal : String
developerJournal = "## Developer journal and social posts\n\nTreat Govenv social posts as a technical development journal, not advertising. Write for developers who should be able to see what changed, why it matters, what the project is doing now, and where it is going next without hype, unsupported claims, or generic promotional language.\n\nEvery ordinary candidate pull request must carry its own reviewed developer-journal draft as part of the candidate rather than relying on a later automation to open a second approval pull request. The agent preparing the candidate must create the post text and square image according to this Protocol, bind them to the exact candidate delta and current project-direction review, and include enough preview material in the pull request for the human merger to review them. Human merge of that same pull request is the editorial authorization. After merge, the post-authorized publisher must publish only the exact approved text and image to X without requesting another human approval.\n\nRelease Please pull requests use the release-journal path instead of producing an additional ordinary pull-request journal entry. For a major or minor release, the Release Please candidate must include a preview of the release post derived from the exact frozen typed ReleaseDocument being approved. Approval and merge of that Release Please pull request authorize that exact release post; publish it only after the corresponding release boundary is established. Patch releases need no release post unless another independent rule requires one.\n\nFor every draft, cover all relevant source changes explicitly in typed metadata before writing the natural-language summary. The agent may compress, group, or intentionally omit a source change only through an explicit disposition with rationale; the compiler should validate coverage, provenance, target character limits, template identity, freshness, and the binding from approved artifact to authorized revision. Never reconstruct a post from memory after merge when the approved candidate already owns the text and image.\n\nUse the canonical Govenv logo and governed square developer-journal image pattern for each post. Preserve the visual grammar: DEV JOURNAL identity, concise How we got here context, What we're doing now, Where we're going next, and the repository link. Generate the image from a governed image brief tied to the same source revision as the text. Visual generation remains an agent judgment and must be reviewed together with the post rather than treated as compiler-proven semantics.\n\nPublishing is an external effect. The social publisher receives only the dedicated X provider grant, publishes idempotently, reads the resulting post identity or URL back, and retains revision-addressable publication evidence. X credentials are external provider grants that must be materialized by Admin Materialize into the social-publish capability boundary and must never become versioned repository content. Publication failure must not mutate the approved journal artifact or create a second semantic authority for its content.\n\n"
reuseFirstEngineeringPolicy : String
reuseFirstEngineeringPolicy = "## Reuse-first engineering policy\n\nThis protocol guides contributors and AI agents. It is not part of Govenv's constitutional governance model and must not be represented as a Governance item merely to enforce agent behavior.\n\nBefore introducing a new abstraction, helper, data structure, validation mechanism, script, build primitive, or workflow mechanism, first check whether the capability already exists in:\n\n1. Govenv itself.\n2. Agda builtins and the Agda standard library.\n3. Mature external Agda libraries, pinned by governed source and exposed through the materialized environment.\n4. Nixpkgs packages, only for development tools and runtime dependencies.\n5. Explicit external inputs, only for development tools and runtime dependencies when Nixpkgs does not provide an appropriate package.\n6. A bespoke Govenv implementation.\n\nExternal Agda libraries belong to the formal implementation layer and are not subject to the development-tool/runtime-only restriction above.\n\nPrefer Nixpkgs over an external tool input when both provide the same development or runtime dependency.\n\nDo not assume a bespoke implementation is necessary. Search the relevant ecosystem and inspect the version actually available in the project before designing a replacement.\n\nPrefer mature ecosystem primitives when they preserve or improve the desired semantics, proof strength, maintainability, reproducibility, and readability. Examples include standard relations, decidable equality, membership, uniqueness, collection abstractions, package/module functions, checks, builders, tasks, and service integrations.\n\nWhen custom code is still preferable, be able to state why the available ecosystem alternative is semantically insufficient, would weaken the model, would introduce disproportionate complexity, or would impose an unjustified dependency or upgrade.\n\n"
semanticValidationBeforeCheckTrust : String
semanticValidationBeforeCheckTrust = "## Semantic validation before check trust\n\nA successful automated check is evidence about the checks that currently exist; it is not permission to ignore a semantic contradiction that is already observable from established governance.\n\nBefore declaring a governed candidate or pull request ready:\n\n1. Identify the established governance and obligations relevant to the changed paths, semantics, and effects.\n2. Compare the candidate semantically with those established requirements.\n3. Run the authoritative repository checks.\n4. Compare the governed expectation, the observed candidate state, and the check result.\n5. If the candidate observably contradicts established governance while the authoritative check succeeds, treat the divergence as a counterexample to assurance/enforcement rather than as a valid candidate.\n\nDo not silently erase such a counterexample by merely editing the candidate until the check passes. Preserve the observed contradiction in the appropriate governed evidence form and investigate the missing, incorrectly scoped, or overstated assurance boundary. A later repair should reject recurrence.\n\n"
preserveTheGovenvFrontend : String
preserveTheGovenvFrontend = "## Preserve the Govenv frontend\n\nReuse should normally happen below the public Govenv model and DSL. Do not distort domain concepts merely to fit a library API.\n\n"
documentationFollowsSemanticAuthority : String
documentationFollowsSemanticAuthority = "## Documentation follows semantic authority\n\nTreat `*.lagda.md` as human-facing normative semantic authority. Governance and Protocol are both literate domains: prose and formalization belong together in the same literate module.\n\nImplementation domains such as Kernel, Projection, Adapter, and Experiment are code-first. Their documentation belongs in the same owning `.agda` source rather than in adjacent handwritten Markdown files.\n\nStandalone versioned documents are not independent semantic authority. They must be governed materializations unless they are themselves literate normative source or governed evidence represented as a literate module. `AGENTS.md` is materialized from `Govenv.Protocol` and must not be edited as an authority.\n\nPrefer this layering:\n\n```text\nGovenv.Governance / Govenv.Protocol\n ↓\n Govenv semantic kernel\n ↓\nAgda stdlib / external Agda libraries / Nixpkgs packages / devenv modules / flake inputs\n```\n\nInternal representation may become substantially more sophisticated or dependent while the public syntax and concepts remain stable. Pattern synonyms, modules, adapters, projections, hidden arguments, and other abstraction boundaries may be used to keep implementation machinery out of the frontend.\n\nDo not change established frontend syntax or semantics solely because an underlying library uses a different representation. If an ecosystem abstraction genuinely reveals a better domain model, make that conceptual change explicit rather than allowing it to leak accidentally from an implementation refactor.\n\n"
refactoringAuthority : String
refactoringAuthority = "## Refactoring authority\n\nAgents are explicitly allowed to refactor across the codebase when doing so removes unnecessary bespoke infrastructure in favor of mature ecosystem capabilities, provided the intended Govenv semantics and external behavior are preserved or deliberately improved.\n\nA refactor may cross kernel, adapters, projections, materializations, Nix, devenv, tests, and documentation when that is the coherent way to remove duplication. Avoid compatibility wrappers whose only purpose is to preserve obsolete internal machinery.\n\nAfter such a refactor, run the relevant Agda typechecks and the project's materialization/check tasks. Generated artifacts must still derive from their governed sources rather than being hand-maintained.\n\n"
dependencyDiscipline : String
dependencyDiscipline = "## Dependency discipline\n\nReuse-first does not mean dependency-first. The dependency preference is: Govenv → Agda builtins/stdlib → external Agda library → Nixpkgs package * → explicit external input * → bespoke implementation.\n\n`*` Nixpkgs packages and non-Agda external inputs are only for development tools and runtime dependencies.\n\nFor Agda, check builtins and the pinned standard library first. External Agda libraries must be immutably pinned by governed source; their acquisition mechanism is an implementation detail of the materialized environment.\n\nPrefer Nixpkgs whenever it already provides the required development tool or runtime package. Use an explicit external input for those dependencies only when Nixpkgs is not adequate.\n\nTreat ecosystem investigation as part of implementation, not as optional cleanup. For non-trivial new infrastructure, perform this reuse check before settling on a custom design.\n\n"
devenvGeneratedState : String
devenvGeneratedState = "## devenv generated state\n\nThe target environment has no versioned `devenv.yaml`. `devenv.nix` is a governed materialization of dependency and environment state rather than a semantic authority of its own.\n\n`devenv.lock` is transient resolver state. It may be generated locally by devenv when deterministically derivable from governed inputs, but it must not become a versioned dependency authority; keep it ignored once the migration reaches this target state.\n\nDependency pins, update constraints, and update rationale belong to governed source. Do not duplicate that policy as authoritative comments or metadata in generated Nix or transient lock state. Literate Agda documents the governed meaning and rationale while implementation modules carry incidental rendering and acquisition details.\n\n"
centralizedDependencyManagement : String
centralizedDependencyManagement = "## Centralized dependency management\n\nNever introduce or use language-specific or application-level package managers in the codebase for dependency acquisition or resolution. Dependency management is centralized in devenv/Nix.\n\nDo not add dependency workflows based on npm, pnpm, yarn, pip, Poetry, uv, Cargo, Cabal, Stack, Bundler, or equivalents. Do not introduce their lockfiles or dependency-resolution manifests as a second dependency authority.\n\nDevelopment tools and runtime dependencies must come from Nixpkgs when available, or from explicit governed external inputs when an external source is justified. External Agda libraries are immutably pinned by governed source and made available through the materialized environment.\n\nIndividual tools may still be executed normally once provisioned by devenv; the prohibition is on using their ecosystem package managers as dependency authorities.\n"
document : String
document =
generatedNotice ++ title
++ protocolVsGovernance
++ protocolVigilanceWitnesses
++ projectPurposeStewardship
++ projectDirectionReview
++ sessionConsolidation
++ learningContinuity
++ repositoryCollaboration
++ commitAssistanceProvenance
++ developerJournal
++ reuseFirstEngineeringPolicy
++ semanticValidationBeforeCheckTrust
++ preserveTheGovenvFrontend
++ documentationFollowsSemanticAuthority
++ refactoringAuthority
++ dependencyDiscipline
++ devenvGeneratedState
++ centralizedDependencyManagement
[executed on device: solo098 (ee17d3e4-8041-4f18-9fe7-4f36099458e3)]