Phase 1: Phase 1 specification and invariants #64

Merged

erikinkinen merged 4 commits from 1-phase1-specification-and-invariants into main

2026-03-03 14:29:15 +01:00

erikinkinen commented

2026-03-03 14:28:24 +01:00

Owner

Summary

Closes #24 by adding a decision-complete Phase 1 specification before revocation implementation work.

This PR introduces docs/phase1.md, locking:

full-knowledge assumptions for Phase 1,
formal revocation correctness (soundness and completeness),
minimal deterministic revocation cost counters,
explicit non-failure boundaries vs true revocation failures.

What Changed

Added Phase 1 purpose, scope, out-of-scope, and exit criteria.
Defined full-knowledge assumptions FK1–FK5 with statement + rationale.
Added formal set-based correctness model with symbols:
- E_t, S_t, E'_t, R_t, Residual_t, Over_t.
Locked correctness semantics:
- immediate direct-edge checks,
- no settle window,
- deterministic failure taxonomy:
  - CompletenessViolation
  - SoundnessViolation
  - InvalidRequest
  - InvariantViolation
Defined conceptual interfaces for later implementation:
- RevocationSelector
- RevocationRequestOutcome
- RevocationCostCountersV1
Defined minimal counters and deterministic update rules:
- revocation_requests_total
- revocation_requests_succeeded_total
- revocation_requests_failed_total
- revocation_edges_removed_total
Added non-failure boundaries and explicit failure cases with pass/fail examples.

Validation

Executed after each step/commit:

cmake --build _build
ctest --test-dir _build --output-on-failure
pre-commit run markdownlint --files docs/phase1.md

Result: all checks passed (36/36 tests).

Scope / Non-Changes

Documentation-only PR.
No production code changes.
No API/header/source modifications.
No event-log, replay, or Phase 0 invariant changes.

## Summary Closes #24 by adding a decision-complete Phase 1 specification before revocation implementation work. This PR introduces [docs/phase1.md](/home/erikinkinen/AES/docs/phase1.md), locking: - full-knowledge assumptions for Phase 1, - formal revocation correctness (`soundness` and `completeness`), - minimal deterministic revocation cost counters, - explicit non-failure boundaries vs true revocation failures. ## What Changed - Added `Phase 1` purpose, scope, out-of-scope, and exit criteria. - Defined full-knowledge assumptions `FK1`–`FK5` with statement + rationale. - Added formal set-based correctness model with symbols: - `E_t`, `S_t`, `E'_t`, `R_t`, `Residual_t`, `Over_t`. - Locked correctness semantics: - immediate direct-edge checks, - no settle window, - deterministic failure taxonomy: - `CompletenessViolation` - `SoundnessViolation` - `InvalidRequest` - `InvariantViolation` - Defined conceptual interfaces for later implementation: - `RevocationSelector` - `RevocationRequestOutcome` - `RevocationCostCountersV1` - Defined minimal counters and deterministic update rules: - `revocation_requests_total` - `revocation_requests_succeeded_total` - `revocation_requests_failed_total` - `revocation_edges_removed_total` - Added non-failure boundaries and explicit failure cases with pass/fail examples. ## Validation Executed after each step/commit: - `cmake --build _build` - `ctest --test-dir _build --output-on-failure` - `pre-commit run markdownlint --files docs/phase1.md` Result: all checks passed (`36/36` tests). ## Scope / Non-Changes - Documentation-only PR. - No production code changes. - No API/header/source modifications. - No event-log, replay, or Phase 0 invariant changes.