feat: begin snapshot-bound verification planning

.github/workflows/ci.yml

@@ -32,7 +32,7 @@ jobs:
           python3 -m unittest discover -s scripts/tests -p 'test_*.py'
 
   lean-proof:
-    name: Lean assurance laws
+    name: Lean assurance and SDLC design laws
     runs-on: ubuntu-latest
     timeout-minutes: 20
     steps:
@@ -63,9 +63,18 @@ jobs:
           echo "ELAN_HOME=$ELAN_HOME" >> "$GITHUB_ENV"
           echo "$ELAN_HOME/bin" >> "$GITHUB_PATH"
 
-      - name: Build assurance proof library
+      - name: Build assurance and SDLC proof libraries
         working-directory: proof/lean
-        run: lake build LambdaAitiaModuleAssuranceProof
+        run: lake build LambdaAitiaModuleAssuranceProof LambdaAitiaModuleSdlcProof
+
+      - name: Reject sorry axioms in exported laws
+        working-directory: proof/lean
+        shell: bash
+        run: |
+          set -euo pipefail
+          output="$(lake env lean AxiomAudit.lean)"
+          printf '%s\n' "$output"
+          ! grep -q 'sorryAx' <<< "$output"
 
       - name: Save Lean cache
         if: steps.lean-cache.outputs.cache-hit != 'true'
@@ -76,6 +85,34 @@ jobs:
             proof/lean/.lake
           key: lambda-aitia-lean-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('proof/lean/lean-toolchain', 'proof/lean/lakefile.lean', 'proof/lean/lake-manifest.json') }}
 
+  quint-model:
+    name: Quint lifecycle, retirement and ingress contracts
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout Lambda Aitia
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      - name: Set up Node for pinned Quint
+        uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4.4.0
+        with:
+          node-version: '22'
+
+      - name: Set up Java for Quint TLC backend
+        uses: actions/setup-java@d7793b545071e98d581d3bf084a51c3213318a07 # v4.9.0
+        with:
+          distribution: temurin
+          java-version: '21'
+
+      - name: Install locked Quint and check all 25 model contracts
+        env:
+          AITIA_QUINT_BIN: ${{ github.workspace }}/proof/quint/node_modules/.bin/quint
+          QUINT_HOME: ${{ runner.temp }}/lambda-aitia-quint
+        run: |
+          npm ci --prefix proof/quint
+          mkdir -p "$QUINT_HOME"
+          python3 proof/quint/check_contract.py
+
   scheme-runtime:
     name: Scheme, integration and Python runtime
     runs-on: ubuntu-latest
@@ -89,7 +126,7 @@ jobs:
         uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
         with:
           repository: tao3k/poo-flow
-          ref: da492eea00a7dab502cfb4c7586edefbba96bbec
+          ref: 3a6330f9135b7e5d7a96f9c2de7b5fb90e9ad399
           path: poo-flow
           submodules: false
 
@@ -144,6 +181,35 @@ jobs:
         working-directory: poo-flow
         run: bazelisk run @local_gerbil//:native_scheme_env -- bash -lc 'cd "$BUILD_WORKSPACE_DIRECTORY/packages/lambda-aitia" && just check-semantic'
 
+      - name: Bind Quint and Lean sources to the retirement POO contract
+        working-directory: poo-flow
+        run: bazelisk run @local_gerbil//:native_scheme_env -- bash -lc 'cd "$BUILD_WORKSPACE_DIRECTORY/packages/lambda-aitia" && just test-scheme-atomic formal retirement-binding-test.ss'
+
+      - name: Execute retirement ingress controls against Scheme Host
+        working-directory: poo-flow
+        run: bazelisk run @local_gerbil//:native_scheme_env -- bash -lc 'cd "$BUILD_WORKSPACE_DIRECTORY/packages/lambda-aitia" && just test-scheme-atomic formal retirement-execution-test.ss'
+
+      - name: Set up Node for pinned Quint correspondence traces
+        uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4.4.0
+        with:
+          node-version: '22'
+
+      - name: Replay Quint states and unsafe-model controls through Scheme
+        working-directory: poo-flow
+        run: |
+          npm ci --prefix packages/lambda-aitia/proof/quint
+          bazelisk run @local_gerbil//:native_scheme_env -- bash -lc 'cd "$BUILD_WORKSPACE_DIRECTORY/packages/lambda-aitia" && just check-quint-scheme'
+
+      - name: Set up Java for complete lifecycle state graph
+        uses: actions/setup-java@d7793b545071e98d581d3bf084a51c3213318a07 # v4.9.0
+        with:
+          distribution: temurin
+          java-version: '21'
+
+      - name: Replay every reachable lifecycle state and authorization delivery fault
+        working-directory: poo-flow
+        run: bazelisk run @local_gerbil//:native_scheme_env -- bash -lc 'cd "$BUILD_WORKSPACE_DIRECTORY/packages/lambda-aitia" && just check-lifecycle-scheme'
+
       - name: Run SDLC and GitOps integration
         working-directory: poo-flow
         run: bazelisk run @local_gerbil//:native_scheme_env -- bash -lc 'cd "$BUILD_WORKSPACE_DIRECTORY/packages/lambda-aitia" && just test-integration'

.gitignore

@@ -8,6 +8,8 @@ version.ss
 .cache/
 .bin/
 .lake/
+_apalache-out/
+proof/quint/node_modules/
 __pycache__/
 *.py[cod]
 *.so