Skip to content

README_LemmaScript.md

Latest commit

 

History

History
111 lines (84 loc) · 5.54 KB

README_LemmaScript.md

File metadata and controls

111 lines (84 loc) · 5.54 KB
Raw

github-star-checker — Verified with LemmaScript

LemmaScript verified

A CLI that polls GitHub star counts and reports per-run deltas, with the diff arithmetic and its sign-classified decomposition verified in Dafny via LemmaScript. The TypeScript in src/domain.ts is the source of truth; the .dfy files are a verification side-car.

The verified core

Layered from primitive to high-level, all in src/domain.ts:

Pure recursive helpers (emit as Dafny functions):

  • sumDiffs(rows) — tail-recursive sum over DiffRow[].
  • sumDiffsUpTo(rows, n) — prefix-indexed sum, bridges to the upTo partition family.
  • sumPositiveUpTo(rows, n) / sumNegativeUpTo(rows, n) — signed partial sums.
  • countPositiveUpTo / countNegativeUpTo / countZeroUpTo — signed partial counts.

Core method computeDiff(repos, oldCounts, newCounts) — builds the per-repo diff report. A single //@ assert repo in newCounts bridges from the universal requires to the concrete narrowing at the access site.

Sign-classified extractors:

  • extractIncreases(report) — rows with diff > 0.
  • extractDecreases(report) — rows with diff < 0.
  • extractUnchanged(report) — rows with diff === 0.

Each carries six theorems (see "What's verified"). extractIncreases is what the watch-mode notification uses — "foo/bar +1, baz/qux +3" is the verified prefix of gainers in input order.

Conservation theorem decompose(report) — returns { increases, decreases, same } and, by invoking the partition lemmas in its body, proves that the three splits partition the report without loss.

What's verified

computeDiff (6 ensures):

  • Row count matches input repo count.
  • Each row's repo, newCount, oldCount, diff are correct per the inputs.
  • totalDiff === sumDiffs(rows) (non-trivial inductive step via SumDiffs_append).

Each extractor (6 ensures × 3 extractors):

  • Length bound |res| ≤ |rows|.
  • Count equality |res| === countXUpTo(rows, |rows|).
  • Sum equality sumDiffs(res) === sumXUpTo(rows, |rows|) (for ±; unchanged's sum is 0 by soundness).
  • Soundness every output row has the expected sign.
  • Completeness every input row with the expected sign appears in the output.
  • Ordered completeness same-sign rows appear in the output in the same order they were listed on the command line — pairs k1 < k2 with matching signs witness ordered j1 < j2 in the output.

decompose (conservation, 3 ensures):

  • |increases| + |decreases| + |same| === |report.rows| — every row in exactly one class.
  • sumDiffs(increases) + sumDiffs(decreases) === report.totalDiff — the non-trivial sums account for the whole delta (the zero sum for same follows by soundness).

33 Dafny verification conditions, 0 errors.

File structure

src/
  domain.ts         annotated TS — source of truth
  domain.dfy.gen    generated by `lsc gen --backend=dafny`
  domain.dfy        .dfy.gen + proof additions
  cli.ts            trusted boundary (fetch, state, output, notification)
bin/
  stars             shell entry — `stars owner/repo [...]`

Proof additions (in src/domain.dfy)

On top of the generated .dfy.gen, the following are hand-written:

  1. SumDiffs_append lemma — sumDiffs(rows + [row]) === sumDiffs(rows) + row.diff, by induction on |rows|. Used by computeDiff's loop body and in each extractor's per-iteration step to carry the sumDiffs(out) === sumXUpTo invariant.
  2. Partition lemmas:
    • CountPartitionUpTo(rows, n) — positive + negative + zero counts equal n. Induction on n.
    • SumPartitionUpTo(rows, n) — positive + negative sums equal sumDiffsUpTo. Induction on n.
  3. Bridge lemmas:
    • SumDiffs_eq_UpTo(rows) — sumDiffs(rows) === sumDiffsUpTo(rows, |rows|). Induction on |rows|, via…
    • SumDiffsUpTo_shift(rows) — sumDiffsUpTo(rows, |rows|) === rows[0].diff + sumDiffsUpTo(rows[1..], |rows| - 1). The head/tail equivalence used to close the induction. Via…
    • SumDiffsUpTo_prefix_agrees(rs, rt, n) — the technical helper showing that sumDiffsUpTo only inspects a prefix and agrees across a shift.
  4. Witness hints in each extractor's loop body: ghost var out_old := out snapshot, plus asserts that out[|out_old|] matches the appended row (Some-branch) and that the prefix is preserved across append (both branches). The same pattern carries the plain-completeness, ordered-completeness, sum-equality, and count-equality invariants.
  5. Proof lemma calls in decompose's body: CountPartitionUpTo, SumPartitionUpTo, SumDiffs_eq_UpTo invoked in sequence so Dafny can combine the extractors' upTo-indexed ensures into the top-level conservation claims.

Setup

Prerequisites: Node.js ≥ 18, Dafny ≥ 4.x. Assumes LemmaScript is cloned as a sibling (../LemmaScript).

cd ../LemmaScript/tools && npm install
cd -                     && npm install

Usage

npm run stars -- owner/repo1 owner/repo2 ...
npm run stars -- --watch --every 10 owner/repo1 ...

npm link once and stars is on PATH.

Verification

npm run check      # lsc check --backend=dafny src/domain.ts
npm run gen        # regen domain.dfy.gen
npm run regen      # three-way merge .dfy with new .dfy.gen