midspiral/lemmafit/lemmafit-post-react-audit

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

1. State derivations in React — Any computed value derived from state (filtering, sorting, calculations, conditional logic) that is not exposed through Api.Present or a Dafny function. These belong in Dafny.
2. Validation in JS — Input validation, constraint checks, or boundary enforcement done in React hooks or components instead of Dafny predicates.
3. 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.
4. 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.
5. Duplicated logic — Logic that exists in Dafny and is available via API but is re-implemented in JS (even partially), creating a consistency risk.
6. Utils with hidden logic — Utility functions in src/utils that contain domain logic rather than pure display helpers.

Severity Labels

Label each finding with one of:

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.