chore: Wave 9 engineering cleanup and Wave E/11/13 delivery #137
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: Apache-2.0 | |
| # Copyright 2025 Provability-Fabric Contributors | |
| name: Allowlist Sync Validation | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| on: | |
| push: | |
| branches: [main, develop] | |
| paths: | |
| - "core/lean-libs/**" | |
| - "bundles/**/proofs/**" | |
| - "tools/gen_allowlist_from_lean.py" | |
| - "runtime/sidecar-watcher/policy/allowlist.json" | |
| pull_request: | |
| branches: [main, develop] | |
| paths: | |
| - "core/lean-libs/**" | |
| - "bundles/**/proofs/**" | |
| - "tools/gen_allowlist_from_lean.py" | |
| - "runtime/sidecar-watcher/policy/allowlist.json" | |
| jobs: | |
| validate-allowlist-sync: | |
| runs-on: ubuntu-latest | |
| name: Validate Allowlist Sync | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Set up Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: "3.11" | |
| - name: Install dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| pip install -r tools/requirements.txt || echo "No requirements.txt found" | |
| - name: Install Lean 4 | |
| run: | | |
| curl -fsSL https://raw.githubusercontent.com/leanprover/elan/v4.2.1/elan-init.sh | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| export PATH="$HOME/.elan/bin:$PATH" | |
| TOOLCHAIN=$(tr -d '\n\r' < lean-toolchain) | |
| elan toolchain install "$TOOLCHAIN" | |
| elan override set "$TOOLCHAIN" | |
| lean --version | |
| - name: Vendor mathlib | |
| run: | | |
| chmod +x scripts/vendor-mathlib.sh | |
| bash scripts/vendor-mathlib.sh | |
| - name: Build Lean proofs | |
| run: | | |
| cd core/lean-libs | |
| if [ -f "lakefile.lean" ]; then | |
| lake build | |
| else | |
| echo "No lakefile.lean found, skipping Lean build" | |
| fi | |
| - name: Generate allowlist from Lean | |
| run: | | |
| python3 tools/gen_allowlist_from_lean.py . /tmp/generated_allowlist.json | |
| - name: Compare with committed allowlist | |
| run: | | |
| echo "Comparing generated allowlist with committed version..." | |
| if [ ! -f "runtime/sidecar-watcher/policy/allowlist.json" ]; then | |
| echo "Committed allowlist not found!" | |
| exit 1 | |
| fi | |
| python3 - <<'PY' | |
| import json | |
| import sys | |
| VOLATILE = {"generation_timestamp", "lean_environment", "workspace_hash", "validation_status"} | |
| def normalize_paths(obj): | |
| if isinstance(obj, dict): | |
| return {k: normalize_paths(v) for k, v in obj.items()} | |
| if isinstance(obj, list): | |
| return [normalize_paths(v) for v in obj] | |
| if isinstance(obj, str): | |
| return obj.replace("\\\\", "/").replace("\\", "/") | |
| return obj | |
| def canonical(path: str) -> dict: | |
| with open(path, encoding="utf-8") as f: | |
| data = json.load(f) | |
| for key in VOLATILE: | |
| data.pop(key, None) | |
| return normalize_paths(data) | |
| committed = canonical("runtime/sidecar-watcher/policy/allowlist.json") | |
| generated = canonical("/tmp/generated_allowlist.json") | |
| # Tool capabilities are the security-critical sync surface; policies/metadata | |
| # vary with Lean vendor layout and path formatting across platforms. | |
| if committed.get("tools") != generated.get("tools"): | |
| print("ALLOWLIST SYNC VALIDATION FAILED") | |
| print("Committed and generated tool capabilities differ.") | |
| sys.exit(1) | |
| print("Allowlist sync validation passed") | |
| PY | |
| - name: Validate allowlist structure | |
| run: | | |
| echo "Validating allowlist structure..." | |
| python3 -c " | |
| import json | |
| import sys | |
| with open('runtime/sidecar-watcher/policy/allowlist.json', 'r') as f: | |
| allowlist = json.load(f) | |
| # Check required fields | |
| required_fields = ['version', 'generated_from', 'tools', 'sync_with_lean'] | |
| missing_fields = [field for field in required_fields if field not in allowlist] | |
| if missing_fields: | |
| print(f'❌ Missing required fields: {missing_fields}') | |
| sys.exit(1) | |
| # Check sync_with_lean is true | |
| if not allowlist.get('sync_with_lean', False): | |
| print('❌ sync_with_lean must be true') | |
| sys.exit(1) | |
| # Check each tool has required fields | |
| for tool_name, tool_config in allowlist['tools'].items(): | |
| required_tool_fields = ['can_use', 'conditions', 'source_file'] | |
| missing_tool_fields = [field for field in required_tool_fields if field not in tool_config] | |
| if missing_tool_fields: | |
| print(f'❌ Tool {tool_name} missing fields: {missing_tool_fields}') | |
| sys.exit(1) | |
| print('✅ Allowlist structure validation PASSED!') | |
| print(f'Validated {len(allowlist[\"tools\"])} tools') | |
| " | |
| - name: Check for drift indicators | |
| run: | | |
| echo "Checking for drift indicators..." | |
| # Check if any tools have default_deny without Lean proofs | |
| python3 -c " | |
| import json | |
| with open('runtime/sidecar-watcher/policy/allowlist.json', 'r') as f: | |
| allowlist = json.load(f) | |
| drift_issues = [] | |
| for tool_name, tool_config in allowlist['tools'].items(): | |
| # Check for tools that default to deny due to missing Lean proofs | |
| if (tool_config.get('capability_type') == 'default_deny' or | |
| not tool_config.get('lean_definition', True)): | |
| drift_issues.append(f'Tool {tool_name} lacks explicit Lean capability proof') | |
| if drift_issues: | |
| print('⚠️ DRIFT DETECTED:') | |
| for issue in drift_issues: | |
| print(f' - {issue}') | |
| print('') | |
| print('Consider adding explicit CanUse proofs in Lean for these tools.') | |
| # Don't fail CI for drift warnings, just notify | |
| else: | |
| print('✅ No drift detected - all tools have explicit Lean proofs') | |
| " | |
| - name: Generate drift report | |
| if: always() | |
| run: | | |
| echo "Generating drift report..." | |
| python3 -c " | |
| import json | |
| from datetime import datetime | |
| with open('runtime/sidecar-watcher/policy/allowlist.json', 'r') as f: | |
| allowlist = json.load(f) | |
| report = { | |
| 'timestamp': datetime.utcnow().isoformat(), | |
| 'commit_sha': '${{ github.sha }}', | |
| 'branch': '${{ github.ref_name }}', | |
| 'total_tools': len(allowlist['tools']), | |
| 'explicit_proofs': len([t for t in allowlist['tools'].values() if t.get('lean_definition', True)]), | |
| 'default_deny': len([t for t in allowlist['tools'].values() if t.get('capability_type') == 'default_deny']), | |
| 'sync_status': 'in_sync' if allowlist.get('sync_with_lean') else 'drift_detected' | |
| } | |
| with open('/tmp/drift_report.json', 'w') as f: | |
| json.dump(report, f, indent=2) | |
| print('Drift report:') | |
| print(json.dumps(report, indent=2)) | |
| " | |
| - name: Upload drift report | |
| if: always() | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: allowlist-drift-report | |
| path: /tmp/drift_report.json | |
| - name: Comment on PR | |
| if: github.event_name == 'pull_request' && failure() | |
| # ci-honesty: justified wave7-remediation | |
| continue-on-error: true | |
| uses: actions/github-script@v6 | |
| with: | |
| script: | | |
| github.rest.issues.createComment({ | |
| issue_number: context.issue.number, | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| body: `❌ **Allowlist Sync Validation Failed** | |
| The runtime allowlist is out of sync with Lean proofs. Please run: | |
| \`\`\`bash | |
| python3 tools/gen_allowlist_from_lean.py . runtime/sidecar-watcher/policy/allowlist.json | |
| \`\`\` | |
| Then commit the updated allowlist to ensure runtime configuration matches formal specifications.` | |
| }) |