Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
0514e09
proof(coq): Phase 1 β€” cfg-remember + atomic-axiom tactic on Lemma B (…
claude May 24, 2026
7acf1e5
proof(coq): add subst_preserves_typing_strong (unlocks Cluster A of L…
claude May 24, 2026
96efe22
proof(coq): Qed output_ctx_det β€” output-context determinacy for has_type
claude May 24, 2026
d97ba32
proof(coq): Lemma B β€” close 3 Cluster A cases (S_Let_Val, S_LetLin_Va…
claude May 24, 2026
9a03df6
proof(coq): Lemma B β€” close all 7 Cluster A cases (S_If_True/False, S…
claude May 24, 2026
d4161b6
proof(coq): Lemma B β€” close 4 Cluster C cases (S_Fst, S_Snd, S_Copy, …
claude May 24, 2026
68712fc
proof(coq): Lemma B β€” close 10 Cluster B congruence cases (35->11, 69%)
claude May 24, 2026
a2e8bcf
proof(coq): close S_App_Step1, S_App_Step2 via sibling type_determina…
claude May 24, 2026
ad5f299
proof(coq): Lemma B β€” Cluster C complete (S_StringLen atomic, S_Regio…
claude May 24, 2026
cf058e3
proof(coq): introduce step_preserves_type sub-lemma (partial; ~15 of …
claude May 24, 2026
f499c82
proof(coq): step_preserves_type clone-out β€” 8 more cases (12 of 35 re…
claude May 24, 2026
eed4901
proof(coq): step_preserves_type β€” close 4 cases fully, structure rema…
claude May 24, 2026
50ce303
proof(coq): step_preserves_type β€” add step_R_change_shape, close MIDD…
claude May 24, 2026
caa424c
proof(coq): step_preserves_type β€” close 7 RIGHT sub-cases via members…
claude May 24, 2026
0c64b9e
proof(coq): close 13 of 14 admits in step_output_context_eq (Lemma B)
claude May 24, 2026
0713ff6
proof(coq): add has_type_lift_across_step_no_shrink helper + extend S…
claude May 24, 2026
a4870d7
proof(coq): add safe_for_step precondition definition for preservatio…
claude May 25, 2026
2eac3e8
proof(coq): preservation path 2 β€” close 11 of 12 congruence cases via…
claude May 25, 2026
6724f37
proof(coq): preservation S_Region_Step β€” close 3 of 4 sub-cases via s…
claude May 25, 2026
379c73d
chore: gitignore Claude Code agent worktrees
claude May 25, 2026
5d13815
Merge remote-tracking branch 'origin/main' into claude/adoring-gates-…
hyperpolymath May 25, 2026
51d4376
Merge branch 'claude/adoring-gates-E57WG' of github.com:hyperpolymath…
hyperpolymath May 25, 2026
520afde
chore(repo): major tidy β€” purge cache cruft, consolidate docs
claude May 25, 2026
93f165c
chore(repo): tidy β€” move aqueduct example + add KNOWN-PROOF-DEBT
claude May 25, 2026
1bbd507
docs: add docs/README.md + spec/README.md navigation hubs
claude May 25, 2026
d161c31
fix(coq): close preservation proof holes for Hypatia
hyperpolymath May 25, 2026
d89bc97
Merge branch 'claude/adoring-gates-E57WG' of github.com:hyperpolymath…
hyperpolymath May 25, 2026
a189df3
fix(ci): stop Hypatia code-scanning self-reports
hyperpolymath May 25, 2026
3f10d1b
ci: adopt standards reusable workflows for Scorecard, Hypatia, and Go…
hyperpolymath Jun 21, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
13 changes: 2 additions & 11 deletions .github/workflows/governance.yml
Original file line number Diff line number Diff line change
@@ -1,25 +1,16 @@
# SPDX-License-Identifier: PMPL-1.0-or-later
# governance.yml β€” single wrapper calling the shared estate governance bundle
# in hyperpolymath/standards instead of carrying per-repo copies.
#
# Replaces the per-repo governance scaffolding removed in this PR:
# quality.yml, guix-nix-policy.yml, npm-bun-blocker.yml, ts-blocker.yml,
# security-policy.yml, rsr-antipattern.yml, wellknown-enforcement.yml,
# workflow-linter.yml
#
# Load-bearing build/security workflows stay standalone in the repo.

name: Governance

on:
push:
branches: [main, master]
pull_request:
branches: [main, master]
workflow_dispatch:

permissions:
contents: read

jobs:
governance:
uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@main
uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910
405 changes: 5 additions & 400 deletions .github/workflows/hypatia-scan.yml

Large diffs are not rendered by default.

81 changes: 0 additions & 81 deletions .github/workflows/scorecard-enforcer.yml

This file was deleted.

31 changes: 3 additions & 28 deletions .github/workflows/scorecard.yml
Original file line number Diff line number Diff line change
@@ -1,41 +1,16 @@
# SPDX-License-Identifier: PMPL-1.0-or-later
name: OSSF Scorecard

on:
push:
branches: [main, master]
schedule:
- cron: '0 4 * * *'
workflow_dispatch:

# Estate guardrail: cancel superseded runs so re-pushes / rebased PR
# updates do not pile up queued runs against the shared account-wide
# Actions concurrency pool. Applied only to read-only check workflows
# (no publish/mutation), so cancelling a superseded run is always safe.
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

permissions:
contents: read

jobs:
analysis:
runs-on: ubuntu-latest
permissions:
security-events: write
id-token: write
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
with:
persist-credentials: false

- name: Run Scorecard
uses: ossf/scorecard-action@4eaacf0543bb3f2c246792bd56e8cdeffafb205a # v2.4.3
with:
results_file: results.sarif
results_format: sarif

- name: Upload results
uses: github/codeql-action/upload-sarif@7211b7c8077ea37d8641b6271f6a365a22a5fbfa # v3.31.8
with:
sarif_file: results.sarif
scorecard:
uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
# SPDX-License-Identifier: PMPL-1.0-or-later
# RSR-compliant .gitignore

# Claude Code agent worktrees
.claude/

# OS & Editor
.DS_Store
Thumbs.db
Expand All @@ -22,6 +25,7 @@ build/
# Zig
**/zig-out/
**/.zig-cache/
.zig-cache-global/

# Coq / Rocq
*.vo
Expand Down
120 changes: 0 additions & 120 deletions .zig-cache-global/b/87f6089f6466e02607681b715c77e280/builtin.zig

This file was deleted.

Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/205970867f39f5e5eaa06dc60ce61ffd
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/226445d6846e2509d709748ec699253e
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/422683bdefe36c03c75b326af16d024b
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/6689af5bc4ad9464a0ca5c2b641e27c6
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/8563f6b2d2a8e27f70b6192d74834b30
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/8d6d93449dea8f76ac42bec4eb09ca17
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/a621e75b6a08de285c4b694a92a295a7
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/b9773d45ef33cae10e9caa6d52f4e86b
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file removed .zig-cache-global/z/bc72cf5b705498c1c0900f3970bc262c
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Loading