From 775580d463e27e0df0246cc2ceacf75e512ab3d0 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sat, 17 Oct 2026 22:40:31 +0700 Subject: [PATCH] spec(t27f): first real reel -- the t27 basics course as a 27-cell map (Closes #9996) specs/t27f/reel_t27_basics.t27 draws one real topic with the reel camera and the deck look: the 27 lessons of gHashTag/trinity's t27 basics course, in order, one reel row per three course modules. A cell's status is earned from two measurements (lesson page live on t27.ai, lesson spec passes on the lab), and the slide text of all five demo scenes is checked against deck.t27 for every preset. Runs under both t27c and t27b with the same verdict on every test. t27b refused the first draft for comparing a str's u64 .len with an i32; lengths are cast now. Refs gHashTag/trinity#1677 Co-Authored-By: Claude Opus 5.5 --- specs/t27f/reel_t27_basics.t27 | 264 +++++++++++++++++++++++++++++++++ 1 file changed, 264 insertions(+) create mode 100644 specs/t27f/reel_t27_basics.t27 diff --git a/specs/t27f/reel_t27_basics.t27 b/specs/t27f/reel_t27_basics.t27 new file mode 100644 index 0000000000..afdde8ac51 --- /dev/null +++ b/specs/t27f/reel_t27_basics.t27 @@ -0,0 +1,264 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/t27f/reel_t27_basics.t27 -- the first real T27F reel: course 0, "t27 basics", 27 lessons. +; trinity#1677 (Topic-to-Value Engine) asks for a 27-step map that is source-grounded, with gaps shown +; instead of filler. This file is that map for one real topic, drawn with the reel camera +; (specs/t27f/reel.t27) and the deck look (specs/t27f/deck.t27). + +; SOURCE: gHashTag/trinity apps/website/specs/course/t27-basics.t27 at commit SOURCE_COMMIT. Its 27 +; lessons, in order, are the 27 cells; nothing here is new teaching text. The slide rows quote or +; shorten that file's lesson 11 text and task, its SAY_PRIVATE line, and courses.t27's order. + +; LENSES: the reel draws one row per lens, nine cells per row. The course has 9 modules of 3 lessons, +; so each row is three whole modules: lessons 1-9 (a spec file, values and types, arrays and trits), +; 10-18 (tests and functions, inside a function, your own types), 19-27 (modules and rules, the +; compiler and tri, errors and what next). The test lenses_are_whole_modules holds that. + +; STATUS is measured, not chosen. On 2026-10-17: +; - page: GET https://t27.ai/learn// returned 200 with the title ": t27 basics +; course, lesson N of 27" for all 27; a made-up id returned 404, so 200 is not a catch-all. +; - spec: t27c test-report on the Railway lab passed every test of all 27 lesson specs +; (apps/website/public/t27/files/specs/basics/*.t27 at SOURCE_COMMIT). 23 of them report their +; passes as vacuous because every assert is on constants and is checked when compiled; planting +; a wrong one (lesson 11, HOURS == 25) turned that test red, so the checks are real. +; A cell is PUBLISHED only when both hold, VERIFIED when only the spec passes, DRAFT otherwise. + +; SCENES: the t27f_view host draws the reel.t27 demo camera (overview, lens 0, focus on cell 10, +; evidence, call), so this reel uses that camera; the test the_camera_is_the_demo_camera holds it. +; The slide text below is checked against deck.t27 for every preset, so the host never has to +; refuse it as "does not fit one slide". + +; TWO COMPILERS: this file, reel.t27 and deck.t27 run under t27c (the Zig backend) and under t27b +; (t27's own AArch64 backend, `t27b test --check`, qemu-aarch64 on the lab). On 2026-10-17 the two +; agreed on every test (6 + 20 + 15 pass), and each planted fault above failed the same test in both. +; t27b also refused the first draft of this file: it compared a str's u64 `.len` with an i32, which +; t27c accepted; every length is now cast to i32 before it is compared. + +; Not claimed: no GIF or MP4 is rendered or posted; stills only, for the chat. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module reel_t27_basics; + +use t27f::reel::CELL_COUNT; +use t27f::reel::COLS; +use t27f::reel::DEMO_COUNT; +use t27f::reel::DEMO_KIND; +use t27f::reel::DEMO_CELL; +use t27f::reel::DEMO_LENS; +use t27f::reel::PRESET_COUNT; +use t27f::reel::STYLE_PUBLISHED; +use t27f::reel::cell_row; +use t27f::reel::cell_style; +use t27f::deck::LAYOUT_SPLIT; +use t27f::deck::LAYOUT_STAGE; +use t27f::deck::REGION_TITLE; +use t27f::deck::HEADLINE_PX; +use t27f::deck::BODY_PX; +use t27f::deck::HEADLINE_EM_PERMILLE; +use t27f::deck::BODY_EM_PERMILLE; +use t27f::deck::MAX_ROWS; +use t27f::deck::layout_for; +use t27f::deck::text_fits; +use t27f::deck::chars_per_line; +use t27f::deck::card_inner_w; +use t27f::deck::region_w; + +pub const TOPIC_ID : str = "t27-basics"; +pub const SOURCE_REPO : str = "gHashTag/trinity"; +pub const SOURCE_SPEC : str = "apps/website/specs/course/t27-basics.t27"; +pub const SOURCE_COMMIT : str = "ee512359254bcd7438bb6a79c8a4a7f8b554b620"; +pub const LESSON_PAGE_BASE : str = "https://t27.ai/learn/"; +pub const MEASURED_ON : str = "2026-10-17"; + +pub const LESSONS_PER_MODULE : i32 = 3; +pub const MODULES_PER_LENS : i32 = 3; + +/// Lesson statuses, the T27fTopicEngine codes reel.t27 reads. +pub const STATUS_DRAFT : u8 = 3; +pub const STATUS_VERIFIED : u8 = 4; +pub const STATUS_PUBLISHED : u8 = 5; + +/// The two measurements per lesson, in lesson order (see the header for how each was taken). +pub const PAGE_LIVE : [27]bool = [true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true]; +pub const SPEC_PASSES : [27]bool = [true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true, true]; + +/// What a host passes the viewer, per cell: the status code and the lesson number as a label. +pub const STATUS : [27]u8 = [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]; +pub const LABELS : [27]str = ["1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15", "16", "17", "18", "19", "20", "21", "22", "23", "24", "25", "26", "27"]; + +pub const LENS_TITLES : [3]str = ["values", "logic", "tools"]; + +/// Slide text per demo scene. HEAD is the headline, one line: a stage strip holds one line on the wide +/// and square presets, and the host wraps a title greedily by words, so a headline that fits one line +/// on every preset is the only kind the host draws the same everywhere. ROWS holds four card rows per +/// scene (index scene*4+row; an empty row is no row), each short enough never to wrap. +pub const HEAD : [5]str = [ + "t27 basics: 27 lessons", + "Lessons 1-9: values", + "Many small tests", + "Evidence", + "Start lesson 1" +]; +pub const ROWS : [20]str = [ + "", "", "", "", + "", "", "", "", + "Lesson 11 of 27: one test, one idea", + "A test's name says which idea broke", + "The lesson spec: 3 tests, 5 asserts", + "Try: break one, the other two still pass", + "27 of 27 lesson pages live on t27.ai", + "27 of 27 lesson specs pass on the lab", + "A planted wrong assert turns it red", + "Measured 2026-10-17", + "t27.ai/learn/what-a-spec-is/", + "Progress stays in this browser", + "Next: the FPGA course", + "" +]; + +pub fn lesson_number(cell: i32) -> i32 { + return cell + 1; +} + +pub fn module_of(cell: i32) -> i32 { + return @divTrunc(cell, LESSONS_PER_MODULE); +} + +/// The status a cell has earned from its two measurements. +pub fn measured_status(cell: i32) -> u8 { + const live : bool = PAGE_LIVE[@intCast(cell)]; + const pass : bool = SPEC_PASSES[@intCast(cell)]; + if (live and pass) { + return STATUS_PUBLISHED; + } + if (pass) { + return STATUS_VERIFIED; + } + return STATUS_DRAFT; +} + +pub fn count_true(xs: [27]bool) -> i32 { + var n : i32 = 0; + var c : i32 = 0; + while (c < CELL_COUNT) { + if (xs[@intCast(c)]) { + n = n + 1; + } + c = c + 1; + } + return n; +} + +pub fn row_count(scene: i32) -> i32 { + var n : i32 = 0; + var j : i32 = 0; + while (j < MAX_ROWS) { + if (ROWS[@intCast(scene * 4 + j)].len > 0) { + n = n + 1; + } + j = j + 1; + } + return n; +} + +/// Characters a headline line may hold on this scene's slide, as the host breaks it. +pub fn head_chars(layout: u8, preset: u8) -> i32 { + if (layout == LAYOUT_SPLIT) { + return chars_per_line(card_inner_w(preset), HEADLINE_PX[preset], HEADLINE_EM_PERMILLE); + } + return chars_per_line(region_w(layout, preset, REGION_TITLE), HEADLINE_PX[preset], HEADLINE_EM_PERMILLE); +} + +pub fn row_chars(preset: u8) -> i32 { + return chars_per_line(card_inner_w(preset), BODY_PX[preset], BODY_EM_PERMILLE); +} + +test every_lesson_is_a_cell { + assert CELL_COUNT == 27; + assert lesson_number(0) == 1; + assert lesson_number(CELL_COUNT - 1) == 27; + assert LABELS[0].len == 1; + assert LABELS[26].len == 2; + var c : i32 = 0; + while (c < CELL_COUNT) { + const n : i32 = lesson_number(c); + var want : i32 = 1; + if (n >= 10) { + want = 2; + } + const len : i32 = @intCast(LABELS[@intCast(c)].len); + assert len == want; + c = c + 1; + } +} + +test lenses_are_whole_modules { + assert COLS == LESSONS_PER_MODULE * MODULES_PER_LENS; + var c : i32 = 0; + while (c < CELL_COUNT) { + // the row a cell is drawn in is the lens of its module: three whole modules per row + assert cell_row(c) == @divTrunc(module_of(c), MODULES_PER_LENS); + c = c + 1; + } + assert LENS_TITLES[2].len > 0; +} + +test a_status_is_earned_not_chosen { + var c : i32 = 0; + while (c < CELL_COUNT) { + assert STATUS[@intCast(c)] == measured_status(c); + c = c + 1; + } + assert count_true(PAGE_LIVE) == 27; + assert count_true(SPEC_PASSES) == 27; + // a published cell wears the published style, never a gap or a draft + assert cell_style(STATUS[0]) == STYLE_PUBLISHED; +} + +test the_camera_is_the_demo_camera { + assert DEMO_COUNT == 5; + // scene 1 shows lens 0, the row HEAD[1] calls "Lessons 1-9" + assert DEMO_LENS[1] == 0; + // scenes 2 and 3 focus cell 10, which the focus slide calls "Lesson 11" + assert DEMO_CELL[2] == 10; + assert DEMO_CELL[3] == 10; + assert lesson_number(DEMO_CELL[2]) == 11; +} + +test every_slide_fits_every_preset { + var s : i32 = 0; + while (s < DEMO_COUNT) { + const layout : u8 = layout_for(DEMO_KIND[@intCast(s)]); + assert HEAD[@intCast(s)].len > 0; + var p : u8 = 0; + while (p < PRESET_COUNT) { + // one headline line that the host never breaks, and rows it never breaks either + assert text_fits(1, row_count(s), layout, p); + const head_len : i32 = @intCast(HEAD[@intCast(s)].len); + assert head_len <= head_chars(layout, p); + var j : i32 = 0; + while (j < MAX_ROWS) { + const row_len : i32 = @intCast(ROWS[@intCast(s * 4 + j)].len); + assert row_len <= row_chars(p); + j = j + 1; + } + p = p + 1; + } + s = s + 1; + } +} + +test stage_slides_carry_no_card_text { + // why HEAD is one line: on the wide frame a second stage line would not fit the strip + assert text_fits(2, 0, LAYOUT_STAGE, 0) == false; + var s : i32 = 0; + while (s < DEMO_COUNT) { + if (layout_for(DEMO_KIND[@intCast(s)]) == LAYOUT_STAGE) { + assert row_count(s) == 0; + } + s = s + 1; + } +} + +invariant one_lens_per_row { + assert CELL_COUNT == 3 * COLS; +}