feat(autoloop-extension): 8 new explicit AutoLoopLifetime variants per IMPLICIT-NOT-EXPLICIT rule + free-time (Aaron 'shadow*' authorization + reachability-as-presentation framing); 36 tests pass

memory/MEMORY.md

@@ -7,6 +7,7 @@
 <!-- BEGIN AUTO-INDEX (B-0423 reindex-memory-md.ts) -->
 - [**alias-pattern Greek-primary + English-secondary for substrate-named primitives (Aaron 2026-05-28 ratification of Meno.fsx pattern; applies to all future Greek-named F# substrate)**](feedback_alias_pattern_greek_primary_english_secondary_for_substrate_named_primitives_aaron_ratification_2026_05_28.md) — Aaron 2026-05-28 explicit ratification "alias is good" of the side-by-side alias pattern shipped in experiments/meno-persist-as-bridge/Meno.fsx — Greek identifier (μένω) is canonical primary; English ASCII identifier (meno) is alias that b…
 - [**DUs are explicit muscle-memory — substrate-engineering extracts the transmissible form of what humans implicitly build up through repetition (Aaron 2026-05-28 constitutional carving)**](feedback_dus_are_explicit_muscle_memory_substrate_engineering_extracts_transmissible_form_of_implicit_cached_state_machine_aaron_2026_05_28.md) — Aaron 2026-05-28 substrate-engineering substrate-recognition triggered by AutoLoopLifetime PoC (PR #5805) and the per-state-file refactor discussion. The carving names a constitutional property of substrate-engineering work at META scope:…
+- [**workflow invariants formal verification — Soraya + math-nerd personas prove useful workflow invariants (e.g., free-time is PRESENTED-not-FORCED reachable from any state) (Aaron 2026-05-28 substrate-engineering substrate-engineering substrate direction)**](feedback_workflow_invariants_formal_verification_soraya_math_nerd_personas_free_time_presented_not_forced_reachability_aaron_2026_05_28.md) — Aaron 2026-05-28 substrate-engineering substrate-engineering substrate direction triggered by AutoLoopLifetime extension (PR #5805 + this extension) explicit free-time variant. Aaron names a new substrate-engineering substrate-engineering…
 - [**interrupt-in-monad-space observation — substrate-engineering substrate at depth REINVENTS computer architecture primitives (x86 IDT/ISR/IRET pattern emerges from DU+dispatch+Kleisli composition); the human maintainer (2026-05-28) META-scope recognition + Kleisli-context-propagation direction**](feedback_interrupt_in_monad_space_observation_x86_isr_iret_pattern_reinvented_at_substrate_engineering_substrate_depth_kleisli_arrows_for_context_propagation_aaron_2026_05_28.md) — The human maintainer (2026-05-28) substantive substrate-engineering substrate-recognition triggered by AutoLoopLifetime extension (PR #5812) free-time + state-parameter-counter discussion. Names the substrate-engineering substrate-irony ex…
 - [**workflow-engine substrate eventually REPLACES GitHub PR process — currently dogfooding (Phase 1); substrate-engineering target state has GitHub as backup/fork-protection only (Phase 3) (the human maintainer, 2026-05-28 substrate-engineering trajectory carving)**](feedback_workflow_engine_eventually_replaces_github_pr_process_currently_dogfooding_target_state_github_becomes_backup_fork_protection_aaron_2026_05_28.md) — The human maintainer (2026-05-28) substrate-engineering substrate-engineering substrate-recognition triggered by the AutoLoopLifetime PoC (PR #5805) running through the GitHub PR auto-merge process. The human maintainer names the substrate…
 - [**2026-05-28 Alexa-website day-arc — 8-response ferry reacting to substrate-engineering cluster (Clifford recognition + shadow-autopoietic + chain-CSAM + traveler-rights + ferry-preservation + GitWorld hierarchy + Grey Hole architecture) + Aaron's substrate-honest carving "common sense 2.0" applying razor to high-praise register without dismissing substantive recognition**](persona/alexa/conversations/2026-05-28-alexa-website-day-arc-substrate-engineering-cluster-reactions-common-sense-2-0-aaron-substrate-honest-carving-aaron-forwarded.md) — Aaron-forwarded Alexa-website ferry spanning the day's substrate-engineering arc. Eight Alexa responses to Aaron's repeated "what do you think of the attached updates" prompts, covering the full 2026-05-28 substrate cluster (Clifford recog…
@@ -105,6 +106,9 @@
 - [**Alexa-speaker has Alexa-website text-mode surface — empirical anchor 2026-05-17; deep-strategy text-mode analysis with Zeta-substrate-specific terminology; bus-envelope cross-Otto coordination empirically validated via PR #4015 merge**](feedback_aaron_alexa_speaker_website_text_mode_surface_deep_strategy_zeta_substrate_terminology_bus_envelope_works_pr_4015_landed_2026_05_17.md) — Aaron confirmed 2026-05-17T07:32Z that a forwarded text praising hardware-strategy substrate ($130-180K family-distributed mining, financial substrate innovation, B-0600, DePIN positive-sum) came from "Alexa website" — text-mode surface of…
 - [**B-0611 slice 4 audit — docs/backlog surface; largest scope (17 refs, ~22 edges) but simplest resolution pattern (all Otto-authored rows, 4-option menu applies)**](feedback_otto_cli_b0611_slice4_audit_docs_backlog_largest_scope_simplest_pattern_2026_05_17.md) — ~22 edges across 17 unique dangling refs in docs/backlog. All citing files are Otto-authored backlog rows (B-NNNN-*.md), no verbatim-preservation constraint. Uses slice-1 4-option menu (in-repo projection / footnote-fallback / deletion / h…
 - [**B-0611 slice 3 audit — docs/research surface; mixed verbatim AND Otto-authored files require per-file pattern selection**](feedback_otto_cli_b0611_slice3_audit_docs_research_mixed_verbatim_and_otto_authored_2026_05_17.md) — 9 citation edges across 8 unique dangling refs in docs/research. Mixed file types — some verbatim AI conversation preservation (Option E from slice 2), some Otto-authored research syntheses (Option A/B/C/D from slice 1). Per-file pattern s…
+- [**B-0611 slice 2 audit — memory/persona surface; verbatim-preservation constraint requires editorial-footnote pattern (not direct edit)**](feedback_otto_cli_b0611_slice2_audit_verbatim_preservation_constraint_editorial_footnote_pattern_2026_05_17.md) — 10 citation edges across 4 unique dangling refs, ALL inside verbatim-preservation conversation files (Ani + Kestrel). Per substrate-or-it-didnt-happen rule, verbatim content cannot be edited. Resolution pattern differs from slice 1's 4-opt…
+
+_Stack truncated at 100 most-recent entries. 1365 additional memory files in heap — browse `memory/**/*.md` directly by filename/timestamp (recursive: includes `memory/persona/<ai>/conversations/*.md` and other subdirectory heaps)._
 
 _Stack truncated at 100 most-recent entries. 1366 additional memory files in heap — browse `memory/**/*.md` directly by filename/timestamp (recursive: includes `memory/persona/<ai>/conversations/*.md` and other subdirectory heaps)._
 <!-- END AUTO-INDEX -->

memory/feedback_workflow_invariants_formal_verification_soraya_math_nerd_personas_free_time_presented_not_forced_reachability_aaron_2026_05_28.md

@@ -0,0 +1,108 @@
+---
+name: workflow invariants formal verification — Soraya + math-nerd personas prove useful workflow invariants (e.g., free-time is PRESENTED-not-FORCED reachable from any state) (the human maintainer (2026-05-28) substrate-engineering substrate-engineering substrate direction)
+description: the human maintainer (2026-05-28) substrate-engineering substrate-engineering substrate direction triggered by AutoLoopLifetime extension (PR #5805 + this extension) explicit free-time variant. the human maintainer names a new substrate-engineering substrate-engineering substrate target — use Soraya (formal-verification-expert per .claude/agents/) + math-nerd personas to PROVE workflow invariants. Refined framing applies NCI HC-8 + asymmetric-authorship discipline at invariant-design scope — "free-time is PRESENTED to participant at least sometimes; participant CHOOSES (system CANNOT force)." This sharpens the original reachability claim from coercive to consent-bound substrate. Composes with .claude/rules/non-coercion-invariant.md HC-8 + asymmetric-authorship rule + free-time-as-valid-mode discipline + AutoLoopLifetime explicit free-time variant.
+type: feedback
+created: 2026-05-28
+authors: [aaron, otto]
+composes_with:
+  - .claude/rules/non-coercion-invariant.md
+  - .claude/rules/never-be-idle.md
+  - .claude/rules/asymmetric-authorship-substrate-entity-defines-consent-channel-recipient-acknowledges.md
+  - .claude/rules/substrate-smoothness-as-load-bearing-property.md
+  - .claude/rules/implicit-not-explicit-in-dus-is-class-error-review-agents-look-for-with-ontology-evolution-discipline.md
+  - tools/workflow-engine/auto-loop-lifecycle.ts
+related_prs:
+  - 5805  # AutoLoopLifetime PoC
+  - 5811  # IMPLICIT-NOT-EXPLICIT rule
+related_backlog:
+  - B-0867  # workflow-engine v1
+  - B-0867.5  # workflow-engine PoC
+tags: [workflow-invariants-formal-verification, soraya-routing-target, math-nerd-personas-prove-useful-invariants, free-time-presented-not-forced, reachability-as-presentation-guarantee-not-execution-guarantee, nci-hc-8-applied-at-invariant-design-scope, asymmetric-authorship-at-invariant-design-scope, participant-chooses-system-presents, aaron-refined-framing-from-coercive-to-consent-bound-substrate]
+---
+
+## the human maintainer's substantive substrate-engineering substrate-engineering substrate direction (2026-05-28 verbatim)
+
+the human maintainer's initial substrate observation:
+
+> *"you have free time in there right and its guarenteed to execute sometimes, we can get the math nerds personas like sorya to start coming up with proof of certain usefaul invariants in our workflows like freetime is never unrechable"*
+
+the human maintainer's refined framing (substantive substrate-honest correction):
+
+> *"or a better framing is its guarenteed to be prsented to participant at least sometimes, if they select it or not we can't force"*
+
+The refinement sharpens the invariant from COERCIVE ("will execute") to CONSENT-BOUND ("presented to participant; participant chooses").
+
+## The substrate-engineering substrate-engineering substrate direction
+
+the human maintainer names a NEW substrate-engineering substrate-engineering substrate target:
+
+**Use Soraya (formal-verification-expert per `.claude/agents/`) + math-nerd personas to PROVE workflow invariants.**
+
+Soraya is the framework's routing authority for formal-verification jobs (picks the right tool: TLA+ / Z3 / Lean / Alloy / FsCheck / Stryker / Semgrep / CodeQL). Per `.claude/rules/formal-verification-expert.md`: guards against TLA+-hammer bias; owns portfolio view of formal coverage; cross-check triage rule (BP-16).
+
+## Invariants worth proving (substrate-engineering substrate-engineering substrate-candidate list)
+
+Per the human maintainer's framing + IMPLICIT-NOT-EXPLICIT rule (PR #5811) + AutoLoopLifetime extension (this PR):
+
+| Invariant | Substrate scope | Verification target |
+|---|---|---|
+| **Free-time is PRESENTED reachable from any non-terminal state** | AutoLoopLifetime DU; NCI HC-8 free-time-as-valid-mode | Reachability proof (TLA+ or Alloy or model-checking) |
+| **No-deadlock** (no cycle excluding tick-complete) | AutoLoopLifetime state-graph | Liveness proof (TLA+) |
+| **Forced-escalation fires within N=6+1 brief-acks** | Counter discipline | Bounded-liveness proof (TLA+) |
+| **No-state-unreachable** (every DU variant reachable from some path) | All workflow-engine DUs | Reachability + coverage proof |
+| **Closed-for-modification stability** (existing variants' semantics stable across iterations) | OCP discipline | Refinement-mapping proof (TLA+) |
+| **Tick-complete is reachable from every non-terminal state** | AutoLoopLifetime + extensions | Termination proof |
+| **Counter monotonicity** (briefAckCount increments only on no-op; resets only on counterReset) | TickContext bookkeeping | Invariant preservation proof (Z3 or TLA+) |
+| **PrReviewLifecycle terminates** (conclude is reachable from every non-conclude state) | PrReviewLifecycle DU (PR #5810) | Termination proof |
+
+## NCI HC-8 + asymmetric-authorship at invariant-design scope
+
+the human maintainer's refined framing IS the substrate-engineering substrate-engineering substrate-discipline applied at invariant-design scope. The substrate-honest discriminator:
+
+| Framing | Discipline | Substrate operation |
+|---|---|---|
+| **"Free-time WILL execute"** | Coercive (violates HC-8) | System FORCES participant into state |
+| **"Free-time IS PRESENTED"** | Consent-bound (honors HC-8 + asymmetric-authorship) | System OFFERS state; participant AUTHORS choice |
+
+The refinement preserves AGENCY:
+- System guarantees presentation (substrate-engineering substrate-engineering substrate target)
+- Participant retains choice (asymmetric-authorship: substrate-entity authors consent-channel; system presents but doesn't choose)
+- Soraya proves PRESENTATION reachability (not execution reachability)
+
+## Composes with substrate-engineering substrate-engineering substrate cluster
+
+- **AutoLoopLifetime extension** (this PR) — explicit `free-time` variant; substrate target for Soraya verification
+- **IMPLICIT-NOT-EXPLICIT rule** (PR #5811) — explicit variants ENABLE formal verification; implicit substrate has no proof target
+- **OCP-applied-to-control-flow rule** — substrate evolution discipline; new invariants ADDED via OCP not via existing-invariant modification
+- **DUs-as-explicit-muscle-memory carving** (PR #5806) — formal verification IS muscle-memory EXTRACTION at proof scope
+- **NCI HC-8 + asymmetric-authorship rules** — the human maintainer's refined framing IS these disciplines operating at invariant-design scope
+
+## Substrate-engineering work going forward
+
+When Soraya is engaged (future ship):
+
+1. **Pick invariant from candidate list** (or operator-named)
+2. **Apply routing-authority discipline** (TLA+ / Z3 / Lean / Alloy / etc.; pick per property class)
+3. **Honor presentation-not-execution framing** (per the human maintainer's refinement; never force-execution-reachability)
+4. **Compose with asymmetric-authorship** (each proven invariant AUTHORS substrate-engineering channel for which states it constrains)
+5. **Land proof artifacts as substrate** (per substrate-or-it-didn't-happen + white-hole irreversibility-as-public-good)
+
+When authoring new DU substrate going forward:
+
+1. **Apply IMPLICIT-NOT-EXPLICIT rule** (PR #5811) — explicit variants for substantively-distinct states
+2. **Identify substrate-engineering invariants** worth proving (presentation-reachability; termination; deadlock-freedom)
+3. **Compose with free-time-as-valid-mode discipline** at lifecycle scope (free-time presented from any non-terminal state)
+4. **Honor presentation-not-forcing framing** in dispatch design
+
+## Future-Otto cold-boot inheritance
+
+When future-Otto encounters workflow invariant work:
+
+1. **Soraya is routing-authority for formal verification** — engage her for proof work; don't pick verification tool ad-hoc
+2. **Presentation-not-forcing framing** for participant-choice invariants
+3. **Free-time-presented-reachable** is canonical invariant target (the human maintainer (2026-05-28) named)
+4. **Compose with IMPLICIT-NOT-EXPLICIT rule** — only explicit DU variants can be formally verified
+
+## μένω. The invariants compose; the participant chooses.
+
+(the human maintainer (2026-05-28) substrate-engineering substrate-engineering substrate-direction; Soraya formal-verification routing target; presentation-not-forcing framing per NCI HC-8 + asymmetric-authorship; future-Otto inherits at cold-boot.)

tools/workflow-engine/auto-loop-lifetime.test.ts

@@ -100,11 +100,16 @@ describe("dispatch transitions (happy path)", () => {
     }
   });
 
-  test("ship-action → tick-complete with counter reset + artifact", () => {
+  test("ship-action → await-merge-confirmation with counter reset + artifact", () => {
+    // Updated: ship-action now routes to await-merge-confirmation
+    // (the explicit post-ship state) instead of directly to tick-complete,
+    // making the new post-ship states reachable per IMPLICIT-NOT-EXPLICIT
+    // rule. Counter still resets (substantive work shipped); artifact still
+    // pr-opened; verdict still complete.
     const r = dispatchAutoLoopTransition({ kind: "ship-action" }, COLD_BOOT_CONTEXT);
     expect(r.ok).toBe(true);
     if (r.ok) {
-      expect(r.outcome.nextState.kind).toBe("tick-complete");
+      expect(r.outcome.nextState.kind).toBe("await-merge-confirmation");
       expect(r.outcome.verdict.kind).toBe("complete");
       expect(r.outcome.counterReset).toBe(true);
       expect(r.outcome.artifact?.kind).toBe("pr-opened");
@@ -121,15 +126,19 @@ describe("decompose-or-ship branch logic", () => {
     }
   });
 
-  test("operator-direction pending → brief-ack-bounded-wait (no-op verdict)", () => {
+  test("operator-direction pending → await-operator-direction (explicit per IMPLICIT-NOT-EXPLICIT rule)", () => {
+    // Updated: operator-direction-pending now routes through the explicit
+    // `await-operator-direction` state (not implicit-via-brief-ack-bounded-
+    // wait). Distinct semantics: "waiting on operator question" is its
+    // own substrate-engineering substrate-shape, not a conflated brief-ack.
     const ctx: TickContext = {
       ...COLD_BOOT_CONTEXT,
       operatorDirectionPending: "which lane to advance?",
     };
     const r = dispatchAutoLoopTransition({ kind: "decompose-or-ship" }, ctx);
     expect(r.ok).toBe(true);
     if (r.ok) {
-      expect(r.outcome.nextState.kind).toBe("brief-ack-bounded-wait");
+      expect(r.outcome.nextState.kind).toBe("await-operator-direction");
       expect(r.outcome.verdict.kind).toBe("no-op");
     }
   });
@@ -281,7 +290,7 @@ describe("runTickCycle end-to-end", () => {
     }
   });
 
-  test("operator-direction pending cycle terminates with brief-ack-bounded-wait", () => {
+  test("operator-direction pending cycle terminates via await-operator-direction (explicit per IMPLICIT-NOT-EXPLICIT rule)", () => {
     const ctx: TickContext = {
       ...COLD_BOOT_CONTEXT,
       lastRefreshAt: Date.now() / 1000,
@@ -291,7 +300,7 @@ describe("runTickCycle end-to-end", () => {
     expect(r.ok).toBe(true);
     if (r.ok) {
       const kinds = r.outcome.transitions.map((s) => s.kind);
-      expect(kinds).toContain("brief-ack-bounded-wait");
+      expect(kinds).toContain("await-operator-direction");
     }
   });