docs(security): land secret-types research note

[arena-ai-coding-agent]

Closes #29

Decision

Land the preserved secret-types direction as research documentation within epistemic-types, not as a new repository. The note is rewritten against the current interfaces and sets out the in-repository path to a possible formal model.

What changed

• Add docs/secret-types.adoc, distinguishing the current epistemic preorder, BeliefModality, proof transport, and Echo resource grades from confidentiality semantics.
• State explicit non-claims: no secret API, security lattice, declassification, noninterference, linearity, or runtime guarantee is implemented here.
• Chart staged next work: threat model/specification, smallest Agda interface, positive and negative proof controls, semantic theorem, then any runtime integration.
• Link from the README and docs index; note it in the changelog.
• Do not restore the retired AUDIT.adoc.

Proof-scope check

The issue body refers to 23 --safe modules. The current checkout has 17 Agda modules under src/EpistemicTypes/; the recursive proof script checks all 17 with --safe --without-K --no-libraries. The note reports the current count and makes no confidentiality claim based on those proofs.

Validation

• git diff --check passed.
• The local environment has neither just nor agda, so I could not run the Agda gates here; please rely on the required CI proof and rejection-control jobs before merge.

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 5d6fbb1f-255f-4dc0-b77c-9dd693c1d8ff

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}