#+TITLE: 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][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. #+begin_src 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 #+end_src 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 #+begin_src mermaid 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 #+end_src 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?changed=username=. 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 #+begin_src sh dune build && ./_build/default/bin/main.exe # http://localhost:8080/ #+end_src =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_.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.