chore: preserve in-progress KRL Agda proofs (review before merge)

[hyperpolymath]

What

Preserves uncommitted work-in-progress that was sitting in the krl working
tree from a prior session (mtimes ~yesterday), so it isn't lost when this
ephemeral container is reclaimed. It's a refactor splitting
verification/proofs/agda/Properties.agda into two focused agda --safe
proof modules:

• GeneratorIndex.agda (59 lines) — KRL generator-index validity
• PortArity.agda (230 lines) — KRL port-arity proof
• Properties.agda removed (the refactor's intent)
• .gitignore: added *.agdai so compiled Agda artifacts aren't committed

Important caveats (please review before merging)

• Not authored or verified in this session. I found it untracked/uncommitted
  and preserved it faithfully at your request — I did not write it.
• Not checked to compile. Please confirm agda --safe passes on the new
  modules and that nothing still imports the now-removed Properties.agda
  (deleting it will break the build if other modules reference it).
• The compiled .agdai artifacts were intentionally excluded (now gitignored).

Draft, kept off main until you've reviewed it. If it's stale/unwanted, just
close this and the work is discarded cleanly.

https://claude.ai/code/session_017TXizM5c1Yd9HWf7Y15YH2

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 41 issues detected

Severity	Count
🔴 Critical	4
🟠 High	11
🟡 Medium	26

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
    "type": "codeql_language_matrix_mismatch",
    "file": "codeql.yml",
    "action": "switch_codeql_matrix_to_actions",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Download-and-execute pattern (curl|wget pipe to shell) -- verify integrity before execution (3 occurrences, CWE-494)",
    "type": "shell_download_then_run",
    "file": "/home/runner/work/krl/krl/setup.sh",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "line": 24,
    "reason": "Secret found: Generic API key",
    "type": "secret_detected",
    "file": "/home/runner/work/krl/krl/.envrc",
    "action": "revoke_rotate_and_purge",
    "rule_module": "security_errors",
    "severity": "critical"
  },
  {
    "reason": "Nominal-only SAST in krl: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/krl/krl",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in krl",
    "type": "DependencyPinning",
    "file": "/home/runner/work/krl/krl",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 3 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence