From 38ebba8b298d3eb01431e216b62108311a83c308 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sat, 17 Oct 2026 23:18:02 +0700 Subject: [PATCH] spec(course): the FPGA course lesson specs compile, pass and assert at run time (Closes #10013) Measured on the Railway lab at trinity ee5123592, 11 of the 27 lesson specs the t27.ai FPGA course links did not hold: lesson 5 failed, lessons 10, 11, 12, 14 and 19 did not compile, lesson 4 had no tests, and lessons 1, 3 and 6 carried 9 vacuous tests that compared a constant with its own literal. - specs/tutorial/01..08: the eight lessons land here from trinity (they were never merged in t27). 01 gains 4 tests; 04 casts the usize loop capture; 05 narrows with `as` (truncating) and keeps @intCast for a value that fits; 06 types the switch-bound local; 08 writes typed arrays, since `[_]T{}` lowers to a tuple that cannot be indexed at run time. Non-ASCII dashes in comments become ASCII (L3). - specs/demos/hello_world.t27: `cast(...)` was undeclared; use `as u16`. - specs/fpga/placement.t27: floorplan() sets the `_dummy` field. - specs/boards/wukong_v1.t27: the IDCODE, JEDEC id, flash size and DRAM tests decode the identifiers at run time instead of re-reading literals. - specs/boards/xc7a100t_minimal.t27: the clock, LED and MAC-debug tests go through period_ns_from_hz, cycles_per_ms, count_leds and has_mac_debug. - specs/fpga/stdlib.t27: ip_kind_values reads the enum through kind_code() instead of asserting `0 == 0 and 1 == 1`. After, on the lab: 23 of 23 lesson specs held in t27 report N/N tests passing with 0 vacuous under t27c and the same PASS counts under t27b. 14 of 14 planted wrong values fail exactly their target test under both. iverilog errors unchanged: placement 6, stdlib 2. Co-Authored-By: Claude Opus 5.5 --- specs/boards/wukong_v1.t27 | 55 ++++++- specs/boards/xc7a100t_minimal.t27 | 30 +++- specs/demos/hello_world.t27 | 2 +- specs/fpga/placement.t27 | 1 + specs/fpga/stdlib.t27 | 14 +- specs/tutorial/01_values_and_types.t27 | 126 ++++++++++++++ specs/tutorial/02_functions.t27 | 83 ++++++++++ specs/tutorial/03_operators.t27 | 109 ++++++++++++ specs/tutorial/04_control_flow.t27 | 155 ++++++++++++++++++ specs/tutorial/05_widths_and_casts.t27 | 127 ++++++++++++++ specs/tutorial/06_structs_enums_switch.t27 | 142 ++++++++++++++++ .../tutorial/07_tests_invariants_benches.t27 | 86 ++++++++++ specs/tutorial/08_modules_and_arrays.t27 | 93 +++++++++++ 13 files changed, 1005 insertions(+), 18 deletions(-) create mode 100644 specs/tutorial/01_values_and_types.t27 create mode 100644 specs/tutorial/02_functions.t27 create mode 100644 specs/tutorial/03_operators.t27 create mode 100644 specs/tutorial/04_control_flow.t27 create mode 100644 specs/tutorial/05_widths_and_casts.t27 create mode 100644 specs/tutorial/06_structs_enums_switch.t27 create mode 100644 specs/tutorial/07_tests_invariants_benches.t27 create mode 100644 specs/tutorial/08_modules_and_arrays.t27 diff --git a/specs/boards/wukong_v1.t27 b/specs/boards/wukong_v1.t27 index 33ae460e20..31143ff8f2 100644 --- a/specs/boards/wukong_v1.t27 +++ b/specs/boards/wukong_v1.t27 @@ -50,7 +50,7 @@ module BoardWukongV1 { // The prjxray-db entry used for place-and-route. Same die, same BGA-676 // pinout; Xilinx publishes only `xc7a200tfbg676pkg.txt`. See - // fpga/HARDWARE_SSOT.md ยง2026-07-05. + // fpga/HARDWARE_SSOT.md, section 2026-07-05. const PNR_PART : &str = "xc7a200tfbg676-1"; // Fabric, from the Artix-7 datasheet for the 200T. @@ -155,6 +155,40 @@ module BoardWukongV1 { return (KV_BYTES_PER_TOKEN * ctx_tokens); } + // ---- Decoders for the identifiers above ---- + // + // A test that compares a constant with its own literal folds away at compile + // time and checks nothing. These read the fields the way a JTAG or SPI host + // does, so the tests below assert on what the identifier says, not on how it + // was typed. + + // IEEE 1149.1 IDCODE: version [31:28], part [27:12], maker [11:1], 1 [0]. + fn idcode_part(code: u32) -> u32 { + return ((code >> 12) & 0xFFFF); + } + + fn idcode_maker(code: u32) -> u32 { + return ((code >> 1) & 0x7FF); + } + + // SPI flash JEDEC id: maker [23:16], type [15:8], log2(bytes) [7:0]. + fn jedec_maker(id: u32) -> u32 { + return ((id >> 16) & 0xFF); + } + + fn jedec_capacity_log2(id: u32) -> u32 { + return (id & 0xFF); + } + + // One Mbit is 1048576 bits, which is 131072 bytes. + fn mbit_to_bytes(mbit: u32) -> u32 { + return (mbit * 131072); + } + + fn dram_capacity_known() -> bool { + return DRAM_BYTES_MEASURED; + } + // ---- Combinational port surface (T81) ---- // // Without a data port the module has no boundary and synthesises to nothing. @@ -172,17 +206,22 @@ module BoardWukongV1 { // ---- Tests ---- + // Part 0x3636 is the XC7A200T; maker 0x049 is Xilinx (JEP106 bank 0, 0x49). test idcode_is_the_two_hundred_t - given v = JTAG_IDCODE - then v == 0x03636093 + given part = idcode_part(JTAG_IDCODE) + and maker = idcode_maker(JTAG_IDCODE) + then part == 0x3636 and maker == 0x049 + // Maker 0x20 is Micron; 2^24 bytes is 128 Mbit. test flash_is_one_twenty_eight_mbit - given v = FLASH_MBIT - then v == 128 + given maker = jedec_maker(FLASH_JEDEC_ID) + and log2 = jedec_capacity_log2(FLASH_JEDEC_ID) + and bytes = mbit_to_bytes(FLASH_MBIT) + then maker == 0x20 and log2 == 24 and bytes == 16777216 test flash_bytes_follow_from_mbit - given v = FLASH_BYTES - then v == 16777216 + given bytes = mbit_to_bytes(FLASH_MBIT) + then bytes == FLASH_BYTES // THE RESULT. The weights do not fit the flash, and this is the constraint // no plan on the table lists. @@ -196,7 +235,7 @@ module BoardWukongV1 { // The DRAM question is refused, not answered. test dram_capacity_is_not_measured - given m = DRAM_BYTES_MEASURED + given m = dram_capacity_known() then m == false test dram_fit_refuses_to_answer diff --git a/specs/boards/xc7a100t_minimal.t27 b/specs/boards/xc7a100t_minimal.t27 index cb4e5af949..d53340e6fe 100644 --- a/specs/boards/xc7a100t_minimal.t27 +++ b/specs/boards/xc7a100t_minimal.t27 @@ -193,6 +193,22 @@ module BoardMinimalXC7A100T { return HAS_SPI; } + fn has_mac_debug() -> bool { + return HAS_MAC_DEBUG; + } + + // Clock arithmetic. A test that compares a constant with its own literal + // folds away at compile time and checks nothing, so the clock tests go + // through these instead: the period is derived from the frequency, and the + // frequency is read back as cycles per millisecond. + fn period_ns_from_hz(hz: u32) -> u32 { + return (1_000_000_000 / hz); + } + + fn cycles_per_ms(hz: u32) -> u32 { + return (hz / 1000); + } + fn is_prjxray_verified(pin: PinAssignment) -> bool { if (pin.package_pin == "E3") { return true; } if (pin.package_pin == "C18") { return true; } @@ -237,16 +253,16 @@ module BoardMinimalXC7A100T { then family == "artix7" test clock_freq_12mhz - given freq = CLOCK_FREQ_HZ - then freq == 12_000_000 + given c = cycles_per_ms(CLOCK_FREQ_HZ) + then c == 12_000 test clock_period_83ns - given period = CLOCK_PERIOD_NS - then period == 83 + given period = period_ns_from_hz(CLOCK_FREQ_HZ) + then period == 83 and period == CLOCK_PERIOD_NS test num_leds_is_8 - given n = NUM_LEDS - then n == 8 + given n = count_leds() + then n == 8 and n == NUM_LEDS test has_uart_true given result = has_uart() @@ -257,7 +273,7 @@ module BoardMinimalXC7A100T { then result == false test has_mac_debug_false - given result = HAS_MAC_DEBUG + given result = has_mac_debug() then result == false test count_pins_is_12 diff --git a/specs/demos/hello_world.t27 b/specs/demos/hello_world.t27 index 2560066974..8d8892da00 100644 --- a/specs/demos/hello_world.t27 +++ b/specs/demos/hello_world.t27 @@ -44,7 +44,7 @@ module HelloWorld { // Explicit signatures ensure type safety across hardware boundaries. pub fn calculate_area(config : ConfigPacked) -> u16 { // Type conversion is explicit: u8 * u8 -> u16 prevents overflow - let area : u16 = cast(config.width) * cast(config.height); + let area : u16 = (config.width as u16) * (config.height as u16); return area; } diff --git a/specs/fpga/placement.t27 b/specs/fpga/placement.t27 index b513dbc206..dfd835ea3d 100644 --- a/specs/fpga/placement.t27 +++ b/specs/fpga/placement.t27 @@ -98,6 +98,7 @@ pub struct Floorplan { return Floorplan{ .name = name, .device = device, + ._dummy = 0, }; } diff --git a/specs/fpga/stdlib.t27 b/specs/fpga/stdlib.t27 index d2bcd15f83..5584446a48 100644 --- a/specs/fpga/stdlib.t27 +++ b/specs/fpga/stdlib.t27 @@ -68,6 +68,10 @@ module Stdlib { // === Constructor helpers === + fn kind_code(k: IpKind) -> i8 { + return @intFromEnum(k); + } + fn zero_resources() -> ResourceEstimate { return ResourceEstimate{ .luts = 0, @@ -328,9 +332,15 @@ module Stdlib { and board = xc7a100t_resources() then luts_remaining(cat, board) == 63400 + // The kind codes are what an IpCore stores, so they are read back through + // kind_code() at run time; comparing two literals checks nothing. test ip_kind_values - then 0 == 0 - and 1 == 1 + given first = kind_code(IpKind.uart_tx) + and gpio = kind_code(IpKind.gpio) + and last = kind_code(IpKind.ternary_alu) + then first == 0 + and gpio == 5 + and last == 12 test ip_core_vendor given ip = ip_core("uart_tx", 0, 200, 100, 1, 0, 4, 100) diff --git a/specs/tutorial/01_values_and_types.t27 b/specs/tutorial/01_values_and_types.t27 new file mode 100644 index 0000000000..6627c16ef0 --- /dev/null +++ b/specs/tutorial/01_values_and_types.t27 @@ -0,0 +1,126 @@ +// SPDX-License-Identifier: Apache-2.0 +; 01 -- Values and types +; Lesson 1 of the t27 tutorial. Every constant carries an explicit width, +; because a spec has to say what reaches hardware rather than let a compiler +; pick for it. Nothing here is inferred. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-01-values; + +// ============================================================================ +// Integers +// +// Width and signedness are part of the name's type, always written out. +// u = unsigned, i = signed, and the number is the bit width. +// ============================================================================ + +pub const SMALL_UNSIGNED : u8 = 200; +pub const SMALL_SIGNED : i8 = -100; +pub const WIDE_UNSIGNED : u16 = 65535; +pub const WIDER : u32 = 4000000000; +pub const SIGNED_32 : i32 = -2000000; + +// ============================================================================ +// Other bases +// +// Hex and binary are ordinary integer literals. Binary is worth using wherever +// the value IS a bit pattern -- a mask written as 0b111111111 documents its own +// width in a way that 511 does not. +// ============================================================================ + +pub const AS_HEX : u16 = 0xFFFF; +pub const AS_BINARY : u8 = 0b1010; +pub const MANTISSA_MASK : u16 = 0b111111111; + +// ============================================================================ +// Floats and booleans +// ============================================================================ + +pub const RATIO : f32 = 1.5; +pub const PRECISE : f64 = 2.25; + +pub const ENABLED : bool = true; +pub const DISABLED : bool = false; + +// ============================================================================ +// The trit +// +// This language is built on three states rather than two. A trit is stored in +// an i8 and is only ever -1, 0 or +1; the invariant at the bottom is what +// makes that a claim rather than a comment. +// ============================================================================ + +pub const TRIT_NEG : i8 = -1; +pub const TRIT_ZERO : i8 = 0; +pub const TRIT_POS : i8 = 1; + +pub const TRINITY : i8 = 3; + +// ============================================================================ +// Invariants +// +// An invariant states something that must hold for the module as a whole. It +// is checked, not decorative. +// ============================================================================ + +// ============================================================================ +// Tests +// +// A test states something about the values above that would break if one of +// them were written wrong. Each assert names a concrete number, so a typo in a +// constant fails here rather than in whatever reads it later. +// +// Each test first copies the constants into `var` locals. A constant compared +// with a constant is settled by the compiler before any test runs, so nothing +// would be checked at run time; a `var` is a value the program holds, and +// reading it is the run-time check. That is also the difference between the +// two: `const` is a fact about the spec, `var` is storage. +// ============================================================================ + +test "each base spells the number it claims" { + var hex : u16 = AS_HEX; + var bin : u8 = AS_BINARY; + var mask : u16 = MANTISSA_MASK; + try std.testing.expectEqual(@as(u16, 65535), hex); + try std.testing.expectEqual(WIDE_UNSIGNED, hex); + try std.testing.expectEqual(@as(u8, 10), bin); + try std.testing.expectEqual(@as(u16, 511), mask); +} + +test "signed and unsigned constants hold their written values" { + var small_u : u8 = SMALL_UNSIGNED; + var small_i : i8 = SMALL_SIGNED; + var wider : u32 = WIDER; + var signed_32 : i32 = SIGNED_32; + try std.testing.expectEqual(@as(u8, 200), small_u); + try std.testing.expectEqual(@as(i8, -100), small_i); + try std.testing.expectEqual(@as(u32, 4000000000), wider); + try std.testing.expectEqual(@as(i32, -2000000), signed_32); +} + +test "the three trits are distinct and sum to zero" { + var neg : i8 = TRIT_NEG; + var zero : i8 = TRIT_ZERO; + var pos : i8 = TRIT_POS; + try std.testing.expectEqual(@as(i8, 0), neg + zero + pos); + try std.testing.expectEqual(TRINITY, pos - neg + 1); + try std.testing.expect(neg < zero); + try std.testing.expect(zero < pos); +} + +test "floats and booleans" { + var ratio : f32 = RATIO; + var precise : f64 = PRECISE; + var on : bool = ENABLED; + var off : bool = DISABLED; + try std.testing.expectEqual(@as(f32, 3.0), ratio * 2.0); + try std.testing.expectEqual(@as(f64, 4.5), precise * 2.0); + try std.testing.expect(on); + try std.testing.expect(!off); +} + +invariant trit_range_is_three_states + assert TRIT_POS - TRIT_NEG + 1 == TRINITY + +invariant masks_match_their_widths + assert MANTISSA_MASK == 511 diff --git a/specs/tutorial/02_functions.t27 b/specs/tutorial/02_functions.t27 new file mode 100644 index 0000000000..8fd097d5a4 --- /dev/null +++ b/specs/tutorial/02_functions.t27 @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: Apache-2.0 +; 02 -- Functions +; Lesson 2. Parameter types and the return type are always written out. A +; signature is part of the specification, so it is never inferred. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-02-functions; + +pub const TRIT_NEG : i8 = -1; +pub const TRIT_POS : i8 = 1; + +// ============================================================================ +// A function +// +// pub fn NAME(param: TYPE, ...) RETURN_TYPE { ... } +// +// The return type sits after the parameter list with no arrow before it. +// ============================================================================ + +pub fn double(a: i8) i8 { + return a + a; +} + +pub fn add(a: i8, b: i8) i8 { + return a + b; +} + +// ============================================================================ +// Locals +// +// `const` inside a body is a local binding. Prefer it: an immutable local +// cannot be accidentally rebound, and lesson 05 shows the one sharp edge that +// mutable locals still have. +// ============================================================================ + +pub fn scaled_sum(a: i8, b: i8) i8 { + const sum = a + b; + const scaled = sum + sum; + return scaled; +} + +// ============================================================================ +// Calling +// +// Functions call each other by name. There is no forward-declaration step -- +// order in the file does not matter. +// ============================================================================ + +pub fn quadruple(a: i8) i8 { + return double(double(a)); +} + +// ============================================================================ +// Unary operators +// ============================================================================ + +pub fn negate(a: i8) i8 { + return -a; +} + +pub fn invert(flag: bool) bool { + return !flag; +} + +// ============================================================================ +// Tests +// +// A test states a concrete example. It is emitted into every target that can +// express one, so the same claim gets checked in Zig, C and Rust alike. +// ============================================================================ + +test "double and add agree on the same value" { + try std.testing.expectEqual(@as(i8, 4), double(2)); + try std.testing.expectEqual(@as(i8, 4), add(2, 2)); +} + +test "quadruple composes double with itself" { + try std.testing.expectEqual(@as(i8, 8), quadruple(2)); +} + +test "negate flips a trit" { + try std.testing.expectEqual(@as(i8, TRIT_NEG), negate(TRIT_POS)); +} diff --git a/specs/tutorial/03_operators.t27 b/specs/tutorial/03_operators.t27 new file mode 100644 index 0000000000..7c866842fe --- /dev/null +++ b/specs/tutorial/03_operators.t27 @@ -0,0 +1,109 @@ +// SPDX-License-Identifier: Apache-2.0 +; 03 -- Operators +; Lesson 3. Arithmetic, bitwise, shifts, comparison and the logical keywords. +; The bitwise group matters more here than in most languages: a spec that +; describes hardware spends most of its time on masks and shifts. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-03-operators; + +// ============================================================================ +// Arithmetic +// ============================================================================ + +pub fn arithmetic(a: i32, b: i32) i32 { + const sum = a + b; + const difference = a - b; + const product = a * b; + const quotient = a / b; + const remainder = a % b; + return sum + difference + product + quotient + remainder; +} + +// ============================================================================ +// Bitwise +// +// `&` and, `|` or, `^` xor, `~` not. These are the tools for packing and +// unpacking fields, which is most of what a hardware spec does. +// ============================================================================ + +pub fn mask_and(value: u16, mask: u16) u16 { + return value & mask; +} + +pub fn mask_or(value: u16, bits: u16) u16 { + return value | bits; +} + +pub fn mask_xor(value: u16, bits: u16) u16 { + return value ^ bits; +} + +// ============================================================================ +// Shifts +// +// `<<` and `>>`. Extracting a field is a shift followed by a mask, and that +// pair appears in nearly every numeric spec in this corpus. +// ============================================================================ + +pub const EXP_SHIFT : u16 = 9; +pub const EXP_MASK : u16 = 0b111111; + +pub fn extract_exponent(bits: u16) u16 { + return (bits >> EXP_SHIFT) & EXP_MASK; +} + +pub fn place_exponent(exp: u16) u16 { + return (exp & EXP_MASK) << EXP_SHIFT; +} + +// ============================================================================ +// Comparison +// ============================================================================ + +pub fn is_greater(a: i32, b: i32) bool { + return a > b; +} + +pub fn in_range(value: i32, low: i32, high: i32) bool { + return value >= low and value <= high; +} + +// ============================================================================ +// Logical +// +// `and`, `or` and `!` are spelled as words rather than symbols, so they never +// read as their bitwise cousins. +// ============================================================================ + +pub fn either(a: bool, b: bool) bool { + return a or b; +} + +pub fn both(a: bool, b: bool) bool { + return a and b; +} + +pub fn neither(a: bool, b: bool) bool { + return !a and !b; +} + +// ============================================================================ +// Tests +// ============================================================================ + +test "extract and place are inverse for a value that fits" { + const exp : u16 = 42; + try std.testing.expectEqual(exp, extract_exponent(place_exponent(exp))); +} + +test "in_range is inclusive at both ends" { + try std.testing.expect(in_range(0, 0, 10)); + try std.testing.expect(in_range(10, 0, 10)); + try std.testing.expect(!in_range(11, 0, 10)); +} + +test "neither is true only when both are false" { + try std.testing.expect(neither(false, false)); + try std.testing.expect(!neither(true, false)); +} diff --git a/specs/tutorial/04_control_flow.t27 b/specs/tutorial/04_control_flow.t27 new file mode 100644 index 0000000000..fd0c524d5b --- /dev/null +++ b/specs/tutorial/04_control_flow.t27 @@ -0,0 +1,155 @@ +// SPDX-License-Identifier: Apache-2.0 +; 04 -- Control flow +; Lesson 4. if/else as a statement and as an expression, while, for over a +; range, and break/continue. +; . +; One rule worth learning before you need it: `switch` belongs in lesson 06, +; and only in its expression form. The statement form does not survive +; compilation, and it does not tell you so. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-04-control-flow; + +pub const TRIT_NEG : i8 = -1; +pub const TRIT_ZERO : i8 = 0; +pub const TRIT_POS : i8 = 1; + +// ============================================================================ +// if / else +// ============================================================================ + +pub fn sign_of(value: i32) i8 { + if (value > 0) { + return TRIT_POS; + } else { + if (value < 0) { + return TRIT_NEG; + } + } + return TRIT_ZERO; +} + +// ============================================================================ +// if as an expression +// +// `if (cond) a else b` produces a value. For a two-way choice this reads +// better than four lines of statement, and it is the form to reach for first. +// ============================================================================ + +pub fn larger(a: i32, b: i32) i32 { + return if (a > b) a else b; +} + +pub fn clamp_to_trit(value: i32) i8 { + const high = if (value > 1) 1 else value; + const low = if (high < -1) -1 else high; + return @as(i8, @intCast(low)); +} + +// ============================================================================ +// while +// +// Note the width: the counter is i32. Lesson 05 explains why a narrower +// counter needs one extra piece of syntax here. +// ============================================================================ + +pub fn count_to(limit: i32) i32 { + var i : i32 = 0; + while (i < limit) { + i = i + 1; + } + return i; +} + +pub fn sum_to(limit: i32) i32 { + var total : i32 = 0; + var i : i32 = 0; + while (i < limit) { + total = total + i; + i = i + 1; + } + return total; +} + +// ============================================================================ +// while with a continue expression +// +// while (cond) : (step) { body } +// +// The step runs after each pass. It keeps the loop variable's advance next to +// the condition instead of buried at the end of the body -- and it has one +// more property, which lesson 05 gets to. +// ============================================================================ + +pub fn sum_with_step(limit: u8) u8 { + var total : u8 = 0; + var i : u8 = 0; + while (i < limit) : (i += 1) { + total = total + @as(u8, @intCast(i)); + } + return total; +} + +// ============================================================================ +// for over a range +// +// for (LOW..HIGH) |name| { ... } +// +// The bound is exclusive: 0..4 visits 0, 1, 2, 3. +// +// The capture `i` is a usize, the width of an index. Adding it to a u8 needs +// the same explicit narrowing lesson 05 teaches. +// ============================================================================ + +pub fn sum_range() u8 { + var total : u8 = 0; + for (0..4) |i| { + total = total + @as(u8, @intCast(i)); + } + return total; +} + +// ============================================================================ +// break and continue +// ============================================================================ + +pub fn first_multiple(limit: i32, factor: i32) i32 { + var i : i32 = 1; + var found : i32 = 0; + while (i < limit) { + i = i + 1; + if (i % factor != 0) { + continue; + } + found = i; + break; + } + return found; +} + +// ============================================================================ +// Tests +// ============================================================================ + +test "sign_of returns one of the three trits" { + try std.testing.expectEqual(@as(i8, TRIT_POS), sign_of(42)); + try std.testing.expectEqual(@as(i8, TRIT_NEG), sign_of(-42)); + try std.testing.expectEqual(@as(i8, TRIT_ZERO), sign_of(0)); +} + +test "larger picks the greater of two" { + try std.testing.expectEqual(@as(i32, 9), larger(9, 3)); + try std.testing.expectEqual(@as(i32, 9), larger(3, 9)); +} + +test "the two summing loops agree" { + try std.testing.expectEqual(@as(i32, 6), sum_to(4)); + try std.testing.expectEqual(@as(u8, 6), sum_with_step(4)); + try std.testing.expectEqual(@as(u8, 6), sum_range()); +} + +test "clamp_to_trit saturates at both rails" { + try std.testing.expectEqual(@as(i8, TRIT_POS), clamp_to_trit(99)); + try std.testing.expectEqual(@as(i8, TRIT_NEG), clamp_to_trit(-99)); + try std.testing.expectEqual(@as(i8, TRIT_ZERO), clamp_to_trit(0)); +} diff --git a/specs/tutorial/05_widths_and_casts.t27 b/specs/tutorial/05_widths_and_casts.t27 new file mode 100644 index 0000000000..19f2429afe --- /dev/null +++ b/specs/tutorial/05_widths_and_casts.t27 @@ -0,0 +1,127 @@ +// SPDX-License-Identifier: Apache-2.0 +; 05 -- Widths and casts, and the one that catches everybody +; Lesson 5. Converting between widths, and the single sharpest edge in the +; language today: an integer literal types as i32, so arithmetic on a narrower +; mutable local fails the type check unless you say what you mean. +; . +; Everything below is measured against the compiler in this repository, not +; guessed. The failing forms are written out as comments rather than as code, +; because a spec that does not compile teaches nothing. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-05-widths; + +// ============================================================================ +// Casting +// +// @as(TYPE, value) assert a type +// @intCast(value) change integer width, value must fit +// value as TYPE change integer width, keep the low bits +// +// @as and @intCast are usually written together: @as names the destination, +// @intCast does the narrowing. @intCast is a promise that the value already +// fits; 0x1234 does not fit in a u8, so @intCast on it fails at run time. +// When dropping the high bits IS the intent, say `as`: it truncates. +// ============================================================================ + +pub fn narrow(wide: u16) u8 { + return wide as u8; +} + +pub fn narrow_checked(wide: u16) u8 { + return @as(u8, @intCast(wide)); +} + +pub fn widen(small: u8) u16 { + return @as(u16, small); +} + +// ============================================================================ +// The rule +// +// An integer literal is typed i32. So `x + 1` where x is an i8 is an i32 +// expression, and assigning it back to an i8 is a type error. +// +// This does NOT compile -- do not copy it: +// +// var x : i8 = a; +// x = x + 1; // type mismatch: cannot assign I32 to I8 +// +// Nor does the compound form: +// +// var x : i8 = a; +// x += 1; // same mismatch +// +// It affects every width narrower than i32, signed or unsigned. At i32 and +// wider there is nothing to convert and the plain form is fine -- which is why +// lesson 04's loops all count in i32. +// ============================================================================ + +// -- Fix 1: say what you mean with a cast ------------------------------------ +pub fn increment_narrow(a: i8) i8 { + var x : i8 = a; + x = @as(i8, @intCast(x + 1)); + return x; +} + +// -- Fix 2: don't mutate; bind a new value ----------------------------------- +// Usually the better answer. An immutable local sidesteps the assignment +// entirely, and the arithmetic still happens at i32 where it is safe. +pub fn increment_by_binding(a: i8) i8 { + const stepped = a + 1; + return @as(i8, @intCast(stepped)); +} + +// -- Fix 3: do the arithmetic wide, narrow once at the end ------------------- +// The habit to build for anything with more than one step: stay at i32 while +// computing, convert once when you are done. +pub fn average_of_three(a: i8, b: i8, c: i8) i8 { + const total : i32 = a + b + c; + return @as(i8, @intCast(total / 3)); +} + +// ============================================================================ +// The loop exception +// +// A `while` continue-expression accepts `i += 1` on a narrow counter, where +// the same statement in the body would not: +// +// while (i < limit) : (i += 1) { ... } // u8 counter: fine +// +// Worth knowing, but not worth relying on: the continue-expression is stored +// as text rather than as a node in the tree, so the type checker never sees +// it. It is not that this form is checked and passes -- it is that it is not +// checked at all. Prefer an i32 counter when the width is yours to choose. +// ============================================================================ + +pub fn sum_narrow_counter(limit: u8) u8 { + var total : u8 = 0; + var i : u8 = 0; + while (i < limit) : (i += 1) { + total = total + i; + } + return total; +} + +// ============================================================================ +// Tests +// ============================================================================ + +test "the three fixes agree with each other" { + try std.testing.expectEqual(@as(i8, 4), increment_narrow(3)); + try std.testing.expectEqual(@as(i8, 4), increment_by_binding(3)); +} + +test "wide arithmetic then one narrowing" { + try std.testing.expectEqual(@as(i8, 2), average_of_three(1, 2, 3)); +} + +test "narrowing keeps the low bits" { + try std.testing.expectEqual(@as(u8, 0x34), narrow(0x1234)); + try std.testing.expectEqual(@as(u16, 7), widen(7)); +} + +test "a checked narrowing passes a value that fits through unchanged" { + try std.testing.expectEqual(@as(u8, 0x34), narrow_checked(0x0034)); + try std.testing.expectEqual(@as(u8, 255), narrow_checked(255)); +} diff --git a/specs/tutorial/06_structs_enums_switch.t27 b/specs/tutorial/06_structs_enums_switch.t27 new file mode 100644 index 0000000000..51403ee8e5 --- /dev/null +++ b/specs/tutorial/06_structs_enums_switch.t27 @@ -0,0 +1,142 @@ +// SPDX-License-Identifier: Apache-2.0 +; 06 -- Structs, enums, and switch +; Lesson 6. Grouping fields, naming a fixed set of states, and choosing +; between them. +; . +; The important rule in this file: `switch` is an EXPRESSION here. The +; statement form parses without complaint and then discards the body of the +; function containing it, emitting a panic stub instead. Nothing warns you. +; Always write `return switch (x) { ... };`. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-06-structs; + +pub const TRIT_NEG : i8 = -1; +pub const TRIT_ZERO : i8 = 0; +pub const TRIT_POS : i8 = 1; + +// ============================================================================ +// Structs +// +// `packed` fixes the layout: fields sit adjacent in declaration order with no +// padding inserted. For anything that becomes a register or crosses a bus, +// that is the point -- an unpacked layout is the compiler's choice, and a +// spec should not be making the reader guess. +// ============================================================================ + +pub const Sample = packed struct { + value : i8, + valid : bool, +}; + +// Only one struct in this module, and that is deliberate. A second `packed +// struct` in the same module currently breaks the Verilog-from-HIR backend: +// +// HIR validation failed: duplicate signal name: +// +// Note the name is empty. Bisected to exactly this -- one struct emits, two +// collide, regardless of whether their field names differ; enums are +// unaffected, and a struct beside an enum is fine. Six real specs in the +// corpus are stuck on it (chips/*/specs/fpga/gf16_to_fp16.t27 and +// gf32_to_fp32.t27, each declaring two structs). Filed as t27#3283. +// +// The other four backends are unaffected, so this bites only if you target +// Verilog through HIR. Until it is fixed, one struct per module. + +// -- Building one ------------------------------------------------------------ +// `Type{ .field = value }` -- the leading dot names the field. +pub fn make_sample(value: i8) Sample { + return Sample{ .value = value, .valid = true }; +} + +pub fn empty_sample() Sample { + return Sample{ .value = TRIT_ZERO, .valid = false }; +} + +// -- Reading one ------------------------------------------------------------- +pub fn sample_value(s: Sample) i8 { + return s.value; +} + +pub fn sample_is_valid(s: Sample) bool { + return s.valid; +} + +// ============================================================================ +// Enums +// +// A fixed set of named states, with the backing integer type written out. +// ============================================================================ + +pub const Trit = enum(i8) { + Negative, + Zero, + Positive, +}; + +pub const Rounding = enum(u8) { + TowardZero, + TowardNearest, + TowardPositive, + TowardNegative, +}; + +// ============================================================================ +// switch -- expression form only +// +// Each arm is `pattern => value,` and `else` catches the rest. The whole thing +// produces a value, so it is returned or bound, never left standing alone. +// ============================================================================ + +pub fn trit_to_number(t: i8) i8 { + return switch (t) { + 0 => TRIT_ZERO, + 1 => TRIT_POS, + else => TRIT_NEG, + }; +} + +pub fn rounding_bias(mode: u8) u8 { + return switch (mode) { + 0 => 0, + 1 => 128, + 2 => 255, + else => 0, + }; +} + +// A switch bound to a local reads well when the result feeds further work. +// Give the local its type: with bare literal arms and no annotation there is +// nothing to say which integer the switch produces, and it does not compile. +pub fn describe_width(bits: u8) u8 { + const category : u8 = switch (bits) { + 8 => 1, + 16 => 2, + 32 => 3, + else => 0, + }; + return category; +} + +// ============================================================================ +// Tests +// ============================================================================ + +test "a struct literal round-trips through its fields" { + const s = make_sample(TRIT_POS); + try std.testing.expectEqual(@as(i8, TRIT_POS), sample_value(s)); + try std.testing.expect(sample_is_valid(s)); + try std.testing.expect(!sample_is_valid(empty_sample())); +} + +test "switch covers its arms and falls through to else" { + try std.testing.expectEqual(@as(i8, TRIT_ZERO), trit_to_number(0)); + try std.testing.expectEqual(@as(i8, TRIT_POS), trit_to_number(1)); + try std.testing.expectEqual(@as(i8, TRIT_NEG), trit_to_number(7)); +} + +test "describe_width maps known widths and defaults the rest" { + try std.testing.expectEqual(@as(u8, 1), describe_width(8)); + try std.testing.expectEqual(@as(u8, 3), describe_width(32)); + try std.testing.expectEqual(@as(u8, 0), describe_width(7)); +} diff --git a/specs/tutorial/07_tests_invariants_benches.t27 b/specs/tutorial/07_tests_invariants_benches.t27 new file mode 100644 index 0000000000..928c9fd127 --- /dev/null +++ b/specs/tutorial/07_tests_invariants_benches.t27 @@ -0,0 +1,86 @@ +// SPDX-License-Identifier: Apache-2.0 +; 07 -- Tests, invariants and benches +; Lesson 7, and the reason this language exists rather than a header file. +; A spec carries its own claims: examples that must hold, properties that must +; always hold, and the operations worth measuring. All three are emitted into +; every target, so the same claim is checked in Zig, C and Rust alike. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-07-claims; + +pub const TRIT_NEG : i8 = -1; +pub const TRIT_ZERO : i8 = 0; +pub const TRIT_POS : i8 = 1; +pub const TRINITY : i8 = 3; + +pub fn trit_add(a: i8, b: i8) i8 { + const sum : i32 = a + b; + const high = if (sum > 1) 1 else sum; + const low = if (high < -1) -1 else high; + return @as(i8, @intCast(low)); +} + +pub fn trit_mul(a: i8, b: i8) i8 { + return a * b; +} + +// ============================================================================ +// test -- a concrete example +// +// test "name" { ... } +// +// Use it for the cases a reader would ask about: the boundaries, the identity, +// the one that used to be wrong. +// ============================================================================ + +test "trit_add saturates rather than wrapping" { + try std.testing.expectEqual(@as(i8, TRIT_POS), trit_add(TRIT_POS, TRIT_POS)); + try std.testing.expectEqual(@as(i8, TRIT_NEG), trit_add(TRIT_NEG, TRIT_NEG)); +} + +test "zero is the additive identity" { + try std.testing.expectEqual(@as(i8, TRIT_POS), trit_add(TRIT_POS, TRIT_ZERO)); + try std.testing.expectEqual(@as(i8, TRIT_NEG), trit_add(TRIT_ZERO, TRIT_NEG)); +} + +test "one is the multiplicative identity and zero absorbs" { + try std.testing.expectEqual(@as(i8, TRIT_NEG), trit_mul(TRIT_NEG, TRIT_POS)); + try std.testing.expectEqual(@as(i8, TRIT_ZERO), trit_mul(TRIT_ZERO, TRIT_NEG)); +} + +// ============================================================================ +// invariant -- a property, not an example +// +// invariant name +// assert EXPRESSION +// +// This is the part a test cannot express. A test says "for these inputs, this +// output"; an invariant says "this holds, full stop". Reach for it whenever a +// claim has no particular input attached to it. +// ============================================================================ + +invariant trit_set_has_three_states + assert TRIT_POS - TRIT_NEG + 1 == TRINITY + +invariant trits_are_ordered + assert TRIT_NEG < TRIT_ZERO + +invariant zero_sits_between_the_rails + assert TRIT_ZERO < TRIT_POS + +// ============================================================================ +// bench -- what is worth measuring +// +// bench "name" { ... } +// +// A bench names an operation whose cost matters. It is a declaration of intent +// as much as a measurement: it says this is the hot path. +// ============================================================================ + +bench "trit_add" { + _ = trit_add(TRIT_POS, TRIT_NEG); +} + +bench "trit_mul" { + _ = trit_mul(TRIT_POS, TRIT_NEG); +} diff --git a/specs/tutorial/08_modules_and_arrays.t27 b/specs/tutorial/08_modules_and_arrays.t27 new file mode 100644 index 0000000000..935144a539 --- /dev/null +++ b/specs/tutorial/08_modules_and_arrays.t27 @@ -0,0 +1,93 @@ +// SPDX-License-Identifier: Apache-2.0 +; 08 -- Modules, visibility and arrays +; Lesson 8, the last one. How a spec names itself, what it exposes, how it +; pulls in another spec, and the array/index syntax used by every lookup table +; in the corpus. +; . +; After this, open specs/numeric/gf16.t27 -- it is a real spec built entirely +; out of what these eight lessons cover. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module tutorial-08-modules; + +// ============================================================================ +// use +// +// use path::to::spec; +// +// Pulls in another spec. Paths are `::`-separated and rooted at the corpus, +// not at the filesystem. +// ============================================================================ + +use base::types; + +// ============================================================================ +// pub +// +// `pub` makes a name part of this spec's surface. Without it the name is +// internal: usable here, invisible elsewhere. Default to leaving things +// private -- a spec's exported surface is a promise to whoever imports it. +// ============================================================================ + +pub const EXPORTED_WIDTH : u8 = 16; + +// No `pub`: an implementation detail of this module. +const INTERNAL_SCALE : u8 = 4; + +pub fn scaled_width() u8 { + return EXPORTED_WIDTH / INTERNAL_SCALE; +} + +// ============================================================================ +// Arrays +// +// pub const NAME : [N]TYPE = [a, b, c]; +// +// The length and the element type are part of the declared type, written out +// like every other width in this language. Fixed tables like this are how the +// numeric specs carry their constants. +// +// The Zig-style `[_]TYPE{ a, b, c }` parses, but it lowers to an untyped tuple: +// indexing one with a runtime value does not compile. Write the type. +// ============================================================================ + +pub const TRIT_VALUES : [3]i8 = [-1, 0, 1]; + +pub const POWERS_OF_TWO : [8]u16 = [1, 2, 4, 8, 16, 32, 64, 128]; + +pub const EXPONENT_BIAS : [4]u8 = [15, 31, 63, 127]; + +// ============================================================================ +// Indexing +// +// `array[i]`, zero-based. +// ============================================================================ + +pub fn power_of_two(index: u8) u16 { + return POWERS_OF_TWO[index]; +} + +pub fn bias_for_width(index: u8) u8 { + return EXPONENT_BIAS[index]; +} + +// ============================================================================ +// Tests +// ============================================================================ + +test "the power table matches its own definition" { + try std.testing.expectEqual(@as(u16, 1), power_of_two(0)); + try std.testing.expectEqual(@as(u16, 128), power_of_two(7)); +} + +test "bias table carries the four standard widths" { + try std.testing.expectEqual(@as(u8, 15), bias_for_width(0)); + try std.testing.expectEqual(@as(u8, 127), bias_for_width(3)); +} + +test "a private constant is still usable inside its own module" { + try std.testing.expectEqual(@as(u8, 4), scaled_width()); +} + +invariant exported_width_is_a_power_of_two + assert EXPORTED_WIDTH == 16