Skip to content

Commit fc56afa

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Green test suite; harden CI workflows; academic + wiki → AsciiDoc (#53)
* fix: resolve the remaining doc-generator and incremental-lexer test failures - doc_generator: locate declaration line numbers by scanning the source (the AST carries none), so doc comments above CONST/POLICY declarations are found; capture only the contiguous comment block; populate constant examples from the signature; and list constant/policy names in the generated HTML index. - incremental_lexer: snap the re-lex window back to the start of its line, so an edit inside a comment (which yields no token) re-lexes the whole line instead of a mid-line fragment that was misread as identifiers. - fixtures: documented_policy.phr gains a multi-line policy comment and the lower-case "risk threshold" wording the tests assert; sample.phr is rewritten to valid syntax (it previously used unimplemented list-literal syntax). Net: the local ExUnit suite is now fully green (460 tests, 0 failures; 4 skipped ra/consensus tests). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AqMopxUsgu78rg5fhWBUkk * ci: harden secret-scanner and scorecard workflows (Hypatia findings) - secret-scanner: pin trufflesecurity/trufflehog to a release SHA (v3.95.6) and add the missing timeout-minutes to the trufflehog job. - scorecard-enforcer: move the score-gate run step into its own job so the publish job (which holds the OIDC id-token) contains no custom run steps; the SARIF is handed between jobs via an artifact. codeql.yml already uses `language: actions`, so that Hypatia finding is stale; the binary_to_term finding is a false positive (compiler.ex already passes :safe). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AqMopxUsgu78rg5fhWBUkk * docs: convert academic/ and wiki/ corpora to AsciiDoc (CC-BY-SA-4.0) Convert the academic proof corpus (31 files) and the wiki (19 pages) from Markdown to AsciiDoc per the estate "docs must be .adoc" policy, licensed CC-BY-SA-4.0 (via pandoc): - LaTeX math is preserved as [latexmath] blocks; the white-paper sets ":stem: latexmath" so it renders under asciidoctor. - stray in-body "SPDX-License-Identifier: MPL-2.0" lines from the old headers are removed (superseded by the new CC-BY-SA-4.0 header). - intra-wiki cross-links are repointed from .md to .adoc. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AqMopxUsgu78rg5fhWBUkk --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 1f02f3c commit fc56afa

70 files changed

Lines changed: 15563 additions & 12338 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/scorecard-enforcer.yml‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,25 @@ jobs:
3737
uses: github/codeql-action/upload-sarif@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v4
3838
with:
3939
sarif_file: results.sarif
40+
- name: Upload results artifact
41+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
42+
with:
43+
name: scorecard-sarif
44+
path: results.sarif
45+
retention-days: 1
46+
# The score gate runs in a separate job so the publish job (which holds the
47+
# OIDC id-token) contains no custom run steps.
48+
score-gate:
49+
needs: scorecard
50+
runs-on: ubuntu-latest
51+
timeout-minutes: 5
52+
permissions:
53+
contents: read
54+
steps:
55+
- name: Download results artifact
56+
uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
57+
with:
58+
name: scorecard-sarif
4059
- name: Check minimum score
4160
run: |
4261
# Parse score from results

‎.github/workflows/secret-scanner.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,12 @@ jobs:
1616
secrets: inherit
1717
trufflehog:
1818
runs-on: ubuntu-latest
19+
timeout-minutes: 10
1920
steps:
2021
- uses: actions/checkout@692973e3d937129bcbf40652eb9f2f61becf3332
2122
with:
2223
fetch-depth: 0
2324
- name: TruffleHog Secret Scan
24-
uses: trufflesecurity/trufflehog@main
25+
uses: trufflesecurity/trufflehog@30d5bb91af1a771378349dbbb0c82129392acf70 # v3.95.6
2526
with:
2627
extra_args: --only-verified --fail

academic/README.md renamed to academic/README.adoc

Lines changed: 131 additions & 111 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,22 @@
1-
<!--
2-
SPDX-License-Identifier: MPL-2.0
3-
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4-
-->
5-
# Phronesis Academic Documentation
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
4+
== Phronesis Academic Documentation
65

7-
**SPDX-License-Identifier: MPL-2.0
86

97
This directory contains comprehensive academic documentation for Phronesis, including formal proofs, white papers, and mechanized verification. The documentation is designed to withstand rigorous academic scrutiny across multiple fields of mathematics and computer science.
108

11-
---
9+
'''''
1210

13-
## Overview
11+
=== Overview
1412

1513
Phronesis is a formally verified consensus-gated policy language for network configuration. This documentation provides rigorous mathematical foundations suitable for academic peer review, covering 20+ areas of mathematics and computer science.
1614

17-
---
15+
'''''
1816

19-
## Directory Structure
17+
=== Directory Structure
2018

21-
```
19+
....
2220
academic/
2321
├── papers/
2422
│ └── phronesis-white-paper.md # Main academic paper
@@ -113,84 +111,100 @@ academic/
113111
├── notation-guide.md # Unified notation reference
114112
├── theorem-index.md # Cross-referenced theorem index
115113
└── TODO.md # Remaining work items
116-
```
117-
118-
---
119-
120-
## Complete Theorem Coverage
121-
122-
### Foundations (120+ Theorems)
123-
124-
| Area | Key Theorems | Document |
125-
|------|--------------|----------|
126-
| **Type Theory** | Progress, Preservation, Strong Normalization | type-theory-proofs.md |
127-
| **Category Theory** | Functor Laws, Monad Laws, CCC Structure | category-theory-foundations.md |
128-
| **Domain Theory** | CPO Completeness, Scott Continuity, Fixed Points | domain-theory-foundations.md |
129-
| **Order Theory** | Well-Foundedness, WQO Closure, Lattice Properties | order-theory-foundations.md |
130-
| **Set Theory** | ZFC Axioms, Cardinality, Transfinite Induction | set-theoretic-foundations.md |
131-
132-
### Semantics
133-
134-
| Area | Key Theorems | Document |
135-
|------|--------------|----------|
136-
| **Operational** | Determinism, Totality, 45+ Rules | complete-operational-semantics.md |
137-
| **Denotational** | Compositionality, Adequacy, Full Abstraction | denotational-semantics.md |
138-
| **Axiomatic** | Soundness, Completeness, WP Characterization | hoare-logic.md |
139-
| **Algebraic** | Initial Algebra, Catamorphism, Hylomorphism | algebraic-semantics.md |
140-
141-
### Security
142-
143-
| Area | Key Theorems | Document |
144-
|------|--------------|----------|
145-
| **Information Flow** | Noninterference, TINI, Declassification | information-flow-analysis.md |
146-
| **Cryptography** | EUF-CMA, BFT Safety, UC Security | cryptographic-proofs.md |
147-
| **Protocol** | Authentication, Agreement, Replay Prevention | dolev-yao-model.md |
148-
| **Separation Logic** | Frame Rule, Capability Isolation | separation-logic.md |
149-
150-
### Consensus
151-
152-
| Area | Key Theorems | Document |
153-
|------|--------------|----------|
154-
| **Game Theory** | Nash Equilibrium, Incentive Compatibility | consensus-game-theory.md |
155-
| **Temporal Logic** | Safety, Liveness, Fairness | temporal-logic-specifications.md |
156-
| **Concurrency** | Deadlock Freedom, Bisimulation | process-algebra.md |
157-
| **Probability** | Vote Distribution, Tail Bounds | probabilistic-analysis.md |
114+
....
115+
116+
'''''
117+
118+
=== Complete Theorem Coverage
119+
120+
==== Foundations (120+ Theorems)
121+
122+
[cols=",,",options="header",]
123+
|===
124+
|Area |Key Theorems |Document
125+
|*Type Theory* |Progress, Preservation, Strong Normalization |type-theory-proofs.md
126+
|*Category Theory* |Functor Laws, Monad Laws, CCC Structure |category-theory-foundations.md
127+
|*Domain Theory* |CPO Completeness, Scott Continuity, Fixed Points |domain-theory-foundations.md
128+
|*Order Theory* |Well-Foundedness, WQO Closure, Lattice Properties |order-theory-foundations.md
129+
|*Set Theory* |ZFC Axioms, Cardinality, Transfinite Induction |set-theoretic-foundations.md
130+
|===
131+
132+
==== Semantics
133+
134+
[cols=",,",options="header",]
135+
|===
136+
|Area |Key Theorems |Document
137+
|*Operational* |Determinism, Totality, 45+ Rules |complete-operational-semantics.md
138+
|*Denotational* |Compositionality, Adequacy, Full Abstraction |denotational-semantics.md
139+
|*Axiomatic* |Soundness, Completeness, WP Characterization |hoare-logic.md
140+
|*Algebraic* |Initial Algebra, Catamorphism, Hylomorphism |algebraic-semantics.md
141+
|===
142+
143+
==== Security
144+
145+
[cols=",,",options="header",]
146+
|===
147+
|Area |Key Theorems |Document
148+
|*Information Flow* |Noninterference, TINI, Declassification |information-flow-analysis.md
149+
|*Cryptography* |EUF-CMA, BFT Safety, UC Security |cryptographic-proofs.md
150+
|*Protocol* |Authentication, Agreement, Replay Prevention |dolev-yao-model.md
151+
|*Separation Logic* |Frame Rule, Capability Isolation |separation-logic.md
152+
|===
153+
154+
==== Consensus
155+
156+
[cols=",,",options="header",]
157+
|===
158+
|Area |Key Theorems |Document
159+
|*Game Theory* |Nash Equilibrium, Incentive Compatibility |consensus-game-theory.md
160+
|*Temporal Logic* |Safety, Liveness, Fairness |temporal-logic-specifications.md
161+
|*Concurrency* |Deadlock Freedom, Bisimulation |process-algebra.md
162+
|*Probability* |Vote Distribution, Tail Bounds |probabilistic-analysis.md
163+
|===
164+
165+
==== Language Theory
166+
167+
[cols=",,",options="header",]
168+
|===
169+
|Area |Key Theorems |Document
170+
|*Automata* |DFA Recognition, LL(1) Parsing |automata-theory-proofs.md
171+
|*Complexity* |O(n) Parsing, P Membership |computational-complexity-analysis.md
172+
|*Graph Theory* |Valley-Free Routing, Cycle Detection |bgp-graph-theory.md
173+
|===
174+
175+
'''''
176+
177+
=== Formal Verification Status
178+
179+
[cols=",,,,,",options="header",]
180+
|===
181+
|Property |Coq |Lean 4 |Agda |TLA+ |ProVerif
182+
|Type Safety |✓ |✓ |✓ |- |-
183+
|Preservation |✓ |✓ |✓ |- |-
184+
|Determinism |✓ |✓ |✓ |- |-
185+
|Termination |✓ |✓ |✓ |- |-
186+
|Subtyping |✓ |✓ |- |- |-
187+
|Consensus Safety |- |- |- |✓ |-
188+
|Liveness |- |- |- |✓ |-
189+
|Authentication |- |- |- |- |✓
190+
|Noninterference |- |- |- |- |-
191+
|===
192+
193+
*Legend:*
194+
195+
* ✓ = Fully mechanized and verified
196+
* `-` = Not applicable or symbolic proof only
197+
198+
'''''
199+
200+
=== Quick Start
201+
202+
==== View Documentation
158203

159-
### Language Theory
160-
161-
| Area | Key Theorems | Document |
162-
|------|--------------|----------|
163-
| **Automata** | DFA Recognition, LL(1) Parsing | automata-theory-proofs.md |
164-
| **Complexity** | O(n) Parsing, P Membership | computational-complexity-analysis.md |
165-
| **Graph Theory** | Valley-Free Routing, Cycle Detection | bgp-graph-theory.md |
166-
167-
---
168-
169-
## Formal Verification Status
170-
171-
| Property | Coq | Lean 4 | Agda | TLA+ | ProVerif |
172-
|----------|-----|--------|------|------|----------|
173-
| Type Safety | ✓ | ✓ | ✓ | - | - |
174-
| Preservation | ✓ | ✓ | ✓ | - | - |
175-
| Determinism | ✓ | ✓ | ✓ | - | - |
176-
| Termination | ✓ | ✓ | ✓ | - | - |
177-
| Subtyping | ✓ | ✓ | - | - | - |
178-
| Consensus Safety | - | - | - | ✓ | - |
179-
| Liveness | - | - | - | ✓ | - |
180-
| Authentication | - | - | - | - | ✓ |
181-
| Noninterference | - | - | - | - | - |
182-
183-
**Legend:**
184-
- ✓ = Fully mechanized and verified
185-
- `-` = Not applicable or symbolic proof only
186-
187-
---
188-
189-
## Quick Start
190-
191-
### View Documentation
192204
All proofs are in Markdown format for easy reading:
193-
```bash
205+
206+
[source,bash]
207+
----
194208
# Main paper
195209
less academic/papers/phronesis-white-paper.md
196210
@@ -199,55 +213,61 @@ less academic/proofs/type-theory/type-theory-proofs.md
199213
200214
# Theorem index
201215
less academic/theorem-index.md
202-
```
216+
----
203217

204-
### Verify Coq Proofs
205-
```bash
218+
==== Verify Coq Proofs
219+
220+
[source,bash]
221+
----
206222
opam install coq coq-mathcomp
207223
coqc academic/formal-verification/coq/Phronesis.v
208-
```
224+
----
225+
226+
==== Check TLA+ Specification
209227

210-
### Check TLA+ Specification
211-
```bash
228+
[source,bash]
229+
----
212230
tlc formal/PhronesisConsensus.tla
213-
```
231+
----
214232

215-
---
233+
'''''
216234

217-
## Navigation Aids
235+
=== Navigation Aids
218236

219-
- **notation-guide.md**: Comprehensive notation reference across all documents
220-
- **theorem-index.md**: Cross-referenced index of 120+ theorems with dependencies
237+
* *notation-guide.md*: Comprehensive notation reference across all documents
238+
* *theorem-index.md*: Cross-referenced index of 120+ theorems with dependencies
221239

222-
---
240+
'''''
223241

224-
## Citation
242+
=== Citation
225243

226-
```bibtex
244+
[source,bibtex]
245+
----
227246
@techreport{phronesis2025,
228247
title={Phronesis: A Formally Verified Consensus-Gated Policy Language},
229248
author={Phronesis Development Team},
230249
year={2025},
231250
institution={Open Source},
232251
note={Available at https://github.com/hyperpolymath/phronesis}
233252
}
234-
```
253+
----
235254

236-
---
255+
'''''
237256

238-
## Contributing
257+
=== Contributing
239258

240259
Academic contributions are welcome. Please:
241260

242-
1. Follow notation conventions in `notation-guide.md`
243-
2. Include complete proofs with all steps justified
244-
3. Add theorem to `theorem-index.md` with dependencies
245-
4. Provide mechanized proofs where possible
246-
5. Reference existing work appropriately
261+
[arabic]
262+
. Follow notation conventions in `notation-guide.md`
263+
. Include complete proofs with all steps justified
264+
. Add theorem to `theorem-index.md` with dependencies
265+
. Provide mechanized proofs where possible
266+
. Reference existing work appropriately
247267

248-
---
268+
'''''
249269

250-
## License
270+
=== License
251271

252272
All academic documentation is dual-licensed under Apache-2.0 and MIT.
253273
See SPDX headers in individual files.

0 commit comments

Comments
 (0)