project_richard_task_219_cedar_analysis_confronted_VALIDATED_2026_05_02

S2.10 — Cedar Analysis confrontation spike (richard-task #219) — VALIDATED 2026-05-02

Outcome

KILL-CONDITION-NOT-MET on all 4 legs. richard-task #219 (“Cedar Analysis open-source toolkit Phase-1 CI integration spike (~3 weeks)” per ζ-Q2 ξ.+ A-130 aspirational uplift 2026-05-02T05:20 BST) STANDS as Phase-1 commitment. ξ.+ A-130 commitment intact.

This is the FIRST richard-task confrontation spike, exercising the new feedback_confront_richard_tasks_at_creation_time discipline codified 2026-05-02 BST. Locks the pattern that auto-created multi-week obligations get a ½–1 day viability check before being parked as build commitments.

Substantive findings

Tooling

• cedar symcc (Cedar Analysis CLI) ships built-in to cedar-policy-cli 4.10.0 when rebuilt with cargo install cedar-policy-cli --version 4.10.0 --features analyze --force. Pulls cedar-policy-symcc 0.4.0 as optional dependency.
• CVC5 1.2.1 is the SMT solver backend. Static Linux x86_64 binary 29.4MB at https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-x86_64-static.zip. Pinned to symcc 0.4.0 — version-pin tracking convention needed for Phase-1.
• 11 verification verbs: never-errors / always-matches / never-matches / matches-equivalent / matches-implies / matches-disjoint / always-allows / always-denies / equivalent / implies / disjoint.
• Wall-clock per verification query: 6–11ms on a 12-CPU NUC running CVC5 1.2.1 with default solver settings.

Verification scoreboard (12 queries × ~9ms ≈ 100ms total)

Property	Verb	Result
Soundness — never errors (×3 policies)	never-errors	3/3 VERIFIED
No-escalation — invalid grant excluded	disjoint	VERIFIED
No-escalation — wrong grantee excluded	disjoint	VERIFIED
No-escalation — wrong estate excluded	disjoint	VERIFIED
No-escalation — sub-28-day spouse excluded	disjoint	VERIFIED
No-escalation — non-fallback trustee excluded	disjoint	VERIFIED
Coverage / spec — equivalent (vs spec-pair)	equivalent	VERIFIED
Coverage / spec — implies	implies	VERIFIED
Idempotency — no double-distribution	disjoint (state-flag precondition)	VERIFIED
Bug-catch — buggy policy + adversarial	disjoint	DOES NOT HOLD; counterexample generated in 11ms

Phase-1 effort estimate

• ~46 policies × ~30min authoring = ~23h
• ~46 spec-pairs × ~20min = ~15h
• ~230 golden vectors × ~10min = ~38h
• CI integration + G-CEDAR-ANALYSIS-VERIFY gate spec + documentation + runbook = ~30h
• Total ~106h ≈ 13 working days @ 8h/day — comfortable inside 3wk (15-day) budget; ~2 days slack
• Per-CI-run wall-clock: ~138 queries × ~10ms ≈ 1.4s. Well under standard CI-gate budget (5min)
• Net cost ~£15-25K Paul-time-equivalent — matches ~25% slice of ξ.+ A-130’s 219-222 collective £30-40K cost-row

Cedar Analysis vs Catala (richard-task #220)

• Cedar Analysis = POLICY semantics verification (authorization)
• Catala = RULE semantics verification (succession law)
• They are COMPLEMENTARY and BOTH NEEDED for the ξ.+ aspirational-uplift formal-verification narrative
• Neither is redundant; the Cedar-only or Catala-only narrative is weaker by half

Key discipline applications

1. feedback_confront_richard_tasks_at_creation_time (codified 2026-05-02 BST): S2.10 IS this discipline operationalised. ~½ day spike validates a 3wk Phase-1 obligation before Rich signs up. Net result: Rich now KNOWS #219 is realistic; not just a parked auto-task.
2. Refined-prompt v3.6 Step 6e SOFTWARE-INSTALL HANDOFF: install command handed off as single paste-safe bash chain. ~11 min wall-clock total (1m cargo recompile dominant). One paste-safety failure mid-spike (line continuation in smoke-test command got mangled in Rich’s terminal); recovered inline.
3. Refined-prompt v3.6 Step 11 LOGGING-CONTRACT-WITHIN-SAME-SESSION: T-file authoring + arch-state §12 cite + Changelog row + new memory file + MEMORY.md entry + active-work-log update all close within ~30 min of T-file authoring.
4. Refined-prompt v3.6 Step 12 ALTERNATIVES-BEFORE-FALLBACK: alternatives Z3 + Lean 4 + Rosette + Catala formal-verification all pre-installed by Rich in ~/tools/inherit-spike-bin/ BEFORE the spike — but NOT exercised, because kill-condition NOT MET. Discipline correctly distinguishes “pre-installation for readiness” from “exercised under kill-condition”.

Key implications

Audit artefact	Change
richard-task #219 (Cedar Analysis Phase-1 CI integration)	STANDS as Phase-1 commitment
ξ.+ A-130 (ζ-Q2 aspirational uplift)	Commitment INTACT
arch-state v3.19 → v3.20	NEW §12 “Richard-task confrontation spikes” section + S2.10 row VALIDATED + Changelog row
master plan v1.10	UNCHANGED
per-repo BUILD-PLAN	UNCHANGED
Q-003 cascade file	UNCHANGED (S2.10 is NOT part of ε.ι 10-spike suite; separate confrontation lineage)
richard-tasks.md	UNCHANGED (#219 stays open as Phase-1 commitment)
risk register	UNCHANGED

Cross-references

• T-file: ~/off-github/library/projects/inherit/T-spike-eps-iota-S2.10-cedar-analysis-2026-05-02.md v1.0
• Working dir: /tmp/spike-s2.10-cedar-analysis/ (3 INHERIT pilots + 5 adversarials + 1 spec-pair + 1 buggy + 1 idempotent + 1 idempotency-adversarial = 11 .cedar files; 2 .cedarschema files)
• arch-state §12 row + Changelog v3.20: ~/testatetech/docs-strategy/docs/superpowers/specs/inherit-v2-architecture-state.md
• Confrontation discipline source memory: feedback_confront_richard_tasks_at_creation_time.md
• ξ.+ A-130 origin memory: project_zeta_q2_xi_plus_aspirational_uplift_2026_05_02.md
• Companion Catala spike candidate (richard-task #220): not yet confronted; should be next.

Honesty caveats

• PoC was 11 .cedar files; production is ~46 policies × 2 (impl + spec) = ~92 .cedar files. Linear scaling assumption.
• Cedar 4.10 has no first-class DateTime type. Date arithmetic via Long epoch_days works but production may want a Cedar DateTime extension OR push date semantics into Catala.
• Counterexample default-instances are minimal (empty strings, zero longs). Production CI parser to translate CVC5 model output into human-readable Cedar entity instances ~1 day engineering follow-up.
• CVC5 1.2.1 version-pin tracking convention needed (similar to A-33 commit-SHA pinning).
• Multi-policy-set form equivalent --policies1 SET1 --policies2 SET2 with >5 policies per set NOT exercised (Cedar paper claims supported; needs Phase-1 validation at scale).

Wall-clock

• Install handoff: ~10 min Rich-side + 1 min cargo recompile
• 11 .cedar files authored: ~10 min
• 12 verification queries running + interpretation: ~3 min
• T-file authoring: ~10 min
• Logging-contract closure: ~10 min
• Total: ~45 min (~½ day budget honored — closer to ~¼ day)