Skip to content

Commit cecc644

Browse files
frawarefraware
authored
Merge pull request #8 from SentinelOps-CI/remediation/audit-hardening
Audit remediation and production hardening
2 parents aeeb5aa + 44a6a78 commit cecc644

64 files changed

Lines changed: 7501 additions & 5464 deletions

Some content is hidden

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

‎.github/dependabot.yml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,3 +16,9 @@ updates:
1616
schedule:
1717
interval: weekly
1818
open-pull-requests-limit: 5
19+
20+
- package-ecosystem: github-actions
21+
directory: "/"
22+
schedule:
23+
interval: weekly
24+
open-pull-requests-limit: 5

‎.github/workflows/codeql.yml‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
name: CodeQL
2+
3+
on:
4+
push:
5+
branches: [main, master]
6+
pull_request:
7+
schedule:
8+
# Weekly Sunday 06:00 UTC
9+
- cron: "0 6 * * 0"
10+
11+
jobs:
12+
analyze:
13+
name: Analyze JavaScript/TypeScript
14+
runs-on: ubuntu-latest
15+
permissions:
16+
actions: read
17+
contents: read
18+
security-events: write
19+
20+
strategy:
21+
fail-fast: false
22+
matrix:
23+
language: [javascript-typescript]
24+
25+
steps:
26+
- name: Checkout
27+
uses: actions/checkout@v4
28+
29+
- name: Initialize CodeQL
30+
uses: github/codeql-action/init@v3
31+
with:
32+
languages: ${{ matrix.language }}
33+
34+
- name: Autobuild
35+
uses: github/codeql-action/autobuild@v3
36+
37+
- name: Perform CodeQL Analysis
38+
uses: github/codeql-action/analyze@v3
39+
with:
40+
category: "/language:${{ matrix.language }}"

‎.github/workflows/lean4-ci.yml‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,15 @@ on:
66
- "specs/**"
77
- "lakefile.lean"
88
- "lean-toolchain"
9+
- "src/lean4-generator.ts"
910
- ".github/workflows/lean4-ci.yml"
1011
push:
1112
branches: [main, master]
1213
paths:
1314
- "specs/**"
1415
- "lakefile.lean"
1516
- "lean-toolchain"
17+
- "src/lean4-generator.ts"
1618

1719
jobs:
1820
lean4-specs:
@@ -31,6 +33,44 @@ jobs:
3133
auto-config: "true"
3234
test: "false"
3335

36+
- name: Report sorry count
37+
env:
38+
# Fail the job only when SPECSYNC_PROOF_GATE=strict (repo variable or secret).
39+
SPECSYNC_PROOF_GATE: ${{ vars.SPECSYNC_PROOF_GATE || 'soft' }}
40+
run: |
41+
set -euo pipefail
42+
if [ ! -d specs ]; then
43+
echo "No specs/ directory — nothing to report"
44+
exit 0
45+
fi
46+
# Count sorry tokens outside comments (block /- -/ and line --).
47+
# Note: avoid embedding nested /- -/ examples inside docs (breaks strip).
48+
TOTAL=$(python3 - <<'PY'
49+
import re, pathlib
50+
text = ""
51+
for p in pathlib.Path("specs").rglob("*.lean"):
52+
text += p.read_text(encoding="utf-8", errors="ignore") + "\n"
53+
# Remove block comments iteratively so nested markers in docs do not leak tokens.
54+
prev = None
55+
while prev != text:
56+
prev = text
57+
text = re.sub(r"/-.*?-/", " ", text, count=1, flags=re.S)
58+
stripped = re.sub(r"--[^\n]*", " ", text)
59+
print(len(re.findall(r"(?:^|[^A-Za-z0-9_])sorry(?=[^A-Za-z0-9_]|$)", stripped)))
60+
PY
61+
)
62+
TOTAL=${TOTAL:-0}
63+
echo "SpecSync Lean sorry count: ${TOTAL}"
64+
echo "sorry_count=${TOTAL}" >> "$GITHUB_STEP_SUMMARY"
65+
echo "### SpecSync Lean \`sorry\` report" >> "$GITHUB_STEP_SUMMARY"
66+
echo "" >> "$GITHUB_STEP_SUMMARY"
67+
echo "Found **${TOTAL}** \`sorry\` occurrence(s) under \`specs/\`." >> "$GITHUB_STEP_SUMMARY"
68+
echo "Gate: \`SPECSYNC_PROOF_GATE=${SPECSYNC_PROOF_GATE}\` (fail only when \`strict\`)." >> "$GITHUB_STEP_SUMMARY"
69+
if [ "$SPECSYNC_PROOF_GATE" = "strict" ] && [ "$TOTAL" -gt 0 ]; then
70+
echo "SPECSYNC_PROOF_GATE=strict and sorry found — failing"
71+
exit 1
72+
fi
73+
3474
- name: Comment on PR with build summary
3575
if: github.event_name == 'pull_request' && success()
3676
uses: actions/github-script@v7

‎.github/workflows/node-ci.yml‎

Lines changed: 51 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,5 +36,54 @@ jobs:
3636
- name: Build
3737
run: npm run build
3838

39-
- name: Test
40-
run: npm test
39+
- name: Test with coverage gate
40+
run: npm run test:coverage
41+
42+
- name: Production dependency audit
43+
run: npm audit --omit=dev --audit-level=high
44+
45+
docker-smoke:
46+
runs-on: ubuntu-latest
47+
permissions:
48+
contents: read
49+
50+
steps:
51+
- name: Checkout
52+
uses: actions/checkout@v4
53+
54+
- name: Build Docker image
55+
run: docker build -t specsync:ci .
56+
57+
- name: Smoke — image has compiled entrypoint
58+
run: |
59+
docker run --rm --entrypoint node specsync:ci -e "require('fs').accessSync('dist/index.js')"
60+
61+
vscode-extension:
62+
runs-on: ubuntu-latest
63+
permissions:
64+
contents: read
65+
defaults:
66+
run:
67+
working-directory: vscode-extension
68+
69+
steps:
70+
- name: Checkout
71+
uses: actions/checkout@v4
72+
73+
- name: Setup Node.js
74+
uses: actions/setup-node@v4
75+
with:
76+
node-version: "22"
77+
cache: npm
78+
cache-dependency-path: vscode-extension/package-lock.json
79+
80+
- name: Install extension deps
81+
run: |
82+
if [ -f package-lock.json ]; then
83+
npm ci
84+
else
85+
npm install
86+
fi
87+
88+
- name: Compile extension
89+
run: npm run compile

‎README.md‎

Lines changed: 67 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414

1515
**Formal specs, meet your pull requests.**
1616

17-
A GitHub App that turns diffs into structured specification suggestions—powered by LLMs, grounded in AST analysis, and wired for Lean 4 when you want proofs to compile.
17+
A GitHub App that turns PR diffs into structured specification suggestions—powered by LLMs when configured, grounded in tree-sitter AST analysis, and able to write Lean 4 **spec-as-contract** modules under `.specsync/` (opaque stubs + closed proofs where possible; labeled unfinished goals otherwise — not claimed complete).
1818

1919
[![License: MIT](https://img.shields.io/badge/License-MIT-blue.svg)](LICENSE)
2020
[![TypeScript](https://img.shields.io/badge/TypeScript-5.x-3178c6?logo=typescript&logoColor=white)](https://www.typescriptlang.org/)
@@ -29,60 +29,65 @@ A GitHub App that turns diffs into structured specification suggestions—powere
2929

3030
## What it does
3131

32-
| Capability | Description |
33-
| ------------------------ | ------------------------------------------------------------------------------------------------ |
34-
| **Event-driven** | Listens on GitHub for pull requests, pushes, and comments—then runs the analysis pipeline. |
35-
| **Multi-language diffs** | Parses changes across common languages using Tree-sitter–backed extraction. |
36-
| **LLM-assisted specs** | Proposes preconditions, postconditions, invariants, and rationale where API keys are configured. |
37-
| **Lean-ready output** | Generated modules can target your Lake `specs/` tree so `lake build` stays honest. |
38-
| **Operator-friendly** | Health and readiness routes on the Probot router, Docker image, and CI for Node + Lean. |
32+
| Capability | Description |
33+
| --- | --- |
34+
| **Async PR analysis** | Webhooks enqueue work on an in-process `AnalysisJobQueue` (idempotent per PR head SHA) so GitHub gets a fast ack. Optional `SPECSYNC_JOB_MARKERS_DIR` shares completion markers across instances on a volume (not committed to the target repo). |
35+
| **Multi-language diffs** | Tree-sitter AST for JavaScript, TypeScript, Python, Java, and Rust (no Go/C/C++ parsers). Review comments use `RIGHT` for adds/modifies and `LEFT` for pure deletions. |
36+
| **LLM-assisted specs** | Proposes preconditions, postconditions, invariants, and rationale when API keys are set. Production denies silent mock output unless `SPECSYNC_ALLOW_MOCK_LLM=true`. |
37+
| **`.specsync/` store** | `/specsync accept` commits JSON contracts (and Lean stubs) under `.specsync/` on the PR branch. Mutating commands require write AuthZ and are rate-limited per actor/PR. |
38+
| **Soft proof gate** | Default `SPECSYNC_PROOF_GATE=soft`: Lean CI **reports** `sorry` count (comments stripped). Set `strict` to **fail** on any remaining `sorry` in `specs/`. Closed fragments use real proofs (`trivial`, `Nat.zero_le`); unfinished LLM obligations stay labeled — this is not end-to-end formal verification. |
39+
| **Drift on push** | Compares changed functions against accepted `.specsync/` specs on main/master pushes. |
40+
| **Operator-friendly** | `GET /health`, `GET /ready` (includes job + metrics counters), optional secret-gated dashboard (loopback by default), Docker image, Node + Lean + CodeQL + VS Code extension CI. |
3941

40-
The optional [VS Code extension](vscode-extension/) adds editor-side commands and local proof hooks; the server-side app lives in this repository’s `src/` tree.
42+
The optional [VS Code extension](vscode-extension/) reads the same `.specsync/` store; compile it with `npm run compile` in that folder.
4143

4244
---
4345

4446
## Architecture
4547

46-
At a glance: GitHub sends webhooks to **Probot**; the app parses diffs, walks ASTs, asks the **spec analyzer** (and **LLM client** when configured), then posts back via the **GitHub UI** layer. Lean artifacts and CI are first-class paths, not an afterthought.
48+
GitHub webhooks hit **Probot**; handlers enqueue analysis, then the worker parses diffs, walks ASTs, calls the **spec analyzer** / **LLM client**, and posts review comments plus coverage checks. Accepted specs live under **`.specsync/`**; Lake-built Lean sources for this repo also live under [`specs/`](specs/).
4749

4850
```mermaid
4951
flowchart TB
5052
subgraph ingest [GitHub]
5153
E[Webhooks]
5254
end
5355
subgraph pipeline [Analysis]
56+
Q[AnalysisJobQueue]
5457
D[Diff parser]
5558
T[AST extractor]
5659
N[Spec analyzer]
5760
L[LLM client]
5861
end
5962
subgraph surface [Surfaces]
6063
G[PR comments and checks]
61-
K[Lean specs under specs/]
62-
S[Slack and dashboards]
64+
S[".specsync/ store"]
65+
K[Lean stubs / Lake specs]
6366
end
64-
E --> D --> T --> N
67+
E --> Q --> D --> T --> N
6568
N --> L
6669
N --> G
67-
N --> K
68-
N --> S
70+
G --> S
71+
S --> K
6972
```
7073

71-
Formal modules consumed by Lake live under [`specs/`](specs/), with [`lakefile.lean`](lakefile.lean) and [`lean-toolchain`](lean-toolchain) pinning the toolchain.
74+
Formal modules consumed by Lake live under [`specs/`](specs/), with [`lakefile.lean`](lakefile.lean) and [`lean-toolchain`](lean-toolchain) pinning the toolchain. Generated accept-path Lean may also land under `.specsync/lean/` depending on configuration.
7275

7376
---
7477

7578
## Repository layout
7679

77-
| Location | Role |
78-
| ------------------------------------------ | -------------------------------------------------------------------------------- |
79-
| [`src/index.ts`](src/index.ts) | Probot entry: webhooks, `GET /health`, `GET /ready` when the router is available |
80-
| [`src/`](src/) | Application modules—parser, analyzer, GitHub UI, LLM client, generators |
81-
| [`dist/`](dist/) | Build output from `npm run build` (generated, not committed) |
82-
| [`specs/`](specs/) | Lean 4 sources for `lake build` |
83-
| [`test/`](test/) | Jest tests (`*.test.ts`) |
84-
| [`vscode-extension/`](vscode-extension/) | Editor extension (TypeScript → `out/`) |
85-
| [`.github/workflows/`](.github/workflows/) | Continuous integration |
80+
| Location | Role |
81+
| --- | --- |
82+
| [`src/index.ts`](src/index.ts) | Probot entry: webhooks, queue, `GET /health`, `GET /ready` |
83+
| [`src/analysis-queue.ts`](src/analysis-queue.ts) | In-process async job runner with idempotency |
84+
| [`src/spec-store.ts`](src/spec-store.ts) | `.specsync/` read/write helpers |
85+
| [`src/`](src/) | Parser, analyzer, GitHub UI, LLM client, generators, metrics |
86+
| [`dist/`](dist/) | Build output from `npm run build` (generated, not committed) |
87+
| [`specs/`](specs/) | Lean 4 sources for `lake build` |
88+
| [`test/`](test/) | Jest tests (`*.test.ts`) |
89+
| [`vscode-extension/`](vscode-extension/) | Editor extension (`npm run compile`) |
90+
| [`.github/workflows/`](.github/workflows/) | Node CI, Lean CI, CodeQL |
8691

8792
---
8893

@@ -126,35 +131,24 @@ Optional but common:
126131
```env
127132
OPENAI_API_KEY=...
128133
ANTHROPIC_API_KEY=...
129-
GITHUB_TOKEN=...
134+
GITHUB_TOKEN=... # CLI/demo only; PR path uses installation octokit
130135
SPECS_DIR=specs
131136
PORT=3000
137+
SPECSYNC_ALLOW_MOCK_LLM=false
138+
SPECSYNC_PROOF_GATE=soft
139+
SPECSYNC_MAX_SPECS_PER_PR=10
140+
SPECSYNC_JOB_MARKERS_DIR= # optional shared FS for multi-instance job idempotency
141+
SPECSYNC_COMMAND_RATE_LIMIT=10
142+
SPECSYNC_COMMAND_RATE_WINDOW_MS=60000
143+
SPECSYNC_DASHBOARD=0
144+
SPECSYNC_DASHBOARD_SECRET=
132145
```
133146

147+
See [`env.example`](env.example) and [`app.yml`](app.yml) for the full App permission set (`checks: write`, `contents: write` for accept commits, etc.).
148+
134149
### GitHub App manifest (reference)
135150

136-
Use this shape when registering the app; point the webhook URL at your deployed Probot instance.
137-
138-
```yaml
139-
name: SpecSync
140-
description: GitHub-native specification assistant
141-
url: https://github.com/your-org/specsync
142-
hook_attributes:
143-
url: https://your-domain.com/webhook
144-
content_type: json
145-
default_permissions:
146-
contents: read
147-
pull_requests: write
148-
issues: write
149-
metadata: read
150-
default_events:
151-
- pull_request
152-
- push
153-
- issues
154-
- issue_comment
155-
- pull_request_review
156-
- pull_request_review_comment
157-
```
151+
Use [`app.yml`](app.yml) when registering the app; point the webhook URL at your deployed Probot instance. Replace org/domain placeholders with your deployment.
158152

159153
---
160154

@@ -180,28 +174,35 @@ default_events:
180174
When the Probot server exposes a router, the app registers:
181175

182176
- `GET /health` — liveness
183-
- `GET /ready` — readiness (extend when you add databases or queues)
177+
- `GET /ready` — readiness, including analysis-queue stats and in-process metrics counters
184178

185179
The [`Dockerfile`](Dockerfile) healthcheck expects `GET /health` on the process port (default `3000`).
186180

187181
---
188182

189183
## Lean and Lake
190184

191-
- **CI:** [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) runs `lake build` via [lean-action](https://github.com/leanprover/lean-action) when Lean-related paths change.
192-
- **Local:** From the repo root, `lake build` after installing Elan/Lean.
193-
- **Generator contract:** Output from [`src/lean4-generator.ts`](src/lean4-generator.ts) should respect `SPECS_DIR` (default `specs`) so files sit in the same Lake library as [`lakefile.lean`](lakefile.lean).
185+
- **CI:** [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) runs `lake build` via [lean-action](https://github.com/leanprover/lean-action) when Lean-related paths or `src/lean4-generator.ts` change.
186+
- **Local:** From the repo root, `lake build` after installing Elan/Lean (see `lean-toolchain`).
187+
- **Committed baseline:** [`specs/Specs.lean`](specs/Specs.lean) + [`specs/Specs/ClosedNatContract.lean`](specs/Specs/ClosedNatContract.lean) are Std-only and **contain zero `sorry`** (opaque + closed proofs).
188+
- **Generator contract:** [`src/lean4-generator.ts`](src/lean4-generator.ts) emits Std-only Lake modules:
189+
- Function under contract → `opaque` (no unfinished proof for missing bodies)
190+
- Smoke / Nat nonneg / other decidable fragments → real proofs (`trivial`, `Nat.zero_le`, …)
191+
- Undecided LLM postconditions → `/- SpecSync: unproved: <reason> -/` + `sorry` only
192+
- **Proof gate:** `SPECSYNC_PROOF_GATE=soft` (default) reports counts; `strict` fails if any `sorry` remains. SpecSync does **not** claim completed formal verification while open obligations exist.
193+
- **Accept path:** Artifacts for target repos are stored under `.specsync/` (separate from this repo’s `specs/` library).
194194

195195
---
196196

197197
## Continuous integration
198198

199-
| Workflow | Purpose |
200-
| ------------------------------------------------ | ------------------------------------------ |
201-
| [`node-ci.yml`](.github/workflows/node-ci.yml) | Lint, format check, typecheck, build, test |
202-
| [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) | `lake build` for Lean specs |
199+
| Workflow | Purpose |
200+
| --- | --- |
201+
| [`node-ci.yml`](.github/workflows/node-ci.yml) | Lint, format, typecheck, build, coverage tests, `npm audit --production`, Docker smoke, vscode-extension `compile` |
202+
| [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) | `lake build` for Lean specs |
203+
| [`codeql.yml`](.github/workflows/codeql.yml) | CodeQL analysis for JavaScript/TypeScript |
203204

204-
[`dependabot.yml`](.github/dependabot.yml) schedules weekly npm updates for the root package and [`vscode-extension/`](vscode-extension/).
205+
[`dependabot.yml`](.github/dependabot.yml) schedules weekly npm and GitHub Actions updates.
205206

206207
---
207208

@@ -217,10 +218,12 @@ docker run -p 3000:3000 \
217218
-e APP_ID=<id> \
218219
-e PRIVATE_KEY=<pem-or-base64> \
219220
-e WEBHOOK_SECRET=<secret> \
221+
-e NODE_ENV=production \
222+
-e SPECSYNC_ALLOW_MOCK_LLM=false \
220223
specsync
221224
```
222225

223-
Add LLM keys the same way if you use live models in production.
226+
Add LLM keys the same way if you use live models in production. Without keys (and without `SPECSYNC_ALLOW_MOCK_LLM=true`), the app posts an LLM-unavailable notice instead of fake specs.
224227

225228
### Other platforms
226229

@@ -230,17 +233,18 @@ Any environment that provides Node, `PORT`, Probot env vars, and a **public HTTP
230233

231234
## Usage notes
232235

236+
- **Accept / ignore / edit:** Comment `/specsync accept` (or ignore/edit) on a suggestion; AuthZ requires a collaborator (or stronger) or PR committer. Accept writes `.specsync/specs/` + Lean stubs on the PR branch.
233237
- **Demos:** After `npm run build`, run `npm run demo` or `npm run ui-demo`.
234-
- **VS Code:** See [`vscode-extension/README.md`](vscode-extension/README.md) for building the extension (`npx tsc -p .` inside that folder).
235-
- **Lean:** Modules under `specs/` should pass `lake build`; proof sketches may use `sorry` until completed.
238+
- **VS Code:** See [`vscode-extension/README.md`](vscode-extension/README.md); CI runs `npm run compile` in that package.
239+
- **Lean:** Committed modules under `specs/` pass `lake build` with zero `sorry`. Accept-path sketches may still use labeled unfinished proofs until a human (or stronger autoformalization) closes them.
236240

237241
---
238242

239243
## Quality and security
240244

241-
- Pull requests run lint, format, typecheck, build, and tests; Lean CI validates the Lake project.
242-
- Prefer Dependabot PRs and periodic `npm audit` before releases.
243-
- Probot uses structured logging; see [`src/health.ts`](src/health.ts) for optional standalone health HTTP.
245+
- PRs run lint, format, typecheck, build, coverage-gated tests, production `npm audit`, Docker image smoke, and extension compile; CodeQL runs on push/PR/schedule.
246+
- Structured logs (Probot `context.log` / shared pino) include job id, PR, latency, and LLM mock|live soft-cost fields where available.
247+
- Prefer Dependabot PRs; treat audit failures as blocking unless an exception is documented in the workflow.
244248

245249
---
246250

0 commit comments

Comments
 (0)