Skip to content

docs(f33): MicroInterp P4 burn-down; clear stale pf-ci/cla inventory reds #213

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fraware merged 3 commits into from
Jul 17, 2026
Merged

docs(f33): MicroInterp P4 burn-down; clear stale pf-ci/cla inventory reds #213

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
33498e8
docs(f33): document MicroInterp P4 block; clear stale pf-ci/cla noise
fraware Jul 17, 2026
0d1c927
fix(ci): run pf-ci Kind path for caller events, not workflow_call name
fraware Jul 17, 2026
b34e909
fix(ci): drop unjustified || true in cla-bot contributor dump
fraware Jul 17, 2026
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
130 changes: 76 additions & 54 deletions .github/workflows/cla-bot.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,132 +41,154 @@ jobs:
- name: Get unique contributors
id: contributors
run: |
set -euo pipefail
echo "Analyzing contributors..."
: > contributors.txt

# Get all unique commit authors in this PR
if [ "${{ github.event_name }}" = "pull_request" ]; then
# For PRs, get commits in the PR
git log --format="%an|%ae" ${{ github.event.pull_request.base.sha }}..HEAD | sort -u > contributors.txt
git log --format="%an|%ae" "${{ github.event.pull_request.base.sha }}..HEAD" | sort -u > contributors.txt
elif [ "${{ github.event_name }}" = "push" ]; then
BEFORE="${{ github.event.before }}"
AFTER="${{ github.event.after }}"
if [ -n "$BEFORE" ] && [ -n "$AFTER" ] && [ "$BEFORE" != "0000000000000000000000000000000000000000" ]; then
git log --format="%an|%ae" "${BEFORE}..${AFTER}" | sort -u > contributors.txt
else
echo "Push range unavailable; treating as no contributors for this event"
fi
else
# For pushes to main, get commits in this push
git log --format="%an|%ae" ${{ github.event.before }}..${{ github.event.after }} | sort -u > contributors.txt
# workflow_dispatch (and other non-PR events): inventory/smoke only.
# No commit range — leave contributors empty; Option B skip still applies.
echo "Non-PR event (${{ github.event_name }}): skipping contributor range analysis"
fi

# Extract usernames and emails
cat contributors.txt | cut -d'|' -f1 | sort -u > usernames.txt
cat contributors.txt | cut -d'|' -f2 | sort -u > emails.txt
cut -d'|' -f1 contributors.txt | sort -u > usernames.txt
cut -d'|' -f2 contributors.txt | sort -u > emails.txt

echo "Found contributors:"
cat contributors.txt

- name: Check for exempt users
run: |
set -euo pipefail
echo "Checking for exempt users..."
: > exempt_contributors.txt

# Load exempt users from CLA config
jq -r '.exemptions.whitelisted_users[]' "$CLA_CONFIG_PATH" > exempt_users.txt
jq -r '.exemptions.whitelisted_users[]?' "$CLA_CONFIG_PATH" > exempt_users.txt || : > exempt_users.txt

# Check if any contributors are exempt
while IFS= read -r user; do
if grep -q "^$user$" usernames.txt; then
echo "✅ Exempt user found: $user"
[ -z "$user" ] && continue
if [ -s usernames.txt ] && grep -qxF "$user" usernames.txt; then
echo "Exempt user found: $user"
echo "$user" >> exempt_contributors.txt
fi
done < exempt_users.txt

# Remove exempt users from contributors list
if [ -f exempt_contributors.txt ]; then
grep -v -f exempt_contributors.txt contributors.txt > non_exempt_contributors.txt
if [ -s exempt_contributors.txt ]; then
# Keep non-exempt rows; empty result is fine.
grep -v -F -f exempt_contributors.txt contributors.txt > non_exempt_contributors.txt || : > non_exempt_contributors.txt
else
cp contributors.txt non_exempt_contributors.txt
fi

- name: Check for trivial changes
run: |
set -euo pipefail
echo "Checking for trivial changes..."
echo "TRIVIAL_CHANGES=false" >> "$GITHUB_ENV"
: > changed_files.txt

# Get list of changed files
if [ "${{ github.event_name }}" = "pull_request" ]; then
git diff --name-only ${{ github.event.pull_request.base.sha }}..HEAD > changed_files.txt
git diff --name-only "${{ github.event.pull_request.base.sha }}..HEAD" > changed_files.txt
elif [ "${{ github.event_name }}" = "push" ]; then
BEFORE="${{ github.event.before }}"
AFTER="${{ github.event.after }}"
if [ -n "$BEFORE" ] && [ -n "$AFTER" ] && [ "$BEFORE" != "0000000000000000000000000000000000000000" ]; then
git diff --name-only "${BEFORE}..${AFTER}" > changed_files.txt
fi
else
git diff --name-only ${{ github.event.before }}..${{ github.event.after }} > changed_files.txt
echo "Non-PR event: treating as trivial for CLA smoke"
echo "TRIVIAL_CHANGES=true" >> "$GITHUB_ENV"
fi

# Check if changes are trivial
TRIVIAL_CHANGES=true

# Check for documentation-only changes
if ! grep -q -v "\.md$\|\.txt$\|\.rst$\|docs/" changed_files.txt; then
echo "✅ Documentation-only changes detected"
echo "TRIVIAL_CHANGES=true" >> $GITHUB_ENV
fi

# Check for typo fixes (simplified heuristic)
if [ $(wc -l < changed_files.txt) -lt 3 ]; then
echo "✅ Small number of changes detected"
echo "TRIVIAL_CHANGES=true" >> $GITHUB_ENV
if [ ! -s changed_files.txt ]; then
echo "No changed files in range"
echo "TRIVIAL_CHANGES=true" >> "$GITHUB_ENV"
elif ! grep -q -vE '\.(md|txt|rst)$|^docs/' changed_files.txt; then
echo "Documentation-only changes detected"
echo "TRIVIAL_CHANGES=true" >> "$GITHUB_ENV"
elif [ "$(wc -l < changed_files.txt)" -lt 3 ]; then
echo "Small number of changes detected"
echo "TRIVIAL_CHANGES=true" >> "$GITHUB_ENV"
fi

- name: Verify CLA signatures
id: cla-verify
run: |
set -euo pipefail
echo "Verifying CLA signatures..."

# Option B (ci-health-matrix): when CLA hosted service is unavailable, skip
# verification on workflow_dispatch and do not block push-to-main (no push trigger).
# verification. No push trigger on main; workflow_dispatch is advisory smoke.
if ! curl -fsS --max-time 10 "${CLA_URL}" >/dev/null 2>&1; then
echo "CLA service unreachable at ${CLA_URL}; skipping check (configure hosted CLA or restore API)"
echo "cla_status=success" >> $GITHUB_OUTPUT
echo "missing_contributors=" >> $GITHUB_OUTPUT
echo "cla_status=success" >> "$GITHUB_OUTPUT"
echo "missing_contributors=" >> "$GITHUB_OUTPUT"
exit 0
fi

# Skip CLA check for trivial changes if configured
if [ "$TRIVIAL_CHANGES" = "true" ] && [ "$(jq -r '.exemptions.trivial_changes' "$CLA_CONFIG_PATH")" = "true" ]; then
echo "✅ Trivial changes detected, skipping CLA check"
echo "cla_status=success" >> $GITHUB_OUTPUT
echo "missing_contributors=" >> $GITHUB_OUTPUT
if [ "${TRIVIAL_CHANGES:-false}" = "true" ] && [ "$(jq -r '.exemptions.trivial_changes' "$CLA_CONFIG_PATH")" = "true" ]; then
echo "Trivial changes detected, skipping CLA check"
echo "cla_status=success" >> "$GITHUB_OUTPUT"
echo "missing_contributors=" >> "$GITHUB_OUTPUT"
exit 0
fi

# No contributors (e.g. workflow_dispatch smoke) → success
if [ ! -s non_exempt_contributors.txt ]; then
echo "No non-exempt contributors to verify"
echo "cla_status=success" >> "$GITHUB_OUTPUT"
echo "missing_contributors=" >> "$GITHUB_OUTPUT"
exit 0
fi

# Check each non-exempt contributor
missing_contributors=""

while IFS='|' read -r username email; do
[ -z "${username:-}" ] && continue
echo "Checking CLA for: $username ($email)"

# Call CLA verification API

response=$(curl -s -w "%{http_code}" \
-H "Content-Type: application/json" \
-d "{\"username\": \"$username\", \"email\": \"$email\"}" \
"$CLA_URL/verify")

http_code="${response: -3}"
body="${response%???}"

if [ "$http_code" = "200" ]; then
cla_status=$(echo "$body" | jq -r '.signed // false')

if [ "$cla_status" = "true" ]; then
echo "✅ CLA signed by $username"
echo "CLA signed by $username"
else
echo "❌ CLA not signed by $username"
echo "CLA not signed by $username"
missing_contributors="$missing_contributors $username"
fi
else
echo "❌ CLA verification failed for $username"
echo "CLA verification failed for $username (HTTP $http_code)"
missing_contributors="$missing_contributors $username"
fi
done < non_exempt_contributors.txt

if [ -n "$missing_contributors" ]; then
echo "❌ Missing CLA signatures: $missing_contributors"
echo "cla_status=failure" >> $GITHUB_OUTPUT
echo "missing_contributors=$missing_contributors" >> $GITHUB_OUTPUT
echo "Missing CLA signatures: $missing_contributors"
echo "cla_status=failure" >> "$GITHUB_OUTPUT"
echo "missing_contributors=$missing_contributors" >> "$GITHUB_OUTPUT"
else
echo "✅ All contributors have signed the CLA"
echo "cla_status=success" >> $GITHUB_OUTPUT
echo "missing_contributors=" >> $GITHUB_OUTPUT
echo "All contributors have signed the CLA"
echo "cla_status=success" >> "$GITHUB_OUTPUT"
echo "missing_contributors=" >> "$GITHUB_OUTPUT"
fi

- name: Update GitHub Check
Expand Down
57 changes: 55 additions & 2 deletions .github/workflows/pf-ci.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,33 @@ on:
secrets:
CI_PAT:
required: false
# Lightweight main-branch smoke so inventory is not stuck on stale push-era
# failures. Full Kind/TRUST-FIRE path remains workflow_call (pf-reusable-caller)
# or workflow_dispatch with mode=full.
workflow_dispatch:
inputs:
mode:
description: "smoke (inventory clear) or full Kind/TRUST-FIRE"
required: false
default: "smoke"
type: choice
options:
- smoke
- full
pr_number:
description: "Pull Request Number (full mode only; optional)"
required: false
type: string
run_phases:
description: "Comma-separated TRUST-FIRE phases (full mode; default: 2,3,6)"
required: false
default: "2,3,6"
type: string
kind_cluster_name:
description: "Kind cluster name (full mode)"
required: false
default: "pf-ci"
type: string

env:
PYTHON_VERSION: "3.11"
Expand All @@ -33,8 +60,33 @@ env:
HELM_VERSION: "v3.13.0"

jobs:
dispatch-smoke:
name: PF CI dispatch smoke
# Reusable workflows inherit the *caller's* event_name (pull_request/schedule),
# not workflow_call — only skip Kind when this file is dispatched with mode=smoke.
if: github.event_name == 'workflow_dispatch' && inputs.mode != 'full'
runs-on: ubuntu-latest
timeout-minutes: 5
steps:
- name: Checkout
uses: actions/checkout@v4
with:
fetch-depth: 1

- name: Validate reusable PF CI contract
run: |
set -euo pipefail
test -f .github/workflows/pf-ci.yaml
test -f .github/workflows/pf-reusable-caller.yaml
test -f tests/privacy/privacy_burn_down.py
test -f tests/security/malicious_adapter_test.py
test -f tests/compliance/evidence_kpi_audit.py
echo "pf-ci workflow_dispatch smoke OK (full Kind path via caller / mode=full)"

setup:
name: Setup Toolchain, Kind, and Build Images
# Run for caller invocations (PR/schedule) and for dispatch mode=full.
if: github.event_name != 'workflow_dispatch' || inputs.mode == 'full'
runs-on: ubuntu-latest
timeout-minutes: 90
steps:
Expand Down Expand Up @@ -300,6 +352,7 @@ jobs:

trust-fire:
name: Run TRUST-FIRE Phases 2/3/6 and Gate on PASS
if: github.event_name != 'workflow_dispatch' || inputs.mode == 'full'
runs-on: ubuntu-latest
needs: setup
timeout-minutes: 10
Expand All @@ -322,10 +375,10 @@ jobs:
cleanup:
name: Cleanup Kind Cluster
runs-on: ubuntu-latest
if: always()
if: always() && (github.event_name != 'workflow_dispatch' || inputs.mode == 'full')
needs: [setup, trust-fire]
steps:
- name: Delete Kind cluster
run: |
# ci-honesty: justified wave7-remediation
kind delete cluster --name "${{ inputs.kind_cluster_name }}" || true
kind delete cluster --name "${{ inputs.kind_cluster_name || 'pf-ci' }}" || true
26 changes: 21 additions & 5 deletions core/lean-libs/Runtime/MicroInterp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,24 @@ theorem refinement_preserves_safety
-- This would be proven based on the specific non-interference property
exact (by assumption)

/-- Verification that DFA tables match semantics -/
/-- Verification that DFA tables match semantics.

F33 / P4 burn-down (2026-07-17): both directions stay unfinished on purpose.
The claim is not provable from the current hypotheses alone: `clauses`, `M`,
and `sem` are unconstrained, and there is no in-tree
`compileClauses : List ActionDSL.ActionClause → DFAM × Semantics` (or
equivalent) that couples DFA acceptance to `sem.Checked`.

Burn-down before these placeholders can close:

1. Formalize ActionDSL → DFA export (sidecar compiler) as Lean functions.
2. Define matching `Semantics` from the same clauses so per-step `Checked`
witnesses mirror `δ` / acceptance (likely a trace fold over step checks).
3. Prove soundness + completeness for that pair; derive this biconditional.

Do **not** vacuous-close with `axiom` / `by assumption`, and do **not** add
this file to the lean-style enforced set until both placeholders are gone.
See `docs/internal/lean-sorry-burn-down.md`. -/
theorem dfa_semantics_match
(clauses : List ActionDSL.ActionClause)
(M : DFAM) (sem : Semantics) :
Expand All @@ -193,17 +210,16 @@ theorem dfa_semantics_match
-- Therefore M.accepts τ ↔ sem satisfies τ
∀ τ : ActionDSL.Trace,
M.accepts τ ↔ (∃ w : sem.SidecarWitness, sem.Checked τ w) := by
-- This would be proven based on the specific DFA generation algorithm
-- and semantics implementation
-- Blocked on DFA↔semantics generator (see docstring above).
intro τ
constructor
· -- Prove M.accepts τ → ∃ w : sem.SidecarWitness, sem.Checked τ w
intro h_accepts
-- This would be proven based on the DFA generation algorithm
-- Needs compileClauses soundness (accept ⇒ witness).
sorry
· -- Prove ∃ w : sem.SidecarWitness, sem.Checked τ w → M.accepts τ
intro h_exists
-- This would be proven based on the DFA generation algorithm
-- Needs compileClauses completeness (witness ⇒ accept).
sorry

end PF.Runtime
4 changes: 2 additions & 2 deletions docs/internal/ci-health-matrix.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ Verified on `main` (post-#118): each workflow below runs `make submodules` with
|----------|---------|-----|--------|
| nightly-replay.yml | Instant failure on every push (invalid YAML) | Single workflow definition | Fixed |
| demo-e2e.yml | Runs on all main pushes | Path filter on push | Fixed |
| pf-ci.yaml | `workflow_call` only — spurious failed check on push | No push trigger; caller via pf-reusable-caller | Waived — reusable only |
| pf-ci.yaml | Stale push-era failures; `workflow_call` only | `workflow_dispatch` smoke (default) + full Kind via call/`mode=full`; caller via pf-reusable-caller | Smoke clears inventory; not a SaaS re-gate |

## Required secrets (org prerequisites)

Expand All @@ -165,7 +165,7 @@ Contributor-facing steps: [CONTRIBUTING.md — STANDARDS_GITHUB_TOKEN](https://g
| Secret / service | Workflows blocked | Action |
|------------------|-------------------|--------|
| `STANDARDS_GITHUB_TOKEN` | `platform-cert-validate.yml`, `cert-validate.yml`, `replay.yml`, `evidence-v01-smoke.yml`, `standards-pin.yml`, `docs-build.yaml`, `egress.yml`, `nightly-replay.yml`, `platform-replay.yml` | Org admin steps above; each workflow runs `make submodules` with `STANDARDS_GITHUB_TOKEN` env |
| CLA hosted service | `cla-bot.yaml` (PR only after #118) | **Option B applied:** no `push: main`; skip when `/health` fails. Option A: restore hosted API at URL in `cla/cla.json` |
| CLA hosted service | `cla-bot.yaml` (PR + `workflow_dispatch` after #118) | **Option B applied:** no `push: main`; skip when CLA URL unreachable; dispatch smoke has no contributor range. Option A: restore hosted API at URL in `CLA/cla.json` |
| `CI_PAT` (optional) | `release.yaml` cross-repo dispatch | Only if release workflows must pass in closure sweep |
| `AWS_*` (optional) | `dr-cross.yaml`, `evidence.yaml` | Only if DR/evidence collection scheduled jobs are in scope |

Expand Down
Loading
Loading