Hito architecture

Hito is a training tracker for Mike Mentzer's Heavy Duty. This document derives the code from the doctrine, in that order: what the source claims, what those claims force to be true of a program, and how the code carries them.

The source is /Heavy Duty I/ (HD1), in doc/. It is copyrighted reference material, gitignored, never committed.

Premise

Mentzer's central methodological claim is that training must be derived from principles rather than copied from champions. A tracker that merely stores numbers abandons that claim: it would record an overtrained, under-recovered, volume-inflated program as happily as a correct one.

So the program's job is not to hold data. It is to make the doctrine *structural* — to arrange types so that a training state the book forbids is difficult to represent and impossible to represent silently.

Two rules follow, and they govern every decision below.

1. Where a design choice conflicts with the doctrine, the doctrine wins, or the conflict is recorded explicitly (see Tensions with the source).
2. Where a deviation must be *possible* — a trainee really did train early, or really did perform an extra set — it must never be *silent*. It is represented, acknowledged, and retained.

First principles

Six commitments. Each is a claim from HD1; each has a consequence the code is built to satisfy.

Intensity is categorical, not scalar

A working set is carried to momentary muscular failure. HD1 argues there are only two accurate measures of intensity: 0% at rest and 100% at failure.

/Consequence./ Reaching failure is an invariant of the recorded type, not a field to be filled in. What varies is load, the reps it happened to yield, and whether anything carried the effort *past* failure — which is qualitative, not more of the same: Beyond_failure of forced reps, negatives, rest-pause, or a static hold. There is no numeric intensity score anywhere, and there never should be.

The stimulus is the unit of work

HD1 prescribes one drive per exercise. "Superset" in the book *means* pre-exhaustion: an isolation movement into a compound sharing its target, with no pause.

/Consequence./ There is no set count in the model, on either side of the plan/record divide. Volume is not a number a caller supplies; it is the length of a list. A prescription therefore cannot ask for more work than one drive per slot, because there is no field in which to say so. Delivery is Single or Pre_exhaust, and nothing else.

Recovery precedes growth

Training stimulates growth; recovery produces it. Training before reserves are replenished is HD1's primary error, and its effect is systemic rather than local.

/Consequence./ Beginning a workout demands an unforgeable permission: Recovery.clearance. It cannot be constructed by a caller who feels ready. It is either earned — clear returns Some only when recovery is complete — or taken deliberately through override, which records how long you had actually rested against what was recommended. The override is not an escape hatch; it is evidence, and it is what allows a later stall to be attributed to training under-recovered.

Progress is the signal, and it is overload

Progress is an increase in reps, weight, or both. One extra rep counts.

/Consequence./ Reps are an *outcome*, never a target: a set ends at failure, not at a number. A prescribed range only calibrates load. When twelve reps are reached the load rises by 10–20%, so failure returns inside the band. Judgment returns a verdict type — Hold, Increase of a window, Too_heavy — rather than a bare number a caller might round into nonsense.

On a stall, the answer is never more work

HD1's remedy for stalled progress subtracts: a week off, then less volume and less frequency.

/Consequence./ The remedy is a type with a single constructor, Lay_off_then_reduce, carrying a lay-off, stimuli to drop per workout, and extra rest. There is no additive remedy to choose by mistake, because none exists to name. Rising volume is a diagnostic warning, never an achievement.

The record states facts; one module judges them

Progress is knowable only from what was performed. A log that argues with history is useless.

/Consequence./ Evidence records and never interprets. Progression is the only judge, and it may decline: Insufficient_data rather than a guess, so two flat sessions a day apart never condemn a routine. Invariants belong on plans, which are *authored*; not on history, which is *observed*.

What the principles force on the structure

The model is split by what a module *claims*, not by convenient nouns:

| Claim | Module | Answers | |-------------+----------------+--------------------------------| | vocabulary | Exercise | what movements exist, and pair | | normative | Prescription | what should be done | | factual | Evidence | what was done | | inferential | Progression | what that means |

Recovery straddles the divide deliberately: it measures a fact (elapsed rest) and issues a normative artifact (a clearance). That is the one place the two kinds of claim legitimately meet, which is why permission to train lives there and nowhere else.

There is no Principle module. A module cohering around "things that are true" is a constants bag; a principle stated in one place is a principle that can be ignored at every call site. Each is instead enforced where it bites:

| Principle | Enforced at | Mechanism | |-----------------------------------------------+---------------------------------------+-----------| | one drive to failure per slot | shape of Prescription.Stimulus | absence | | a recorded effort reached failure | Evidence.Stimulus.outcome | type | | training requires recovery or acknowledgement | Evidence.Workout.start | type | | a stall is never answered with work | Progression.remedy return type | type | | a correction is not extra volume | Evidence.Workout.replace_stimulus | type | | 6–12 calibration window | Prescription.Rep_range.limits | runtime | | isolation into compound, sharing a target | Exercise.may_pre_exhaust | runtime | | substitutions come from author lists | Exercise.may_substitute | runtime | | 48h between workouts, 72h after the cycle | Prescription.Routine.recovery_after | value | | load rises at twelve reps, by 10–20% | Progression.judge_load | value |

The bias is intentional: a principle carried by a type cannot be forgotten, and the runtime checks are confined to *authoring* — building a prescription, pairing two movements — where a violation is a programming error and raising is correct.

Layers

Three libraries. Dependencies point inward only.

hito.web    Dream · dream-html · js_of_ocaml client
   |            HTTP, HTML, sessions, CSRF, wall-clock time
   v
hito.app    Trainee · Repository (port) · Service · Catalog · Codec
   |            identity, persistence, recovery policy, Lwt
   v
hito.core   Exercise · Recovery · Prescription · Evidence · Progression
                pure domain: no framework, no database, no serialization

The core is five modules, unwrapped (wrapped false), so they are referred to bare: Prescription.Stimulus, Evidence.Workout, Evidence.Log. It has no dependency on Lwt, Caqti, Dream, or any serializer, and gaining one would be a design failure rather than a convenience.

The core model

Exercise — the vocabulary

A curated catalog, not an open string space. An entry is opaque and obtainable only by lookup, keyed by /equipment × movement × variation/; a stable private string id exists solely for external boundaries.

Two relations matter, and both are author-defined rather than inferred: may_pre_exhaust asks whether a pair shares the isolation's target, and may_substitute asks whether a candidate appears on HD1's own "or" list for the original. Novelty is not a virtue here — the catalog is closed on purpose.

Recovery — measurement, and permission

timestamp and duration are private int, so arithmetic on them is deliberate. elapsed is total: it yields zero rather than a negative duration when clocks disagree.

readiness is Ready or Recovering { rested; recommended } — the reading a client needs to say how much longer. clearance is abstract, and basis reports afterwards how it was obtained: Recovered, or Overridden { rested; recommended }.

Prescription — the plan

Rep_range validates authored calibration bands against HD1's 6–12 limits. Stimulus is one prescribed drive: a delivery, its rep window, and its allowed substitutes. Workout is an ordered, non-empty sequence of stimuli — Day 1, and so on. Routine is the cycle: its workouts, workout_after advancing by identity so rotation follows from what was last performed, and the recovery owed after each (training_interval 48h within the cycle, cycle_rest 72h after its final workout). It ships HD1's Ideal Routine as ideal.

Authoring errors raise. There is no result here because a malformed prescription is a bug in a hand-written plan, not user input.

Evidence — the record

Stimulus is one performed drive: efforts carrying exercise, load, reps, and outcome, delivered Single or as a Pair.

Workout is a prescribed workout being performed or already performed. It is the module where the plan/record boundary is enforced in both directions:

• start demands a clearance and a start time.
• add_stimulus records against the next matching unanswered slot, or as extra volume once every matching slot is answered, and refuses a stimulus no slot calls for.
• replace_stimulus ~slot *corrects* a slot in place. A fixed typo is not another set.
• record_at ~slot appends at a named slot, preserving prior fills. This is the faithful-replay primitive the codec needs to reconstruct performed verbatim, including recorded extra volume.
• filled_slots counts distinct answered slots, so a correction can never inflate completion.

Log is history: workouts most recent first, dated observations per exercise oldest first, and readiness computed from the last finished workout. Evidence is dated because a stall is *defined* by two weeks of nothing.

Feedback is a typed vocabulary for reported signals — sleep, appetite, readiness, motivation, difficulty, pain, injury, insufficient preparation — with duplicate categories rejected. Leveled signals carry a five-point score, 1 (very poor) to 5 (very good); these are wellness self-reports, never a measure of set intensity. The application stores reports independently of workouts, and the web tier records them through a sequential optional flow. The flow keeps its partial answers: Back and Skip preserve them, Close cancels the flow, and a report may be saved as a partial list. The logbook draws a small inline-SVG time graph of the leveled scores, one line per factor, once two reports carry a factor.

Progression — the judgment

assess reports Progressing or Stalled from observations, or raises Insufficient_data. stall_window is 14 days. remedy returns Some only for a stall, and only ever subtracts. judge_load reads a single effort against its prescribed band: below the floor is Too_heavy, twelve reps triggers Increase, otherwise Hold — the ceiling of the authored band is deliberately not a trigger, since load_increase_trigger is twelve regardless of the range. diagnose reports habits HD1 names as causes of overtraining: recorded volume beyond the prescription, extensions on every stimulus, and training under-recovered.

Boundaries

The core is pure, so every messy thing has an assigned place outside it.

| Concern | Where it lives | Why not in the core | |-----------------+---------------------------------+----------------------------------------------------| | identity | Repository, Trainee | a plan needs a name only once something remembers | | wall-clock time | hito.web (Handlers) | a pure domain cannot read a clock | | untrusted forms | hito.web (Decode) | the core accepts trusted values | | stored text | hito.app (Codec) | opaque types carry no serializers | | recovery policy | hito.app (Service) | one policy, so no client can loosen it | | persistence | Repository port + adapters | the domain must not know SQL exists | | phrasing | hito.web (Handlers.Present) | wording is presentation, not domain |

Identity and per-trainee state

Repository is a pure module type — no database, no framework. routine_id and workout_id are private string, minted by adapters. Every operation is scoped to a Trainee.id.

There is no server-wide state. A trainee's active routine and workout in progress are *stored*, not held in a slot, so nothing is lost across a restart and two trainees never collide. finish_workout saves a finished workout and clears the in-progress slot as one unit, so a workout is never both filed in history and still shown as in progress.

Adapters: Memory_repo for tests, Sqlite_repo over Caqti for production. Migrations is a versioned ledger — each migration numbered and named, applied inside a transaction, recorded in schema_migrations so a reconnect applies only what is missing; statements still use IF NOT EXISTS so a file from an earlier, ledger-less build stays safe. It also creates the dream_session table Dream's SQL sessions expect.

Serialization

Codec captures only what was *performed* — exercise, load, reps, outcome, timestamps, and the basis a workout was begun on — and rebuilds an Evidence.Workout.t by driving the same constructors a live session drives. A stored record therefore cannot describe a workout the core would refuse.

A prescription is *not* stored. It is found again by name in Catalog. That is the intended coupling: prescriptions are authored, not recorded. The cost is that a stored workout stays valid only as long as its routine and workout names do, and Codec reports that as Unknown_routine or Unknown_workout_name rather than raising.

Each stored stimulus carries the slot it filled, so a corrected or out-of-order record replays into the same slot.

Policy

Service is a functor over Repository.S and is the API a client calls — no HTML, no serialization. It is the only module that decides how a clearance is obtained: earned, or taken through begin_workout's ?override acknowledgment. A native client added later therefore cannot quietly adopt looser rules than the web one. It holds no mutable state of its own.

Accounts and sessions

Trainee normalizes a username — trimmed, lowercased, 4 to 20 characters — and holds a credential that carries a salted hash and never the password. Hashing and constant-time verification happen inside that module through safepass, so no other layer holds a plaintext password beyond a request.

Passwords carry no length or content policy, so they never refuse registration. Public sign-up is closed by default: Handlers.make ?registration_open defaults to false, which removes the /register routes and hides the link; bin/main.ml seeds one account idempotently from HITO_SEED_PASSWORD.

A session holds the trainee id in a signed cookie. Every application route resolves it through one authenticated combinator that passes the trainee to a continuation, so a route with any number of path captures shares one gate. Every state-changing POST verifies a signed CSRF token.

Every failure renders a branded page that names only the class of failure, so no server string leaks. A catch-all route serves the 404 for any unclaimed path and keeps the navigation, so an unknown URL is one tap from a known destination. Handlers.error_handler, wired into Dream.run, covers the rest: 5xx responses and uncaught exceptions.

The cycle

graph LR
  R[Prescription.Routine] -->|workout_after| WP[Prescription.Workout]
  WP -->|start, needs clearance| W[Evidence.Workout]
  S[Evidence.Stimulus] --> W
  W -->|finish| L[Evidence.Log]
  L -->|dated observations| P[Progression]
  L -->|elapsed| RC[Recovery]
  RC -->|clearance| W
  P -.->|remedy| R

Plan and record are distinct types with a one-way transition: a prescription never learns what was performed, and the log never interprets.

The dashed arrow is the one link nothing automates. Progression.remedy returns a remedy; no code applies it to a routine. Acting on it belongs to a tier that does not exist yet, and inventing one silently would violate the rule that plans are authored.

The web tier

Routes, Decode, Pages, Handlers, and a small js_of_ocaml client. Dream and dream-html appear nowhere else. Handlers is a functor over Repository.S, so production runs on SQLite while tests run in memory.

Every domain and service error becomes a user-facing sentence in one Present module, so a handler renders a message rather than inventing wording, and a new error variant surfaces as a missing case.

Route surface

| Route | Method | Purpose | |---------------------------------+-----------+------------------------------------------------| | /login | GET, POST | Sign in | | /register | GET, POST | Create an account (absent unless opened) | | /logout | POST | Sign out | | / | GET | Overview: next workout and the recovery gate | | /routines | GET | Choose a routine | | /routines/:id/select | POST | Make a routine active | | /routine | GET | Active routine detail | | /workout | GET | The workout in progress | | /workout | POST | Begin the next workout, or refuse at the gate | | /workout/slots/:slot | POST | Record one prescribed stimulus | | /workout/slots/:slot/edit | POST | Correct a recorded slot | | /workout/finish | POST | Complete and persist | | /workout/cancel | POST | Discard without saving | | /logbook | GET | All recorded evidence for the user | | /logbook/:id | GET | A saved workout | | /logbook/:id/slots/:slot | POST | Add a missing record | | /logbook/:id/slots/:slot/edit | POST | Correct a saved slot | | /feedback | POST | Advance or save subjective feedback | | /feedback/cancel | POST | Discard the current feedback flow | | /app-feedback | GET | Write or review application feedback | | /app-feedback/submit | POST | Submit application feedback | | /app-feedback/:id/upvote | POST | Upvote another trainee's feedback | | /app-feedback/:id/edit | POST | Edit owned application feedback | | /app-feedback/:id/remove | POST | Remove owned application feedback | | /profile | GET | Account profile: rename and change password | | /profile/username | POST | Change the username | | /profile/password | POST | Change the password (verifies the current one) | | /assets/hito.css | GET | Stylesheet (embedded at build time) | | /assets/workout-client.js | GET | Enhancement client (embedded at build time) |

Slot and record identity live in the path rather than hidden fields.

The refusal at POST /workout redirects to the overview, which reports the remaining rest and offers an explicit override action. The interface therefore makes the clearance invariant visible instead of training early by accident.

The workout view

One page serves both the workout in progress and a saved record. It shows one prescribed slot at a time under a server-rendered exercise selector carrying its slot in ?slot=. The selected option identifies the active slot. A handler clamps a requested slot against the prescription and otherwise opens on the default: the first slot still awaiting a record, or the first slot when all are filled.

This is form navigation and route state, not an ARIA widget — deterministic, and correct with no client script at all.

Progressive enhancement

The js_of_ocaml client is an enhancement, never a requirement. Server-rendered HTML remains the only source of UI, and the fallback is the ordinary link/form behaviour the pages already have.

The contract is a set of markers the server emits:

| Marker | Meaning | |----------------------------+-----------------------------------------------| | data-hito-app-shell | the replaceable shell; carries the page title | | data-hito-app-content | the page surface inside it | | data-hito-app-link | a link eligible for in-place navigation | | data-hito-app-form | a form eligible for in-place submission | | data-hito-workout-* | the same, for current-workout slots and forms | | data-hito-workout-status | an aria-live region for announcements | | data-hito-toast | a transient notice the client dismisses | | data-hito-dialog-open | a button that opens the modal with that id |

Behaviour: the client fetches the same URL the link or form would have used, extracts the marked region from the response, and swaps it. Successful transitions push the final response URL, so redirects stay reflected in the address bar; server-rendered validation responses render in place *without* a history entry. A monotonic request counter makes the newest interaction win, and aria-busy marks the shell while one is pending. Recording a stimulus returns to the submitted slot rather than the server's default, which is the one place the client shapes the flow. Anything it cannot apply — a missing marker, a transport failure, a modified click — falls back to native navigation.

The browser holds no domain logic. It never decides whether a set is valid, whether recovery is complete, or whether a correction is volume.

*Every form uses POST-redirect-GET.* A state-changing POST answers with a 303 redirect to the page that started the flow — the workout, the logbook, the profile, or the app-feedback tab — so a refresh never re-posts. The redirect target carries any message two ways: a transient success or error note rides a one-shot session flash (hito.flash), read once and shown as a data-hito-toast; a confirmation that must survive a bookmarked reload rides a query flag such as /profile?changedusername. Field-level validation is the one exception: a rejected login, registration, or profile edit re-renders its form in place with a 400= status, so the entered values and the per-field messages survive. That response carries no history entry and never mutates state, so it does not break the redirect rule.

Running it

  dune build && ./_build/default/bin/main.exe # http://localhost:8080/

bin/main.ml opens the store, applies migrations, seeds the single account, and starts Dream. The socket binds *loopback only*.

| Variable | Purpose | Default | |----------------------+---------------------------------------+-------------------------| | HITO_DB | Caqti database URI | sqlite3:hito.sqlite | | HITO_SECRET | Signs session cookies and CSRF tokens | random per run | | HITO_PORT | TCP port | 8080 | | HITO_SEED_PASSWORD | Password for the seeded account | none — refuses to start |

Set HITO_SECRET in production; unset, sessions do not survive a restart.

Dream runs its own SQL pool for sessions against the same file as Sqlite_repo. SQLite serializes writers, so this is safe for local use; a separate session store is the path to higher concurrency.

Verification

One Alcotest suite per module, test/test_<module>.ml, each exposing suite, registered in test/test_hito.ml in layer order: vocabulary, plan, record, judgment, service, serialization, storage, decoding, web.

What the less obvious suites are for:

• test_codec — a stored workout round-trips faithfully, and malformed or incomplete text is *reported*, not raised.
• test_sqlite_repo — state survives a reconnect, trainees stay isolated, reapplying migrations is idempotent, and finishing is atomic across a reconnect, against a temporary database file.
• test_decode — the trust boundary: form values are validated before the core sees them.
• test_web — carries the session cookie and CSRF token between requests, so authentication, the recovery gate, corrections, and the no-JavaScript behaviour are exercised end to end.

Done means, in order: dune build @check clean, dune runtest passing, dune fmt applied with dune build @fmt clean, and documentation that matches the change.

Tensions with the source

:PROPERTIES: :CUSTOM_ID: tensions :END:

Recorded rather than resolved, because HD1 does not settle them.

*48h against 72h.* Chapter 3 says up to 72 hours of rest, sometimes more, is needed for growth; the Ideal Routine prescribes training every other day. Mentzer does not reconcile these. We encode the routine — 48h within a cycle, 72h after it — and note the discrepancy here.

*Per-exercise rep windows.* HD1 gives one guideline, 6–10, for every listed exercise. We let a prescription name its own window, bounded to 6–12, on the argument that leg work may warrant a different range. A deliberate departure — and note that Mentzer's own rationale for the upper bound, cardiorespiratory failure arriving before muscular failure, cuts against higher reps for large compounds rather than for them.

*Extra volume is recordable.* HD1 forbids it in the strongest terms, but a log that refuses to state what happened is worse than one recording an error. The constraint lives on the prescription side, which cannot ask for extra work; performing extra shows up as more stimuli than slots.

*Extension rarity is a diagnostic, not an invariant.* Same reason. HD1 says never to extend every exercise of a workout; if you did, the record must say so.

*Deadlifts substitute for hyperextensions* across mechanics, because HD1 offers them as alternatives despite one being an isolation and the other a compound.

*The log form offers one extension, not a stack.* Evidence.Stimulus permits forced reps /then/ negatives, as HD1 describes; the web form currently offers a single choice. A limitation of the form, not the model.

*No consolidation routine.* HD2 material, and we have no source for it.

Deferred

• Progression.remedy is computed but never applied to a routine — the dashed arrow above.
• Equipment granularity, so a suggested load is one a bar can actually hold.
• A trainee layer carrying individual recovery ability, spotter availability, and the way recovery needs outgrow strength as a trainee gets stronger.
• HD2 consolidation, once sourced.
• A separate session store, for concurrency beyond local use.
• A native client, which would sit on hito.app beside the web tier.