Skip to content

Commit de2bd25

Browse files
hyperpolymathhyperpolymath
committed
merge: resolve conflicts in Agda formalization
2 parents 7fa39cd + 6f6e8d8 commit de2bd25

26 files changed

Lines changed: 1292 additions & 1009 deletions

‎.github/workflows/codeql.yml‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,11 @@ jobs:
2828
fail-fast: false
2929
matrix:
3030
include:
31-
- language: javascript-typescript
31+
# Phronesis is Elixir/Erlang (BEAM) — not a CodeQL-supported source
32+
# language, so `javascript-typescript` made `analyze` exit
33+
# "no source files" on every run. `actions` scans the workflow YAML
34+
# (always present), giving real SAST coverage. (Hypatia: SAST check.)
35+
- language: actions
3236
build-mode: none
3337
steps:
3438
- name: Checkout

‎.github/workflows/conformance.yml‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# conformance.yml — parser conformance gate for the Phronesis grammar.
3+
#
4+
# Runs the real parser (Phronesis.parse/1 = Lexer.tokenize |> Parser.parse) over
5+
# the conformance corpus:
6+
# * conformance/valid/*.phr MUST parse (exit 0)
7+
# * conformance/invalid/*.phr MUST fail (exit non-zero)
8+
# The corpus is the executable contract for spec/grammar.ebnf (v0.2.0). Any drift
9+
# between the parser and the documented grammar turns this gate red.
10+
name: Conformance
11+
12+
on:
13+
push:
14+
branches: [main, master]
15+
pull_request:
16+
workflow_dispatch:
17+
18+
# Estate guardrail: cancel superseded runs (read-only check, safe to cancel).
19+
concurrency:
20+
group: ${{ github.workflow }}-${{ github.ref }}
21+
cancel-in-progress: true
22+
23+
permissions:
24+
contents: read
25+
26+
jobs:
27+
conformance:
28+
name: Grammar conformance (parser vs corpus)
29+
runs-on: ubuntu-latest
30+
timeout-minutes: 15
31+
steps:
32+
- name: Checkout
33+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
34+
35+
# Match the project toolchain (.tool-versions: elixir 1.16.0 / erlang 26.2.1).
36+
# Pinned to the estate-vetted setup-beam SHA already used by hypatia-scan.yml.
37+
- name: Setup Elixir
38+
uses: erlef/setup-beam@fc68ffb90438ef2936bbb3251622353b3dcb2f93 # v1.18.2
39+
with:
40+
elixir-version: '1.16'
41+
otp-version: '26'
42+
43+
- name: Fetch dependencies
44+
run: mix deps.get
45+
46+
# Compile without --warnings-as-errors: the gate measures conformance, not
47+
# lint. A genuine compile break still fails here (mix compile exits non-zero).
48+
- name: Compile
49+
run: mix compile
50+
51+
- name: Run conformance corpus
52+
run: ./conformance/run_conformance.sh

‎.github/workflows/lean.yml‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# lean.yml — build + verify the Phronesis Lean 4 metatheory on every push/PR.
3+
#
4+
# Guards the mechanized proofs against regression. `lake build` typechecks the
5+
# whole development (a broken proof fails the build):
6+
# * type safety — progress / preservation / determinism
7+
# * Sandbox Isolation (safety_proofs.md Theorem 1)
8+
# * Capability Soundness (Theorem 2) + Ethical Verdict Consistency
9+
# * BFT quorum-intersection safety (Theorem 3)
10+
# Core Lean only (no Mathlib): the toolchain pinned in
11+
# academic/formal-verification/lean4/lean-toolchain is all CI needs.
12+
name: Lean Proofs
13+
14+
on:
15+
push:
16+
branches: [main, master]
17+
pull_request:
18+
workflow_dispatch:
19+
20+
# Estate guardrail: cancel superseded runs (read-only check, safe to cancel).
21+
concurrency:
22+
group: ${{ github.workflow }}-${{ github.ref }}
23+
cancel-in-progress: true
24+
25+
permissions:
26+
contents: read
27+
28+
jobs:
29+
lean:
30+
name: Build Lean metatheory (lake build)
31+
runs-on: ubuntu-latest
32+
timeout-minutes: 20
33+
steps:
34+
- name: Checkout
35+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
36+
37+
# Installs elan + the toolchain from lean-toolchain, then runs `lake build`.
38+
# No test/lint targets and no Mathlib in this project, so those are off.
39+
- name: Build + verify Lean proofs
40+
uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
41+
with:
42+
lake-package-directory: academic/formal-verification/lean4
43+
build: "true"
44+
test: "false"
45+
lint: "false"
46+
use-mathlib-cache: "false"

‎.github/workflows/tla-consensus.yml‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# tla-consensus.yml — model-check the Byzantine consensus spec with TLC.
3+
#
4+
# Validates formal/PhronesisConsensus.tla (per-agent commit views, equivocating
5+
# proposer + Byzantine voters). Two gates:
6+
# * positive — at Threshold = 2F+1 all safety invariants hold (TypeOK,
7+
# Agreement, Validity, ByzantineSafety);
8+
# * negative — below the quorum bound (Threshold = 2) TLC MUST report an
9+
# Agreement violation, proving the quorum threshold is load-bearing.
10+
name: TLA+ Consensus
11+
12+
on:
13+
push:
14+
branches: [main, master]
15+
pull_request:
16+
workflow_dispatch:
17+
18+
# Estate guardrail: cancel superseded runs (read-only check, safe to cancel).
19+
concurrency:
20+
group: ${{ github.workflow }}-${{ github.ref }}
21+
cancel-in-progress: true
22+
23+
permissions:
24+
contents: read
25+
26+
jobs:
27+
tlc:
28+
name: TLC model-check (BFT safety)
29+
runs-on: ubuntu-latest
30+
timeout-minutes: 15
31+
steps:
32+
- name: Checkout
33+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
34+
35+
- name: Fetch tla2tools (pinned version + sha256-verified)
36+
run: |
37+
curl -fsSL -o tla2tools.jar \
38+
https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
39+
echo "237332bdcc79a35c7d26efa7b82c77c85c2744591c5598673a8a45085ff2a4fb tla2tools.jar" \
40+
| sha256sum -c -
41+
42+
- name: TLC positive — all safety invariants hold at Threshold = 2F+1
43+
working-directory: formal
44+
run: |
45+
java -XX:+UseParallelGC -cp "${GITHUB_WORKSPACE}/tla2tools.jar" \
46+
tlc2.TLC -config PhronesisConsensus.cfg PhronesisConsensus.tla
47+
48+
- name: TLC negative — Agreement must fail below the quorum bound
49+
working-directory: formal
50+
run: |
51+
if java -cp "${GITHUB_WORKSPACE}/tla2tools.jar" \
52+
tlc2.TLC -config PhronesisConsensus_neg.cfg PhronesisConsensus.tla; then
53+
echo "::error::Agreement held at Threshold < 2F+1 — the quorum bound is not load-bearing (invariant vacuous)."
54+
exit 1
55+
fi
56+
echo "Negative test OK: Agreement correctly violated below the quorum bound."

‎ECOSYSTEM.scm.bak‎

Lines changed: 0 additions & 20 deletions
This file was deleted.

‎META.scm.bak‎

Lines changed: 0 additions & 24 deletions
This file was deleted.

0 commit comments

Comments
 (0)