Skip to content
Merged
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
29 changes: 29 additions & 0 deletions .claude/CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -152,3 +152,32 @@ package definitions (not metadata files) and must NOT be deleted.
- SHA-pinned dependencies
- SPDX license headers on all files

## Owner norms (2026-10-14)

These come from the owner. The format rules point at their normative
source in `hyperpolymath/standards`; read that, not a paraphrase.

### Asking the owner

- Ask decisions with the selector tool (structured options, the
recommended one first, with what each option implies). Use prose only
for reports and explanations.
- Work lands as **stacked PRs**: small, each independently reviewable.
- Fix a finding at its source before reaching for a baseline or ledger.
The governance exemption ratchet rejects ledger growth unless a commit
or the PR body carries a `Ratchet-exception:` line naming that ledger.

### Formats (standard, estate-wide)

| Kind | Standard | Source |
|------|----------|--------|
| YAML | KYAML, formatted with standards `scripts/kyaml-format.sh` (mikefarah yq v4 with the KYAML encoder). Estate-owned config uses `.kyaml` unless a tool fixes the name. No Python YAML parser. | `3-practice/YAML-POLICY.adoc` §3.4 (D280, D307, D293) |
| Workflows | KYAML too, but only through the step 6 gate in `standards#1025` (Dependabot / `gh actions-lock` drift accepted in writing, lock coverage, `actionlint`, a run proof per workflow). Lockfiles such as `actions.lock` are tool-owned: never hand-edit or reformat them. | `YAML-POLICY.adoc` §5–§6 |
| JSON | I-JSON (RFC 7493) serialised as JCS (RFC 8785), plus exactly one final LF. Extensions do not change. JSONL is one JCS object per line. JSONC files (`devcontainer.json`, `.vscode/`) are exempt. | `3-practice/JSON-POLICY.adoc` (D306) |
| UUID | Current policy: UUIDv7 for records and events, and UUIDv8 over JCS content bytes for content IDs. Keep this split until the corresponding `ids.rs` migration lands. Apply the Profile T/C rule and prohibit new v4/v7 minting after that migration. echidna mints only through `src/rust/ids.rs`. | `docs/decisions/ADR-008-uuid-v8-estate-standard.adoc` (D305, D305b, D320) |

Keep another format only where a consumer the owner does not control
would break (for example a tool that rewrites the file). Record why
beside the file. Tools the owner controls are changed to handle the
standard instead of being exempted.

7 changes: 4 additions & 3 deletions docs/ROADMAP.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -212,9 +212,10 @@ kernel‑checked translation. `+ResultArbiter+` grades each verdict
(ECH‑05), so a synonym collision cannot reach `+sound+`; dispatch attaches
no evidence yet, so every dispatched verdict is `+belief+`
|*A `+KernelTranslation+` certificate is producible for a named backend
pair*, and a verdict on that pair reaches `+sound+`. First candidate:
HOL4 ↔ HOL Light through OpenTheory (6a); then Lean 4 ↔ Rocq through
Dedukti (6b). Pair table: `+docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc+`
pair*, and a verdict on that pair reaches `+sound+`. First target (owner
decision, 2026-10-14): HOL4 ↔ HOL Light through OpenTheory (6a); next
candidate Lean 4 ↔ Rocq through Dedukti (6b). Pair table:
`+docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc+`
§ "Backend pairs that can share a term"
|===

Expand Down
2 changes: 1 addition & 1 deletion docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ certificate for one pair is the ROADMAP stage 6 acceptance.
|Backend pair |`ExchangeFormat` |External route |In ECHIDNA
|HOL4 ↔ HOL Light |`open_theory` |OpenTheory articles, both directions;
checked by the OpenTheory article reader |DESIGNED (`opentheory.rs`
exports and imports proof states, not checked articles); first candidate
exports and imports proof states, not checked articles); first target (2026-10-14)
|Lean 4 ↔ Rocq |`dedukti` / `lambdapi` |Lean and Coq encodings in λΠ
modulo (Lean4Less/lean4dk, CoqInE); checked by Dedukti or Lambdapi
|DESIGNED (`dedukti.rs`, `lambdapi.rs` translate syntax only)
Expand Down
8 changes: 4 additions & 4 deletions issues/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ awk 'f;/^# /{f=1}' issues/<file> | sed '1{/^$/d}' > /tmp/body.md
| ECH-02 | hyperpolymath/echidna | #421 | `echidna-02-cmaes-julia-gnn.md` |
| ECH-03 | hyperpolymath/echidna | #422 | `echidna-03-chapel-island-migration.md` |
| ECH-04 | hyperpolymath/echidna | #424 | `echidna-04-ffi-abi-bridge.md` |
| ECH-05 | hyperpolymath/echidna | not filed | `echidna-05-fidelity-evidence.md` |
| ECH-05 | hyperpolymath/echidna | #431 | `echidna-05-fidelity-evidence.md` |
| PB-01 | hyperpolymath/proof-burrower | not filed | `proof-burrower-01-combinatorial-tactic-synthesis.md` |
| PB-02 | hyperpolymath/proof-burrower | not filed | `proof-burrower-02-ledger-fitness-formulation.md` |
| EB-01 | hyperpolymath/echidnabot | not filed | `echidnabot-01-adaptive-ci-portfolio-scheduler.md` |
Expand All @@ -30,7 +30,7 @@ awk 'f;/^# /{f=1}' issues/<file> | sed '1{/^$/d}' > /tmp/body.md
## Status

- **ECH-01..04** are filed on hyperpolymath/echidna and carry all their labels. On 2026-10-09 their bodies were replaced by hand with a different text that is not these files; the owner decides which is canonical (see `docs/handover/PARADISEO-ROADMAP-PROMPT.adoc`, WP0). `scripts/issues/sync-roadmap-issues.sh` syncs the bodies from these files (dry run by default; refuses to replace hand-edited bodies without `--overwrite`).
- **ECH-05** is a draft for hyperpolymath/echidna, not filed. Its implementation (fidelity evidence on `ProverAttempt`, `level` on `ArbitratedVerdict`, `EchidnaABI.Arbitration`, the fidelity tests) lands with the PR that adds the file.
- **ECH-05** is filed as #431 and closed as completed by #430 (fidelity evidence on `ProverAttempt`, `level` on `ArbitratedVerdict`, `EchidnaABI.Arbitration`, the fidelity tests). It is the arbiter-typing slice of #429, which stays open for one-kernel (Agda) ingestion of fibre coverage, round-trip and cross-prover agreement.
- **PB-01, PB-02, EB-01** are drafts for copying to their own repositories. They are not filed.

## Provenance of the PB and EB drafts
Expand All @@ -49,6 +49,6 @@ Labels named in the drafts that did not exist when they were written (checked 20
|------------------------------|---------------------------------------------------------------------|
| hyperpolymath/proof-burrower | `area:swarm`, `rust`, `search-tactics`, `area:ledger`, `heuristics` |
| hyperpolymath/echidnabot | `area:dispatcher`, `ci-optimization` (`rust` exists) |
| hyperpolymath/echidna | `area:arbitration`, `area:exchange`, `epistemic-types`, `residual-evidence-types` (ECH-05; checked 2026-10-14) |
| hyperpolymath/echidna | none on the repo since #431 created `area:arbitration`, `area:exchange`, `epistemic-types`, `residual-evidence-types` (default colour, no description); they are not yet in the estate label source (`.github/labels.json` is generated from hyperpolymath/.git-private-farm) |

All labels used by ECH-01..04 exist on hyperpolymath/echidna; ECH-05's `enhancement` and `idris2` do.
All labels used by ECH-01..05 exist on hyperpolymath/echidna.
20 changes: 19 additions & 1 deletion tests/arbitration_regression_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,10 @@
//! the ECH-05 additions, and every replayed verdict must sit at level
//! `belief` — the attempts carry no fidelity evidence.
//!
//! The fixture is JCS (RFC 8785) I-JSON, the estate format standard;
//! `fixture_is_jcs_canonical` keeps it that way. It was re-serialised to
//! JCS after generation without changing any value.
//!
//! Regenerate only at a commit whose numbers are the intended reference:
//!
//! ```sh
Expand Down Expand Up @@ -296,7 +300,21 @@ fn regenerate_arbitration_fixture() {
"tolerance": TOLERANCE,
"cases": replay(),
});
let mut out = serde_json::to_string_pretty(&doc).unwrap();
// Estate format standard: JCS (RFC 8785) I-JSON, plus the final LF
// that .editorconfig requires.
let mut out = serde_json_canonicalizer::to_string(&doc).unwrap();
out.push('\n');
std::fs::write(FIXTURE, out).expect("write fixture");
}

#[test]
fn fixture_is_jcs_canonical() {
let raw = std::fs::read_to_string(FIXTURE).expect("fixture present");
let body = raw.strip_suffix('\n').expect("fixture ends with one LF");
let value: Value = serde_json::from_str(body).expect("fixture is JSON");
assert_eq!(
body,
serde_json_canonicalizer::to_string(&value).unwrap(),
"fixture must be JCS (RFC 8785) canonical"
);
}
Loading
Loading