docs rewrite architecture from first principles

Derive the architecture from Heavy Duty's constraints before describing\nmodules and boundaries, and keep the document aligned with the current\nfive-module core, route surface, and progressive web client.

Commit
26b45d3387cfac08bd6c82058fd417bb4d6af5ce
Author
Marius Peter <dev@marius-peter.com>
Author date
Committer
Marius Peter <dev@marius-peter.com>
Committer date
Changed files
ARCHITECTURE.md
index a0c237d3..00000000 100644..000000
@@ -1,340 +0,0 @@
1 Removed: # hito architecture
2 Removed:
3 Removed: A weightlifting tracker that encodes Mike Mentzer's Heavy Duty in the type
4 Removed: system. This document describes the code as it stands, and is derived from
5 Removed: *Heavy Duty I* (HD1) as the primary source; `doc/` holds the text.
6 Removed:
7 Removed: ## What exists
8 Removed:
9 Removed: Mentzer argued bodybuilding had to be derived from principles rather than copied
10 Removed: from champions, so the domain is carved along his claims rather than along
11 Removed: convenient nouns.
12 Removed:
13 Removed: **The stimulus is the unit of work** — one drive to muscular failure. HD1
14 Removed: prescribes one set per exercise, so there is no set count to record, and no "set
15 Removed: group" wrapping anything. How a drive was delivered is a property of the stimulus.
16 Removed:
17 Removed: **Reaching failure is an invariant, not data.** A recorded effort went to
18 Removed: failure by construction; that is what separates a stimulus from mere exercise.
19 Removed: What varies is load, the reps it happened to yield, and whether anything carried
20 Removed: the effort past failure.
21 Removed:
22 Removed: **Recovery is a precondition.** Training before the body has replenished its
23 Removed: reserves is HD1's primary error, and its effects are systemic rather than local.
24 Removed: Beginning a workout therefore demands an unforgeable clearance.
25 Removed:
26 Removed: **The logbook is the only source of evidence.** Progress is knowable only from
27 Removed: records, so history is never edited to suit the theory.
28 Removed:
29 Removed: **Judgment is one module's job.** Prescriptions state what to do, the logbook
30 Removed: states what happened, and `Progression` alone decides what that means.
31 Removed:
32 Removed: ## Layers
33 Removed:
34 Removed: One library, `hito.core`, with eleven modules. Dependencies point downward.
35 Removed:
36 Removed: ```
37 Removed: vocabulary Units · Muscle · Exercise
38 Removed: normative Prescription · Workout_prescription · Routine
39 Removed: factual Stimulus · Entry · Logbook
40 Removed: inferential Progression
41 Removed: Recovery straddles: it measures fact, and issues a
42 Removed: normative clearance
43 Removed: ```
44 Removed:
45 Removed: The split is epistemic — what a module *claims* — expressed as layering and
46 Removed: documentation rather than as sub-libraries or a module of constants. There is no
47 Removed: `Principle` module: a module cohering around "things that are true" is a
48 Removed: constants bag, and each principle is instead enforced where it bites.
49 Removed:
50 Removed: | Principle | Enforced at |
51 Removed: |-------------------------------------------|-------------------------------------------------------|
52 Removed: | 6-12 stimulus window | `Rep_range.limits` |
53 Removed: | one drive to failure per slot | `Prescription`'s shape — no set count exists to raise |
54 Removed: | isolation into compound, sharing a muscle | `Exercise.may_pre_exhaust` |
55 Removed: | every other day, then two days off | `Routine.recovery_after` |
56 Removed: | load rises at twelve reps, by 10-20% | `Progression.judge_load` |
57 Removed: | never add work on a stall | `Progression.remedy` |
58 Removed:
59 Removed: Only the first, third and fourth are runtime checks; the second is the absence of
60 Removed: a field, and the last two are the shape of a return type. That is the intended
61 Removed: bias — a principle enforced by a type cannot be forgotten at a call site.
62 Removed:
63 Removed: Above the core sit two more libraries, dependencies pointing inward only:
64 Removed:
65 Removed: - **`hito.app`** — `Trainee`, `Repository` (a port), `Catalog`, `Codec`,
66 Removed: `Memory_repo`, `Sqlite_repo`, `Migrations`, and `Service`. Identity is
67 Removed: assigned here, since the core carries none, and so is recovery policy:
68 Removed: `Service` is the only thing that decides how a `Recovery.clearance` is
69 Removed: obtained, so a second client cannot quietly adopt looser rules than the
70 Removed: first. Every `Repository` and `Service` operation is scoped to a
71 Removed: `Trainee.id`. There is no server-wide state: a trainee's active routine and
72 Removed: workout in progress are stored, not held in a slot.
73 Removed: - **`hito.web`** — `Routes`, `Decode`, `Pages`, `Handlers`, and a
74 Removed: authenticated-app `js_of_ocaml` client. Dream and dream-html live only here.
75 Removed: Wall-clock time enters here, never in the core.
76 Removed: `Handlers` is a functor over `Repository.S`, so production runs on
77 Removed: `Sqlite_repo` while tests run on `Memory_repo`. Authenticated pages ship a
78 Removed: small `js_of_ocaml` enhancement client: it replaces marked app content for
79 Removed: navigation, routine selection, workout start/finish/cancel, saved-record
80 Removed: edits, current workout logging, sign-in, registration, and sign-out. Every
81 Removed: JavaScript-disabled workflow retains ordinary browser navigation and
82 Removed: CSRF-protected server forms. Authentication uses one
83 Removed: `authenticated` combinator: it resolves the signed-in trainee and passes it
84 Removed: to a continuation, so a route with any number of path captures shares one
85 Removed: gate. Every domain and service error becomes a user-facing sentence in one
86 Removed: `Present` module, so a handler renders a message rather than choosing its
87 Removed: wording. The workout view — the same page for the workout in progress and a
88 Removed: saved history record — shows one prescribed slot at a time under a strip of
89 Removed: named tabs. Each tab is a server-rendered link that carries its slot in a
90 Removed: `?slot=` query parameter, so the view is deterministic route state with no
91 Removed: client script; the active link is marked with `aria-current="page"`. A
92 Removed: handler clamps a requested slot against the prescription and otherwise opens
93 Removed: on the default: the first slot still awaiting a record, or the first slot
94 Removed: when every slot is filled.
95 Removed:
96 Removed: ### Accounts, sessions, and storage
97 Removed:
98 Removed: - **Trainee** — an account: an opaque id, a normalized username, and a password
99 Removed: credential. A username is trimmed and lowercased, then required to be 4 to 20
100 Removed: characters. A credential carries a bcrypt hash, never the password, and the
101 Removed: hash is computed and checked inside this module through `safepass`. Passwords
102 Removed: carry no length or content policy.
103 Removed: - **Registration posture** — public sign-up is closed for now. `Handlers.make`
104 Removed: takes `?registration_open` (default `false`): when unset the `/register`
105 Removed: routes are absent and the sign-in page hides its Register link. `bin/main.ml`
106 Removed: seeds a single account (`blendux`) on startup, idempotently, with the password
107 Removed: from `HITO_SEED_PASSWORD` (required; the server refuses to start without it).
108 Removed: Reopening sign-up is a one-argument change plus removing the seed.
109 Removed: - **Repository port** — trainee-scoped account, catalog, selection,
110 Removed: in-progress, and history operations, plus a transactional `finish_workout`
111 Removed: that saves a finished workout and clears the in-progress slot as one unit.
112 Removed: Effects run in Lwt, because an adapter may talk to a database.
113 Removed: - **Sqlite_repo** — the durable store, backed by SQLite through Caqti. It stores
114 Removed: performed facts through `Codec` as opaque encoded strings and never inspects
115 Removed: domain shape. `Migrations` creates the schema on connect, including the
116 Removed: `dream_session` table Dream's SQL sessions expect. Finishing a workout —
117 Removed: saving it to history and clearing the in-progress slot — runs in one
118 Removed: transaction, so the two rows never disagree after a crash.
119 Removed: - **Migrations** — versioned, tracked schema migrations. Each migration is a
120 Removed: numbered, named set of statements; a `schema_migrations` ledger records which
121 Removed: versions a file carries, so a reconnect applies only what is missing and each
122 Removed: migration runs inside a transaction. Statements still use `IF NOT EXISTS`, so
123 Removed: a file from an earlier, ledger-less build stays safe.
124 Removed: - **Codec** — the serialization boundary. It captures only what was performed
125 Removed: and rebuilds a `Evidence.Workout.t` by driving the same core constructors a
126 Removed: live session does. Each stored stimulus carries the prescription slot it
127 Removed: filled, so a corrected or out-of-order record replays into the same slot; a
128 Removed: record from before slots were stored replays in performance order instead. A
129 Removed: prescription is not stored; it is found again by name in the `Catalog`. This
130 Removed: keeps the core unchanged and carries no serializers.
131 Removed: - **Authentication** — `Handlers` verifies a local username and password, then
132 Removed: stores the trainee id in a signed session. Every application route requires
133 Removed: an authenticated trainee and redirects to the sign-in page otherwise. Every
134 Removed: state-changing POST verifies a CSRF token; the token is signed, not stored.
135 Removed:
136 Removed: ## Modules
137 Removed:
138 Removed: ### Vocabulary
139 Removed:
140 Removed: - **Values** — load in kilograms and repetitions are primitive values. The core
141 Removed: accepts them as trusted input and does not return validation results. `hito.web`
142 Removed: is the trust boundary. Its decoder treats form values as untrusted and validates
143 Removed: finite, nonnegative loads and positive repetitions before it calls the core.
144 Removed: `Prescription.Rep_range` validates authored calibration ranges.
145 Removed: - **Muscle** — the training targets HD1 names, plus the assisting muscles its
146 Removed: weak-link argument needs. Glutes never appear in HD1 and forearms only
147 Removed: anatomically; both are here because a compound must have something able to
148 Removed: serve the muscle it pre-exhausts. Deliberately minimal otherwise: nothing but
149 Removed: pre-exhaust validation consults it.
150 Removed: - **Exercise** — the curated catalog. Each opaque entry is keyed by
151 Removed: equipment × movement × variation, while a stable string ID serves only
152 Removed: external serialization. Each entry carries a mechanic and worked muscles.
153 Removed: Substitutions come from HD1's own "or" lists, grouped so symmetry is
154 Removed: structural.
155 Removed:
156 Removed: ### Normative — the plan
157 Removed:
158 Removed: - **Prescription** — one prescribed stimulus: a delivery, plus the rep window
159 Removed: calibrating its load. Delivery is `Single` or `Pre_exhaust`, and nothing else:
160 Removed: in HD1 "superset" *means* pre-exhaustion.
161 Removed: - **Workout_prescription** — an ordered sequence of prescribed stimuli, such as
162 Removed: Day 1. Volume needs no representation, being the length of that sequence.
163 Removed: - **Routine** — the cycle of workouts, and how long to rest between them.
164 Removed: `workout_after` advances by identity, so rotation follows from what was last
165 Removed: performed. Ships HD1's Ideal Routine.
166 Removed:
167 Removed: ### Factual — the record
168 Removed:
169 Removed: - **Stimulus** — one drive to failure: how it was delivered, what each effort
170 Removed: lifted, and whether extensions carried it past failure. Warm-ups sit alongside
171 Removed: and carry no outcome, so a warm-up cannot reach failure by type.
172 Removed: - **Entry** — a workout performed against its prescription. Starting one requires
173 Removed: a clearance; adding a stimulus requires that the prescription actually calls
174 Removed: for it. `add_stimulus` fills the next matching slot or records extra volume;
175 Removed: `replace_stimulus ~slot` corrects one slot in place, and `record_at ~slot` is
176 Removed: the faithful-replay primitive the codec uses. A correction is not extra work.
177 Removed: - **Logbook** — every entry, plus the questions history answers: what was
178 Removed: performed last, how long since the last finished workout, and what an effort
179 Removed: has done over time. Evidence is dated, because a stall is defined by two weeks
180 Removed: of nothing.
181 Removed:
182 Removed: ### Recovery
183 Removed:
184 Removed: Timestamps, durations, elapsed rest, a readiness reading — and `clearance`, an
185 Removed: abstract permission to train. A clearance is either earned by having recovered,
186 Removed: or taken through `override`, which records how long you had rested and why you
187 Removed: went ahead. The override is not an escape hatch but evidence: it is what lets a
188 Removed: stall later be attributed to training under-recovered.
189 Removed:
190 Removed: ### Inferential
191 Removed:
192 Removed: - **Progression** — whether the record shows progress, and what follows. Progress
193 Removed: is an increase in reps, weight or both, one rep being significant. A stall is
194 Removed: progress ceasing entirely for two weeks, and its single remedy subtracts: a
195 Removed: week off, one fewer stimulus per workout, an extra rest day. There is no
196 Removed: additive remedy, structurally. It can also decline to judge: too short or too
197 Removed: recent a record yields `Insufficient_data` rather than a guess, so two flat
198 Removed: sessions a day apart never condemn a routine. Diagnostics report habits HD1
199 Removed: names as causes of overtraining.
200 Removed:
201 Removed: ## The cycle
202 Removed:
203 Removed: ```mermaid
204 Removed: graph LR
205 Removed: R[Routine] -->|workout_after| WP[Workout_prescription]
206 Removed: WP -->|start, needs clearance| E[Entry]
207 Removed: S[Stimulus] --> E
208 Removed: E --> L[Logbook]
209 Removed: L -->|dated evidence| P[Progression]
210 Removed: L -->|elapsed| RC[Recovery]
211 Removed: RC -->|clearance| E
212 Removed: P -.->|remedy| R
213 Removed: ```
214 Removed:
215 Removed: Plan and record are distinct types with a one-way transition. Prescriptions never
216 Removed: learn what was performed; the logbook never interprets.
217 Removed:
218 Removed: The dashed arrow is the one link nothing automates: `Progression.remedy` returns
219 Removed: a remedy, but no code applies it to a routine. Acting on it belongs to a tier
220 Removed: that does not exist yet.
221 Removed:
222 Removed: ## Running it
223 Removed:
224 Removed: ```
225 Removed: dune build && ./_build/default/bin/main.exe # http://localhost:8080/
226 Removed: ```
227 Removed:
228 Removed: `bin/main.ml` opens the SQLite store, applies migrations, and starts Dream. The
229 Removed: socket binds **loopback only**. Configuration comes from the environment:
230 Removed:
231 Removed: | Variable | Purpose | Default |
232 Removed: |---------------|---------------------------------------|------------------------|
233 Removed: | `HITO_DB` | Caqti database URI | `sqlite3:hito.sqlite` |
234 Removed: | `HITO_SECRET` | Signs session cookies and CSRF tokens | a random per-run value |
235 Removed: | `HITO_PORT` | TCP port | `8080` |
236 Removed:
237 Removed: Set `HITO_SECRET` in production. When it is unset, the server generates a random
238 Removed: secret for that run, so sessions do not survive a restart.
239 Removed:
240 Removed: Authentication is local username and password. A username is normalized and must
241 Removed: be 4 to 20 characters; a password has no length or content policy. A password is
242 Removed: stored as a bcrypt hash. A session holds the trainee id in a signed cookie,
243 Removed: backed by the `dream_session` table. Every state-changing POST carries a signed
244 Removed: CSRF token.
245 Removed:
246 Removed: Storage is durable: trainees, their active routine, the workout in progress, and
247 Removed: history all live in SQLite. There is no server-wide in-memory state, and each
248 Removed: trainee has a separate logbook. The workout in progress is a stored row keyed by
249 Removed: trainee, so it survives a closed tab and a restart.
250 Removed:
251 Removed: Dream runs its own SQL pool for sessions against the same database file, next to
252 Removed: the pool `Sqlite_repo` opens. SQLite serializes writers, so this is safe for
253 Removed: local use. A separate session store is the path to higher concurrency.
254 Removed:
255 Removed: | Route | Method | Purpose |
256 Removed: |----------------------------|-----------|-------------------------------------------------------|
257 Removed: | `/register` | GET, POST | Create an account and sign in (disabled by default) |
258 Removed: | `/login` | GET, POST | Sign in |
259 Removed: | `/logout` | POST | Sign out |
260 Removed: | `/routines` | GET | Choose a routine |
261 Removed: | `/routines/:id/select` | POST | Make a routine active |
262 Removed: | `/routine` | GET | Active routine details |
263 Removed: | `/workout` | GET | The workout in progress |
264 Removed: | `/workout` | POST | Start the next workout or refuse at the recovery gate |
265 Removed: | `/workout/slots/:slot` | POST | Record one prescribed stimulus |
266 Removed: | `/workout/slots/:slot/edit`| POST | Correct a recorded slot (replaces it, adds no volume) |
267 Removed: | `/workout/finish` | POST | Complete and persist |
268 Removed: | `/history` | GET | What has been performed |
269 Removed: | `/history/:id` | GET | View a saved workout and its missing records |
270 Removed: | `/history/:id/slots/:slot` | POST | Add a missing saved record |
271 Removed: | `/history/:id/slots/:slot/edit` | POST | Correct a recorded slot of a saved workout |
272 Removed:
273 Removed: Dream permits nested resource paths, so slot and record identity live in the
274 Removed: path rather than hidden fields or query parameters.
275 Removed:
276 Removed: The refusal at `POST /workout` redirects to the overview. The overview reports
277 Removed: the remaining rest and offers an explicit override action. The override keeps
278 Removed: the rested and recommended durations in the entry. The UI therefore makes the
279 Removed: clearance invariant visible instead of silently training early.
280 Removed:
281 Removed: ## Tests
282 Removed:
283 Removed: One Alcotest suite per module, `test/test_<module>.ml`, each exposing a `suite`
284 Removed: value registered in `test/test_hito.ml` in layer order. `dune runtest`.
285 Removed: `test_codec` proves a stored workout round-trips faithfully and that malformed
286 Removed: or incomplete text is reported, not raised. `test_sqlite_repo` proves state
287 Removed: survives a reconnect and trainees stay isolated, that reapplying migrations is
288 Removed: idempotent, and that finishing is atomic across a reconnect, using a temporary
289 Removed: database file. `test_web` carries the session cookie and CSRF token between
290 Removed: requests, so it exercises authentication end to end.
291 Removed:
292 Removed: ## Deviations and tensions
293 Removed:
294 Removed: Recorded rather than resolved, since the source does not settle them.
295 Removed:
296 Removed: **48h against 72h.** Chapter 3 says up to 72 hours of rest, and in some cases
297 Removed: more, is needed for growth. The Ideal Routine prescribes training every other
298 Removed: day. Mentzer does not reconcile these. We encode what the routine says — 48h
299 Removed: within a cycle, 72h after it — and note the discrepancy here.
300 Removed:
301 Removed: **Per-exercise rep windows.** HD1 gives one guideline, 6-10, for every listed
302 Removed: exercise. We allow a prescription to name its own window, bounded to lie within
303 Removed: 6-12, on the argument that leg work may warrant a different range. This is a
304 Removed: deliberate departure. Note that Mentzer's own rationale for the upper bound —
305 Removed: cardiorespiratory failure arriving before muscular failure — cuts against higher
306 Removed: reps for large compounds rather than for them.
307 Removed:
308 Removed: **No consolidation routine.** HD2 material, and we have no source for it.
309 Removed:
310 Removed: **Extra volume is recordable.** HD1 forbids it in the strongest terms, but a log
311 Removed: that refuses to state what happened is worse than one that records an error. The
312 Removed: constraint lives on the prescription side, which cannot prescribe extra work;
313 Removed: performing extra shows as more stimuli than slots. A correction is distinct from
314 Removed: extra volume: `Evidence.Workout.replace_stimulus ~slot` targets one slot and
315 Removed: replaces its record, so fixing a mistyped load never counts as another set. The
316 Removed: web edit forms and the `.../slots/:slot/edit` routes drive this API, and the
317 Removed: completion count (`filled_slots`) counts distinct answered slots, so a correction
318 Removed: never advances or inflates it.
319 Removed:
320 Removed: **Extension rarity is a diagnostic, not an invariant.** Same reason: HD1 says
321 Removed: never to extend every exercise of a workout, but if you did, the record must say
322 Removed: so. Invariants belong on plans, which you author; not on history, which you
323 Removed: observe.
324 Removed:
325 Removed: **Deadlifts substitute for hyperextensions** across mechanics, because HD1 offers
326 Removed: them as alternatives despite one being an isolation and the other a compound.
327 Removed:
328 Removed: **The log form offers one extension, not a stack.** `Stimulus` permits forced
329 Removed: reps *then* negatives, as HD1 describes; the web form currently offers a single
330 Removed: choice per stimulus. A limitation of the form, not the model.
331 Removed:
332 Removed: ## Deferred
333 Removed:
334 Removed: Authentication, per-trainee storage and workout state, and durable storage
335 Removed: behind the `Repository` port are now in place. What remains: equipment
336 Removed: granularity, so a suggested load is one a bar actually takes; a trainee layer
337 Removed: carrying individual recovery ability, spotter availability, and the way recovery
338 Removed: needs outgrow strength; HD2 consolidation once sourced; a separate session store
339 Removed: for higher concurrency; and a native client, which would sit on `hito.app`
340 Removed: beside the web tier.
ARCHITECTURE.org
index 00000000..45424f01 000000..100644
@@ -0,0 +1,507 @@
1 Added: #+title: hito architecture
2 Added: #+options: toc:2 num:nil
3 Added:
4 Added: hito is a training tracker for Mike Mentzer's Heavy Duty. This document derives
5 Added: the code from the doctrine, in that order: what the source claims, what those
6 Added: claims force to be true of a program, and how the code carries them.
7 Added:
8 Added: The source is /Heavy Duty I/ (HD1), in =doc/=. It is copyrighted reference
9 Added: material, gitignored, never committed.
10 Added:
11 Added: * Premise
12 Added:
13 Added: Mentzer's central methodological claim is that training must be derived from
14 Added: principles rather than copied from champions. A tracker that merely stores
15 Added: numbers abandons that claim: it would record an overtrained, under-recovered,
16 Added: volume-inflated program as happily as a correct one.
17 Added:
18 Added: So the program's job is not to hold data. It is to make the doctrine
19 Added: *structural* — to arrange types so that a training state the book forbids is
20 Added: difficult to represent and impossible to represent silently.
21 Added:
22 Added: Two rules follow, and they govern every decision below.
23 Added:
24 Added: 1. Where a design choice conflicts with the doctrine, the doctrine wins, or the
25 Added: conflict is recorded explicitly (see [[#tensions][Tensions with the source]]).
26 Added: 2. Where a deviation must be *possible* — a trainee really did train early, or
27 Added: really did perform an extra set — it must never be *silent*. It is
28 Added: represented, acknowledged, and retained.
29 Added:
30 Added: * First principles
31 Added:
32 Added: Six commitments. Each is a claim from HD1; each has a consequence the code is
33 Added: built to satisfy.
34 Added:
35 Added: ** Intensity is categorical, not scalar
36 Added:
37 Added: A working set is carried to momentary muscular failure. HD1 argues there are
38 Added: only two accurate measures of intensity: 0% at rest and 100% at failure.
39 Added:
40 Added: /Consequence./ Reaching failure is an invariant of the recorded type, not a
41 Added: field to be filled in. What varies is load, the reps it happened to yield, and
42 Added: whether anything carried the effort *past* failure — which is qualitative, not
43 Added: more of the same: =Beyond_failure= of forced reps, negatives, rest-pause, or a
44 Added: static hold. There is no numeric intensity score anywhere, and there never
45 Added: should be.
46 Added:
47 Added: ** The stimulus is the unit of work
48 Added:
49 Added: HD1 prescribes one drive per exercise. "Superset" in the book *means*
50 Added: pre-exhaustion: an isolation movement into a compound sharing its target, with
51 Added: no pause.
52 Added:
53 Added: /Consequence./ There is no set count in the model, on either side of the
54 Added: plan/record divide. Volume is not a number a caller supplies; it is the length
55 Added: of a list. A prescription therefore cannot ask for more work than one drive per
56 Added: slot, because there is no field in which to say so. Delivery is =Single= or
57 Added: =Pre_exhaust=, and nothing else.
58 Added:
59 Added: ** Recovery precedes growth
60 Added:
61 Added: Training stimulates growth; recovery produces it. Training before reserves are
62 Added: replenished is HD1's primary error, and its effect is systemic rather than
63 Added: local.
64 Added:
65 Added: /Consequence./ Beginning a workout demands an unforgeable permission:
66 Added: =Recovery.clearance=. It cannot be constructed by a caller who feels ready. It
67 Added: is either earned — =clear= returns =Some= only when recovery is complete — or
68 Added: taken deliberately through =override=, which records how long you had actually
69 Added: rested against what was recommended. The override is not an escape hatch; it is
70 Added: evidence, and it is what allows a later stall to be attributed to training
71 Added: under-recovered.
72 Added:
73 Added: ** Progress is the signal, and it is overload
74 Added:
75 Added: Progress is an increase in reps, weight, or both. One extra rep counts.
76 Added:
77 Added: /Consequence./ Reps are an *outcome*, never a target: a set ends at failure, not
78 Added: at a number. A prescribed range only calibrates load. When twelve reps are
79 Added: reached the load rises by 10–20%, so failure returns inside the band. Judgment
80 Added: returns a verdict type — =Hold=, =Increase= of a window, =Too_heavy= — rather
81 Added: than a bare number a caller might round into nonsense.
82 Added:
83 Added: ** On a stall, the answer is never more work
84 Added:
85 Added: HD1's remedy for stalled progress subtracts: a week off, then less volume and
86 Added: less frequency.
87 Added:
88 Added: /Consequence./ The remedy is a type with a single constructor,
89 Added: =Lay_off_then_reduce=, carrying a lay-off, stimuli to drop per workout, and
90 Added: extra rest. There is no additive remedy to choose by mistake, because none
91 Added: exists to name. Rising volume is a diagnostic warning, never an achievement.
92 Added:
93 Added: ** The record states facts; one module judges them
94 Added:
95 Added: Progress is knowable only from what was performed. A log that argues with
96 Added: history is useless.
97 Added:
98 Added: /Consequence./ =Evidence= records and never interprets. =Progression= is the
99 Added: only judge, and it may decline: =Insufficient_data= rather than a guess, so two
100 Added: flat sessions a day apart never condemn a routine. Invariants belong on plans,
101 Added: which are *authored*; not on history, which is *observed*.
102 Added:
103 Added: * What the principles force on the structure
104 Added:
105 Added: The model is split by what a module *claims*, not by convenient nouns:
106 Added:
107 Added: | Claim | Module | Answers |
108 Added: |-------------+----------------+--------------------------------|
109 Added: | vocabulary | =Exercise= | what movements exist, and pair |
110 Added: | normative | =Prescription= | what should be done |
111 Added: | factual | =Evidence= | what was done |
112 Added: | inferential | =Progression= | what that means |
113 Added:
114 Added: =Recovery= straddles the divide deliberately: it measures a fact (elapsed rest)
115 Added: and issues a normative artifact (a clearance). That is the one place the two
116 Added: kinds of claim legitimately meet, which is why permission to train lives there
117 Added: and nowhere else.
118 Added:
119 Added: There is no =Principle= module. A module cohering around "things that are true"
120 Added: is a constants bag; a principle stated in one place is a principle that can be
121 Added: ignored at every call site. Each is instead enforced where it bites:
122 Added:
123 Added: | Principle | Enforced at | Mechanism |
124 Added: |-----------------------------------------------+---------------------------------------+-----------|
125 Added: | one drive to failure per slot | shape of =Prescription.Stimulus= | absence |
126 Added: | a recorded effort reached failure | =Evidence.Stimulus.outcome= | type |
127 Added: | training requires recovery or acknowledgement | =Evidence.Workout.start= | type |
128 Added: | a stall is never answered with work | =Progression.remedy= return type | type |
129 Added: | a correction is not extra volume | =Evidence.Workout.replace_stimulus= | type |
130 Added: | 6–12 calibration window | =Prescription.Rep_range.limits= | runtime |
131 Added: | isolation into compound, sharing a target | =Exercise.may_pre_exhaust= | runtime |
132 Added: | substitutions come from author lists | =Exercise.may_substitute= | runtime |
133 Added: | 48h between workouts, 72h after the cycle | =Prescription.Routine.recovery_after= | value |
134 Added: | load rises at twelve reps, by 10–20% | =Progression.judge_load= | value |
135 Added:
136 Added: The bias is intentional: a principle carried by a type cannot be forgotten, and
137 Added: the runtime checks are confined to *authoring* — building a prescription,
138 Added: pairing two movements — where a violation is a programming error and raising is
139 Added: correct.
140 Added:
141 Added: * Layers
142 Added:
143 Added: Three libraries. Dependencies point inward only.
144 Added:
145 Added: #+begin_src
146 Added: hito.web Dream · dream-html · js_of_ocaml client
147 Added: | HTTP, HTML, sessions, CSRF, wall-clock time
148 Added: v
149 Added: hito.app Trainee · Repository (port) · Service · Catalog · Codec
150 Added: | identity, persistence, recovery policy, Lwt
151 Added: v
152 Added: hito.core Exercise · Recovery · Prescription · Evidence · Progression
153 Added: pure domain: no framework, no database, no serialization
154 Added: #+end_src
155 Added:
156 Added: The core is five modules, unwrapped (=wrapped false=), so they are referred to
157 Added: bare: =Prescription.Stimulus=, =Evidence.Workout=, =Evidence.Log=. It has no
158 Added: dependency on Lwt, Caqti, Dream, or any serializer, and gaining one would be a
159 Added: design failure rather than a convenience.
160 Added:
161 Added: * The core model
162 Added:
163 Added: ** Exercise — the vocabulary
164 Added:
165 Added: A curated catalog, not an open string space. An entry is opaque and obtainable
166 Added: only by lookup, keyed by /equipment × movement × variation/; a stable =private
167 Added: string= id exists solely for external boundaries.
168 Added:
169 Added: Two relations matter, and both are author-defined rather than inferred:
170 Added: =may_pre_exhaust= asks whether a pair shares the isolation's target, and
171 Added: =may_substitute= asks whether a candidate appears on HD1's own "or" list for the
172 Added: original. Novelty is not a virtue here — the catalog is closed on purpose.
173 Added:
174 Added: ** Recovery — measurement, and permission
175 Added:
176 Added: =timestamp= and =duration= are =private int=, so arithmetic on them is
177 Added: deliberate. =elapsed= is total: it yields zero rather than a negative duration
178 Added: when clocks disagree.
179 Added:
180 Added: =readiness= is =Ready= or =Recovering { rested; recommended }= — the reading a
181 Added: client needs to say how much longer. =clearance= is abstract, and =basis=
182 Added: reports afterwards how it was obtained: =Recovered=, or =Overridden { rested;
183 Added: recommended }=.
184 Added:
185 Added: ** Prescription — the plan
186 Added:
187 Added: =Rep_range= validates authored calibration bands against HD1's 6–12 limits.
188 Added: =Stimulus= is one prescribed drive: a delivery, its rep window, and its allowed
189 Added: substitutes. =Workout= is an ordered, non-empty sequence of stimuli — Day 1, and
190 Added: so on. =Routine= is the cycle: its workouts, =workout_after= advancing by
191 Added: identity so rotation follows from what was last performed, and the recovery owed
192 Added: after each (=training_interval= 48h within the cycle, =cycle_rest= 72h after its
193 Added: final workout). It ships HD1's Ideal Routine as =ideal=.
194 Added:
195 Added: Authoring errors raise. There is no =result= here because a malformed
196 Added: prescription is a bug in a hand-written plan, not user input.
197 Added:
198 Added: ** Evidence — the record
199 Added:
200 Added: =Stimulus= is one performed drive: efforts carrying exercise, load, reps, and
201 Added: outcome, delivered =Single= or as a =Pair=.
202 Added:
203 Added: =Workout= is a prescribed workout being performed or already performed. It is
204 Added: the module where the plan/record boundary is enforced in both directions:
205 Added:
206 Added: - =start= demands a clearance and a start time.
207 Added: - =add_stimulus= records against the next matching unanswered slot, or as extra
208 Added: volume once every matching slot is answered, and refuses a stimulus no slot
209 Added: calls for.
210 Added: - =replace_stimulus ~slot= *corrects* a slot in place. A fixed typo is not
211 Added: another set.
212 Added: - =record_at ~slot= appends at a named slot, preserving prior fills. This is the
213 Added: faithful-replay primitive the codec needs to reconstruct =performed= verbatim,
214 Added: including recorded extra volume.
215 Added: - =filled_slots= counts distinct answered slots, so a correction can never
216 Added: inflate completion.
217 Added:
218 Added: =Log= is history: workouts most recent first, dated =observations= per exercise
219 Added: oldest first, and =readiness= computed from the last finished workout. Evidence
220 Added: is dated because a stall is *defined* by two weeks of nothing.
221 Added:
222 Added: =Feedback= is a typed vocabulary for reported signals — sleep, appetite,
223 Added: readiness, motivation, difficulty, pain, injury, insufficient preparation — with
224 Added: duplicate categories rejected. It is defined and unit-tested in the core, and
225 Added: nothing in =hito.app= or =hito.web= consumes it yet.
226 Added:
227 Added: ** Progression — the judgment
228 Added:
229 Added: =assess= reports =Progressing= or =Stalled= from observations, or raises
230 Added: =Insufficient_data=. =stall_window= is 14 days. =remedy= returns =Some= only for
231 Added: a stall, and only ever subtracts. =judge_load= reads a single effort against its
232 Added: prescribed band: below the floor is =Too_heavy=, twelve reps triggers
233 Added: =Increase=, otherwise =Hold= — the ceiling of the authored band is deliberately
234 Added: not a trigger, since =load_increase_trigger= is twelve regardless of the range.
235 Added: =diagnose= reports habits HD1 names as causes of overtraining: extensions on
236 Added: every stimulus, and training under-recovered.
237 Added:
238 Added: * Boundaries
239 Added:
240 Added: The core is pure, so every messy thing has an assigned place outside it.
241 Added:
242 Added: | Concern | Where it lives | Why not in the core |
243 Added: |-----------------+---------------------------------+----------------------------------------------------|
244 Added: | identity | =Repository=, =Trainee= | a plan needs a name only once something remembers |
245 Added: | wall-clock time | =hito.web= (=Handlers=) | a pure domain cannot read a clock |
246 Added: | untrusted forms | =hito.web= (=Decode=) | the core accepts trusted values |
247 Added: | stored text | =hito.app= (=Codec=) | opaque types carry no serializers |
248 Added: | recovery policy | =hito.app= (=Service=) | one policy, so no client can loosen it |
249 Added: | persistence | =Repository= port + adapters | the domain must not know SQL exists |
250 Added: | phrasing | =hito.web= (=Handlers.Present=) | wording is presentation, not domain |
251 Added:
252 Added: ** Identity and per-trainee state
253 Added:
254 Added: =Repository= is a pure module type — no database, no framework. =routine_id= and
255 Added: =workout_id= are =private string=, minted by adapters. Every operation is scoped
256 Added: to a =Trainee.id=.
257 Added:
258 Added: There is no server-wide state. A trainee's active routine and workout in
259 Added: progress are *stored*, not held in a slot, so nothing is lost across a restart
260 Added: and two trainees never collide. =finish_workout= saves a finished workout and
261 Added: clears the in-progress slot as one unit, so a workout is never both filed in
262 Added: history and still shown as in progress.
263 Added:
264 Added: Adapters: =Memory_repo= for tests, =Sqlite_repo= over Caqti for production.
265 Added: =Migrations= is a versioned ledger — each migration numbered and named, applied
266 Added: inside a transaction, recorded in =schema_migrations= so a reconnect applies
267 Added: only what is missing; statements still use =IF NOT EXISTS= so a file from an
268 Added: earlier, ledger-less build stays safe. It also creates the =dream_session= table
269 Added: Dream's SQL sessions expect.
270 Added:
271 Added: ** Serialization
272 Added:
273 Added: =Codec= captures only what was *performed* — exercise, load, reps, outcome,
274 Added: timestamps, and the basis a workout was begun on — and rebuilds an
275 Added: =Evidence.Workout.t= by driving the same constructors a live session drives. A
276 Added: stored record therefore cannot describe a workout the core would refuse.
277 Added:
278 Added: A prescription is *not* stored. It is found again by name in =Catalog=. That is
279 Added: the intended coupling: prescriptions are authored, not recorded. The cost is
280 Added: that a stored workout stays valid only as long as its routine and workout names
281 Added: do, and =Codec= reports that as =Unknown_routine= or =Unknown_workout_name=
282 Added: rather than raising.
283 Added:
284 Added: Each stored stimulus carries the slot it filled, so a corrected or out-of-order
285 Added: record replays into the same slot.
286 Added:
287 Added: ** Policy
288 Added:
289 Added: =Service= is a functor over =Repository.S= and is the API a client calls — no
290 Added: HTML, no serialization. It is the only module that decides how a clearance is
291 Added: obtained: earned, or taken through =begin_workout='s =?override=
292 Added: acknowledgment. A native client added later therefore cannot quietly adopt
293 Added: looser rules than the web one. It holds no mutable state of its own.
294 Added:
295 Added: ** Accounts and sessions
296 Added:
297 Added: =Trainee= normalizes a username — trimmed, lowercased, 4 to 20 characters — and
298 Added: holds a =credential= that carries a salted hash and never the password. Hashing
299 Added: and constant-time verification happen inside that module through =safepass=, so
300 Added: no other layer holds a plaintext password beyond a request.
301 Added:
302 Added: Passwords carry no length or content policy, so they never refuse registration.
303 Added: Public sign-up is closed by default: =Handlers.make ?registration_open=
304 Added: defaults to =false=, which removes the =/register= routes and hides the link;
305 Added: =bin/main.ml= seeds one account idempotently from =HITO_SEED_PASSWORD=.
306 Added:
307 Added: A session holds the trainee id in a signed cookie. Every application route
308 Added: resolves it through one =authenticated= combinator that passes the trainee to a
309 Added: continuation, so a route with any number of path captures shares one gate. Every
310 Added: state-changing POST verifies a signed CSRF token.
311 Added:
312 Added: * The cycle
313 Added:
314 Added: #+begin_src mermaid
315 Added: graph LR
316 Added: R[Prescription.Routine] -->|workout_after| WP[Prescription.Workout]
317 Added: WP -->|start, needs clearance| W[Evidence.Workout]
318 Added: S[Evidence.Stimulus] --> W
319 Added: W -->|finish| L[Evidence.Log]
320 Added: L -->|dated observations| P[Progression]
321 Added: L -->|elapsed| RC[Recovery]
322 Added: RC -->|clearance| W
323 Added: P -.->|remedy| R
324 Added: #+end_src
325 Added:
326 Added: Plan and record are distinct types with a one-way transition: a prescription
327 Added: never learns what was performed, and the log never interprets.
328 Added:
329 Added: The dashed arrow is the one link nothing automates. =Progression.remedy= returns
330 Added: a remedy; no code applies it to a routine. Acting on it belongs to a tier that
331 Added: does not exist yet, and inventing one silently would violate the rule that plans
332 Added: are authored.
333 Added:
334 Added: * The web tier
335 Added:
336 Added: =Routes=, =Decode=, =Pages=, =Handlers=, and a small =js_of_ocaml= client. Dream
337 Added: and dream-html appear nowhere else. =Handlers= is a functor over =Repository.S=,
338 Added: so production runs on SQLite while tests run in memory.
339 Added:
340 Added: Every domain and service error becomes a user-facing sentence in one =Present=
341 Added: module, so a handler renders a message rather than inventing wording, and a new
342 Added: error variant surfaces as a missing case.
343 Added:
344 Added: ** Route surface
345 Added:
346 Added: | Route | Method | Purpose |
347 Added: |---------------------------------+-----------+-----------------------------------------------|
348 Added: | =/login= | GET, POST | Sign in |
349 Added: | =/register= | GET, POST | Create an account (absent unless opened) |
350 Added: | =/logout= | POST | Sign out |
351 Added: | =/= | GET | Overview: next workout and the recovery gate |
352 Added: | =/routines= | GET | Choose a routine |
353 Added: | =/routines/:id/select= | POST | Make a routine active |
354 Added: | =/routine= | GET | Active routine detail |
355 Added: | =/workout= | GET | The workout in progress |
356 Added: | =/workout= | POST | Begin the next workout, or refuse at the gate |
357 Added: | =/workout/slots/:slot= | POST | Record one prescribed stimulus |
358 Added: | =/workout/slots/:slot/edit= | POST | Correct a recorded slot |
359 Added: | =/workout/finish= | POST | Complete and persist |
360 Added: | =/workout/cancel= | POST | Discard without saving |
361 Added: | =/history= | GET | What has been performed |
362 Added: | =/history/:id= | GET | A saved workout |
363 Added: | =/history/:id/slots/:slot= | POST | Add a missing record |
364 Added: | =/history/:id/slots/:slot/edit= | POST | Correct a saved slot |
365 Added: | =/assets/hito.css= | GET | Stylesheet (embedded at build time) |
366 Added: | =/assets/workout-client.js= | GET | Enhancement client (embedded at build time) |
367 Added:
368 Added: Slot and record identity live in the path rather than hidden fields.
369 Added:
370 Added: The refusal at =POST /workout= redirects to the overview, which reports the
371 Added: remaining rest and offers an explicit override action. The interface therefore
372 Added: makes the clearance invariant visible instead of training early by accident.
373 Added:
374 Added: ** The workout view
375 Added:
376 Added: One page serves both the workout in progress and a saved record. It shows one
377 Added: prescribed slot at a time under a vertical group of named exercise buttons, each
378 Added: a server-rendered link carrying its slot in =?slot==. The active link is marked
379 Added: =aria-current="page"=. A handler clamps a requested slot against the
380 Added: prescription and otherwise opens on the default: the first slot still awaiting a
381 Added: record, or the first slot when all are filled.
382 Added:
383 Added: This is link navigation and route state, not an ARIA widget — deterministic, and
384 Added: correct with no client script at all.
385 Added:
386 Added: ** Progressive enhancement
387 Added:
388 Added: The =js_of_ocaml= client is an enhancement, never a requirement. Server-rendered
389 Added: HTML remains the only source of UI, and the fallback is the ordinary link/form
390 Added: behaviour the pages already have.
391 Added:
392 Added: The contract is a set of markers the server emits:
393 Added:
394 Added: | Marker | Meaning |
395 Added: |----------------------------+-----------------------------------------------|
396 Added: | =data-hito-app-shell= | the replaceable shell; carries the page title |
397 Added: | =data-hito-app-content= | the page surface inside it |
398 Added: | =data-hito-app-link= | a link eligible for in-place navigation |
399 Added: | =data-hito-app-form= | a form eligible for in-place submission |
400 Added: | =data-hito-workout-*= | the same, for current-workout slots and forms |
401 Added: | =data-hito-workout-status= | an =aria-live= region for announcements |
402 Added:
403 Added: Behaviour: the client fetches the same URL the link or form would have used,
404 Added: extracts the marked region from the response, and swaps it. Successful
405 Added: transitions push the final response URL, so redirects stay reflected in the
406 Added: address bar; server-rendered validation responses render in place *without* a
407 Added: history entry. A monotonic request counter makes the newest interaction win, and
408 Added: =aria-busy= marks the shell while one is pending. Recording a stimulus returns
409 Added: to the submitted slot rather than the server's default, which is the one place
410 Added: the client shapes the flow. Anything it cannot apply — a missing marker, a
411 Added: transport failure, a modified click — falls back to native navigation.
412 Added:
413 Added: The browser holds no domain logic. It never decides whether a set is valid,
414 Added: whether recovery is complete, or whether a correction is volume.
415 Added:
416 Added: * Running it
417 Added:
418 Added: #+begin_src sh
419 Added: dune build && ./_build/default/bin/main.exe # http://localhost:8080/
420 Added: #+end_src
421 Added:
422 Added: =bin/main.ml= opens the store, applies migrations, seeds the single account, and
423 Added: starts Dream. The socket binds *loopback only*.
424 Added:
425 Added: | Variable | Purpose | Default |
426 Added: |----------------------+---------------------------------------+-------------------------|
427 Added: | =HITO_DB= | Caqti database URI | =sqlite3:hito.sqlite= |
428 Added: | =HITO_SECRET= | Signs session cookies and CSRF tokens | random per run |
429 Added: | =HITO_PORT= | TCP port | =8080= |
430 Added: | =HITO_SEED_PASSWORD= | Password for the seeded account | none — refuses to start |
431 Added:
432 Added: Set =HITO_SECRET= in production; unset, sessions do not survive a restart.
433 Added:
434 Added: Dream runs its own SQL pool for sessions against the same file as
435 Added: =Sqlite_repo=. SQLite serializes writers, so this is safe for local use; a
436 Added: separate session store is the path to higher concurrency.
437 Added:
438 Added: * Verification
439 Added:
440 Added: One Alcotest suite per module, =test/test_<module>.ml=, each exposing =suite=,
441 Added: registered in =test/test_hito.ml= in layer order: vocabulary, plan, record,
442 Added: judgment, service, serialization, storage, decoding, web.
443 Added:
444 Added: What the less obvious suites are for:
445 Added:
446 Added: - =test_codec= — a stored workout round-trips faithfully, and malformed or
447 Added: incomplete text is *reported*, not raised.
448 Added: - =test_sqlite_repo= — state survives a reconnect, trainees stay isolated,
449 Added: reapplying migrations is idempotent, and finishing is atomic across a
450 Added: reconnect, against a temporary database file.
451 Added: - =test_decode= — the trust boundary: form values are validated before the core
452 Added: sees them.
453 Added: - =test_web= — carries the session cookie and CSRF token between requests, so
454 Added: authentication, the recovery gate, corrections, and the no-JavaScript
455 Added: behaviour are exercised end to end.
456 Added:
457 Added: Done means, in order: =dune build @check= clean, =dune runtest= passing,
458 Added: =dune fmt= applied with =dune build @fmt= clean, and documentation that matches
459 Added: the change.
460 Added:
461 Added: * Tensions with the source
462 Added: :PROPERTIES:
463 Added: :CUSTOM_ID: tensions
464 Added: :END:
465 Added:
466 Added: Recorded rather than resolved, because HD1 does not settle them.
467 Added:
468 Added: *48h against 72h.* Chapter 3 says up to 72 hours of rest, sometimes more, is
469 Added: needed for growth; the Ideal Routine prescribes training every other day.
470 Added: Mentzer does not reconcile these. We encode the routine — 48h within a cycle,
471 Added: 72h after it — and note the discrepancy here.
472 Added:
473 Added: *Per-exercise rep windows.* HD1 gives one guideline, 6–10, for every listed
474 Added: exercise. We let a prescription name its own window, bounded to 6–12, on the
475 Added: argument that leg work may warrant a different range. A deliberate departure —
476 Added: and note that Mentzer's own rationale for the upper bound, cardiorespiratory
477 Added: failure arriving before muscular failure, cuts against higher reps for large
478 Added: compounds rather than for them.
479 Added:
480 Added: *Extra volume is recordable.* HD1 forbids it in the strongest terms, but a log
481 Added: that refuses to state what happened is worse than one recording an error. The
482 Added: constraint lives on the prescription side, which cannot ask for extra work;
483 Added: performing extra shows up as more stimuli than slots.
484 Added:
485 Added: *Extension rarity is a diagnostic, not an invariant.* Same reason. HD1 says
486 Added: never to extend every exercise of a workout; if you did, the record must say so.
487 Added:
488 Added: *Deadlifts substitute for hyperextensions* across mechanics, because HD1 offers
489 Added: them as alternatives despite one being an isolation and the other a compound.
490 Added:
491 Added: *The log form offers one extension, not a stack.* =Evidence.Stimulus= permits
492 Added: forced reps /then/ negatives, as HD1 describes; the web form currently offers a
493 Added: single choice. A limitation of the form, not the model.
494 Added:
495 Added: *No consolidation routine.* HD2 material, and we have no source for it.
496 Added:
497 Added: * Deferred
498 Added:
499 Added: - =Evidence.Feedback= is modelled and tested but not yet recorded or shown.
500 Added: - =Progression.remedy= is computed but never applied to a routine — the dashed
501 Added: arrow above.
502 Added: - Equipment granularity, so a suggested load is one a bar can actually hold.
503 Added: - A trainee layer carrying individual recovery ability, spotter availability, and
504 Added: the way recovery needs outgrow strength as a trainee gets stronger.
505 Added: - HD2 consolidation, once sourced.
506 Added: - A separate session store, for concurrency beyond local use.
507 Added: - A native client, which would sit on =hito.app= beside the web tier.