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; +}