tomevault-io Lemmafit Post React Audit
Audit: Logic-in-JS-post
Check whether any effect-free logic required for the current build phase is found written directly in JavaScript or TypeScript instead of Dafny.
What to check
- State derivations in React — Any computed value derived from state (filtering, sorting, calculations, conditional logic) that is not exposed through
Api.Presentor a Dafny function. These belong in Dafny. - Validation in JS — Input validation, constraint checks, or boundary enforcement done in React hooks or components instead of Dafny predicates.
- Business rules in event handlers — Pure conditional guards on dispatching (e.g., "only allow X if Y" where Y is derivable from model state) that aren't enforced by Dafny preconditions or exposed as predicates. Exclude effect-gating logic (e.g., "only call Stripe API if active") — that belongs in JS.
- Formatting with logic — Display formatting that encodes business rules (e.g., color based on threshold, status text based on state) rather than pure cosmetic formatting.
- Duplicated logic — Logic that exists in Dafny and is available via API but is re-implemented in JS (even partially), creating a consistency risk.
- Utils with hidden logic — Utility functions in
src/utilsthat contain domain logic rather than pure display helpers.
Severity Labels
Label each finding with one of:
| Severity | Meaning | Action |
|---|---|---|
critical |
Effect-free logic in JS that could produce wrong behavior if it diverges from Dafny, or logic duplicated between JS and Dafny | Must move to Dafny before shipping |
moderate |
Effect-free logic in JS that should be a Dafny function or predicate but isn't yet causing a correctness risk | Should move to Dafny |
minor |
Borderline case where JS logic is arguably pure formatting, or a trivial derivation not worth a Dafny round-trip | Can keep in JS, document why |
Output Format
Present findings as a numbered list with severity tag and file location:
## Logic-in-JS Post-React Audit
1. [critical] src/hooks/useSubscription.ts:42 — computes prorated refund in JS, duplicates Dafny proration logic
2. [moderate] src/components/PlanCard.tsx:18 — derives "canUpgrade" from state fields, should be a Dafny predicate
3. [minor] src/utils/format.ts:10 — date formatting, pure display (OK)
Pass Criteria
The audit passes when there are zero critical and zero moderate findings. If any remain, move the logic to Dafny (back to Step 2), re-verify, then re-run this audit.
Source: midspiral/lemmafit — distributed by TomeVault.