Skip to content

fix(specs): make 36 specs compile under the current t27 compiler #99

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gHashTag merged 1 commit into from
Sep 24, 2026
Merged

fix(specs): make 36 specs compile under the current t27 compiler #99

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
211 changes: 109 additions & 102 deletions specs/fpga/avs_controller_48.t27
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,14 @@ pub const AvsStatus = struct {
fault_code : u8,
}

// Named form of the anonymous `struct { opcode, level, reserved }` that
// decode_avs_48_cmd returns (same fields, same types).
pub const Avs48Cmd = struct {
opcode : u8,
level : u8,
reserved : u8,
}

pub const AvsConfig = struct {
mode : AvsMode,
min_mv : u16,
Expand Down Expand Up @@ -131,7 +139,7 @@ pub fn avs_voltage_in_hysteresis(current_mv: u16, target_mv: u16, hysteresis_mv:
// avs_should_adjust(current_mv: u16, target_mv: u16, hysteresis_mv: u16) -> bool
// Check if voltage should be adjusted
pub fn avs_should_adjust(current_mv: u16, target_mv: u16, hysteresis_mv: u16) -> bool {
return not avs_voltage_in_hysteresis(current_mv, target_mv, hysteresis_mv);
return !avs_voltage_in_hysteresis(current_mv, target_mv, hysteresis_mv);
}

// ============================================================================
Expand Down Expand Up @@ -284,7 +292,7 @@ pub fn avs_control_pin_for_bit(bit_index: u8) -> u8 {

// encode_avs_48_cmd(opcode: u8, level: u8, reserved: u8) -> u16
// Encode AVS 48-pin command
pub fn encode_avs_48_cmd(opcode: u8, level: u8, reserved: u8) u16 {
pub fn encode_avs_48_cmd(opcode: u8, level: u8, reserved: u8) -> u16 {
// Format: [OP:8][LEVEL:6][RES:2]
const op_field : u16 = @as(u16, opcode) << 8;
const level_field : u16 = @as(u16, level & 0x3F) << 2;
Expand All @@ -294,224 +302,223 @@ pub fn encode_avs_48_cmd(opcode: u8, level: u8, reserved: u8) u16 {

// decode_avs_48_cmd(encoded: u16) -> struct { opcode: u8, level: u8, reserved: u8 }
// Decode AVS 48-pin command
pub fn decode_avs_48_cmd(encoded: u16) -> struct { opcode: u8, level: u8, reserved: u8 } {
pub fn decode_avs_48_cmd(encoded: u16) -> Avs48Cmd {
const opcode : u8 = @as(u8, @truncate((encoded >> 8) & 0xFF));
const level : u8 = @as(u8, @truncate((encoded >> 2) & 0x3F));
const reserved : u8 = @as(u8, @truncate(encoded & 0x03));
return .{ .opcode = opcode, .level = level, .reserved = reserved };
return Avs48Cmd{ .opcode = opcode, .level = level, .reserved = reserved };
}

// ============================================================================
// TDD Tests
// ============================================================================

test "pins_48_constant" {
try std.testing.expect(PINS_48 == 48);
assert(PINS_48 == 48);
}

test "voltage_constants" {
try std.testing.expect(VOLTAGE_MIN_MV == 800);
try std.testing.expect(VOLTAGE_MAX_MV == 1200);
try std.testing.expect(VOLTAGE_STEP_MV == 10);
try std.testing.expect(VOLTAGE_LEVELS == 41);
assert(VOLTAGE_MIN_MV == 800);
assert(VOLTAGE_MAX_MV == 1200);
assert(VOLTAGE_STEP_MV == 10);
assert(VOLTAGE_LEVELS == 41);
}

test "target_voltage_constant" {
try std.testing.expect(TARGET_MV == 1000);
assert(TARGET_MV == 1000);
}

test "control_pin_constants" {
try std.testing.expect(CONTROL_PIN_OFFSET == 16);
try std.testing.expect(CONTROL_PIN_COUNT == 6);
assert(CONTROL_PIN_OFFSET == 16);
assert(CONTROL_PIN_COUNT == 6);
}

test "avs_voltage_from_level_zero" {
try std.testing.expect(avs_voltage_from_level(0) == VOLTAGE_MIN_MV);
assert(avs_voltage_from_level(0) == VOLTAGE_MIN_MV);
}

test "avs_voltage_from_level_max" {
given max_level = VOLTAGE_LEVELS - 1
try std.testing.expect(avs_voltage_from_level(max_level) == VOLTAGE_MAX_MV);
const max_level = VOLTAGE_LEVELS - 1;
assert(avs_voltage_from_level(max_level) == VOLTAGE_MAX_MV);
}

test "avs_voltage_from_level_target" {
given level = avs_level_from_voltage(TARGET_MV)
try std.testing.expect(avs_voltage_from_level(level) == TARGET_MV);
const level = avs_level_from_voltage(TARGET_MV);
assert(avs_voltage_from_level(level) == TARGET_MV);
}

test "avs_level_from_voltage_min" {
try std.testing.expect(avs_level_from_voltage(VOLTAGE_MIN_MV) == 0);
assert(avs_level_from_voltage(VOLTAGE_MIN_MV) == 0);
}

test "avs_level_from_voltage_max" {
try std.testing.expect(avs_level_from_voltage(VOLTAGE_MAX_MV) == VOLTAGE_LEVELS - 1);
assert(avs_level_from_voltage(VOLTAGE_MAX_MV) == VOLTAGE_LEVELS - 1);
}

test "avs_level_from_voltage_clamp_low" {
try std.testing.expect(avs_level_from_voltage(700) == 0);
assert(avs_level_from_voltage(700) == 0);
}

test "avs_level_from_voltage_clamp_high" {
try std.testing.expect(avs_level_from_voltage(1500) == VOLTAGE_LEVELS - 1);
assert(avs_level_from_voltage(1500) == VOLTAGE_LEVELS - 1);
}

test "avs_control_code_from_level_zero" {
try std.testing.expect(avs_control_code_from_level(0) == 0);
assert(avs_control_code_from_level(0) == 0);
}

test "avs_control_code_from_level_max" {
given code = avs_control_code_from_level(63)
try std.testing.expect(code == 63);
const code = avs_control_code_from_level(63);
assert(code == 63);
}

test "avs_control_code_from_level_clamp" {
given code = avs_control_code_from_level(100)
try std.testing.expect(code == 36 // 100 & 0x3F);
const code = avs_control_code_from_level(100);
assert(code == 36); // 100 & 0x3F
}

test "avs_level_from_control_code_roundtrip" {
given level = 20
try std.testing.expect(code = avs_control_code_from_level(level));
try std.testing.expect(decoded = avs_level_from_control_code(code));
try std.testing.expect(decoded == level);
const level = 20;
const code = avs_control_code_from_level(level);
const decoded = avs_level_from_control_code(code);
assert(decoded == level);
}

test "avs_voltage_valid_in_range" {
try std.testing.expect(avs_voltage_valid(900) == true);
try std.testing.expect(avs_voltage_valid(1000) == true);
try std.testing.expect(avs_voltage_valid(1100) == true);
assert(avs_voltage_valid(900) == true);
assert(avs_voltage_valid(1000) == true);
assert(avs_voltage_valid(1100) == true);
}

test "avs_voltage_valid_out_of_range" {
try std.testing.expect(avs_voltage_valid(700) == false);
try std.testing.expect(avs_voltage_valid(1300) == false);
assert(avs_voltage_valid(700) == false);
assert(avs_voltage_valid(1300) == false);
}

test "avs_voltage_in_hysteresis_true" {
try std.testing.expect(avs_voltage_in_hysteresis(1000, 1000, 20) == true);
try std.testing.expect(avs_voltage_in_hysteresis(1015, 1000, 20) == true);
try std.testing.expect(avs_voltage_in_hysteresis(985, 1000, 20) == true);
assert(avs_voltage_in_hysteresis(1000, 1000, 20) == true);
assert(avs_voltage_in_hysteresis(1015, 1000, 20) == true);
assert(avs_voltage_in_hysteresis(985, 1000, 20) == true);
}

test "avs_voltage_in_hysteresis_false" {
try std.testing.expect(avs_voltage_in_hysteresis(1050, 1000, 20) == false);
try std.testing.expect(avs_voltage_in_hysteresis(950, 1000, 20) == false);
assert(avs_voltage_in_hysteresis(1050, 1000, 20) == false);
assert(avs_voltage_in_hysteresis(950, 1000, 20) == false);
}

test "avs_should_adjust_false_in_hysteresis" {
try std.testing.expect(avs_should_adjust(1010, 1000, 20) == false);
assert(avs_should_adjust(1010, 1000, 20) == false);
}

test "avs_should_adjust_true_out_of_hysteresis" {
try std.testing.expect(avs_should_adjust(1050, 1000, 20) == true);
assert(avs_should_adjust(1050, 1000, 20) == true);
}

test "avs_config_init_structure" {
given config = avs_config_init()
try std.testing.expect(config.mode == AvsMode.automatic);
try std.testing.expect(config.target_mv == TARGET_MV);
try std.testing.expect(config.hysteresis_mv == HYSTERESIS_MV);
const config = avs_config_init();
assert(config.mode == AvsMode.automatic);
assert(config.target_mv == TARGET_MV);
assert(config.hysteresis_mv == HYSTERESIS_MV);
}

test "avs_config_manual_structure" {
given config = avs_config_manual(900)
try std.testing.expect(config.mode == AvsMode.manual);
try std.testing.expect(config.target_mv == 900);
const config = avs_config_manual(900);
assert(config.mode == AvsMode.manual);
assert(config.target_mv == 900);
}

test "avs_config_adaptive_structure" {
given config = avs_config_adaptive(850, 1150)
try std.testing.expect(config.mode == AvsMode.adaptive);
try std.testing.expect(config.min_mv == 850);
try std.testing.expect(config.max_mv == 1150);
const config = avs_config_adaptive(850, 1150);
assert(config.mode == AvsMode.adaptive);
assert(config.min_mv == 850);
assert(config.max_mv == 1150);
}

test "avs_status_init_structure" {
given status = avs_status_init()
try std.testing.expect(status.state == AvsState.disabled);
try std.testing.expect(status.current_mv == VOLTAGE_MIN_MV);
const status = avs_status_init();
assert(status.state == AvsState.disabled);
assert(status.current_mv == VOLTAGE_MIN_MV);
}

test "avs_status_enable" {
given status = avs_status_init()
try std.testing.expect(config = avs_config_init());
try std.testing.expect(result = avs_status_enable(status, config));
try std.testing.expect(result.state == AvsState.enabled);
try std.testing.expect(result.mode == AvsMode.automatic);
const status = avs_status_init();
const config = avs_config_init();
const result = avs_status_enable(status, config);
assert(result.state == AvsState.enabled);
assert(result.mode == AvsMode.automatic);
}

test "avs_status_adjust" {
given status = avs_status_init()
try std.testing.expect(result = avs_status_adjust(status, 10));
try std.testing.expect(result.state == AvsState.adjusting);
try std.testing.expect(result.level == 10);
const status = avs_status_init();
const result = avs_status_adjust(status, 10);
assert(result.state == AvsState.adjusting);
assert(result.level == 10);
}

test "avs_status_settled" {
given status = avs_status_init()
try std.testing.expect(result = avs_status_settled(status, 1000));
try std.testing.expect(result.state == AvsState.settled);
try std.testing.expect(result.current_mv == 1000);
const status = avs_status_init();
const result = avs_status_settled(status, 1000);
assert(result.state == AvsState.settled);
assert(result.current_mv == 1000);
}

test "avs_status_fault" {
given status = avs_status_init()
try std.testing.expect(result = avs_status_fault(status, 1));
try std.testing.expect(result.state == AvsState.fault);
try std.testing.expect(result.fault_code == 1);
const status = avs_status_init();
const result = avs_status_fault(status, 1);
assert(result.state == AvsState.fault);
assert(result.fault_code == 1);
}

test "avs_control_pins_start" {
try std.testing.expect(avs_control_pins_start() == CONTROL_PIN_OFFSET);
assert(avs_control_pins_start() == CONTROL_PIN_OFFSET);
}

test "avs_control_pins_end" {
try std.testing.expect(avs_control_pins_end() == CONTROL_PIN_OFFSET + CONTROL_PIN_COUNT - 1);
assert(avs_control_pins_end() == CONTROL_PIN_OFFSET + CONTROL_PIN_COUNT - 1);
}

test "avs_is_control_pin_true" {
try std.testing.expect(avs_is_control_pin(16) == true);
try std.testing.expect(avs_is_control_pin(21) == true);
assert(avs_is_control_pin(16) == true);
assert(avs_is_control_pin(21) == true);
}

test "avs_is_control_pin_false" {
try std.testing.expect(avs_is_control_pin(15) == false);
try std.testing.expect(avs_is_control_pin(22) == false);
assert(avs_is_control_pin(15) == false);
assert(avs_is_control_pin(22) == false);
}

test "avs_control_pin_for_bit" {
try std.testing.expect(avs_control_pin_for_bit(0) == CONTROL_PIN_OFFSET);
try std.testing.expect(avs_control_pin_for_bit(5) == CONTROL_PIN_OFFSET + 5);
assert(avs_control_pin_for_bit(0) == CONTROL_PIN_OFFSET);
assert(avs_control_pin_for_bit(5) == CONTROL_PIN_OFFSET + 5);
}

test "avs_control_pin_for_bit_clamp" {
try std.testing.expect(avs_control_pin_for_bit(10) == CONTROL_PIN_OFFSET);
assert(avs_control_pin_for_bit(10) == CONTROL_PIN_OFFSET);
}

test "encode_avs_48_cmd" {
given encoded = encode_avs_48_cmd(0x10, 20, 0)
try std.testing.expect((encoded >> 8) == 0x10);
const encoded = encode_avs_48_cmd(0x10, 20, 0);
assert((encoded >> 8) == 0x10);
}

test "decode_avs_48_cmd" {
given decoded = decode_avs_48_cmd(0x1050)
try std.testing.expect(decoded.opcode == 0x10);
try std.testing.expect(decoded.level == 20);
const decoded = decode_avs_48_cmd(0x1050);
assert(decoded.opcode == 0x10);
assert(decoded.level == 20);
}

// ============================================================================
// Invariants
// ============================================================================

}
invariant voltage_range_positive
assert VOLTAGE_MIN_MV > 0 and VOLTAGE_MAX_MV > VOLTAGE_MIN_MV

invariant voltage_step_positive
assert VOLTAGE_STEP_MV > 0

invariant voltage_levels_calculated
try std.testing.expect(VOLTAGE_LEVELS == ((VOLTAGE_MAX_MV - VOLTAGE_MIN_MV) / VOLTAGE_STEP_MV) + 1);
assert VOLTAGE_LEVELS == ((VOLTAGE_MAX_MV - VOLTAGE_MIN_MV) / VOLTAGE_STEP_MV) + 1

invariant target_voltage_in_range
assert avs_voltage_valid(TARGET_MV)
Expand All @@ -527,36 +534,36 @@ invariant control_pin_count_six

invariant avs_voltage_from_level_roundtrip
given level = 15
try std.testing.expect(voltage = avs_voltage_from_level(level));
try std.testing.expect(result_level = avs_level_from_voltage(voltage));
try std.testing.expect(result_level == level);
and voltage = avs_voltage_from_level(level)
and result_level = avs_level_from_voltage(voltage)
then result_level == level

invariant avs_voltage_in_hysteresis_exact
try std.testing.expect(avs_voltage_in_hysteresis(TARGET_MV, TARGET_MV, 0) == true);
assert avs_voltage_in_hysteresis(TARGET_MV, TARGET_MV, 0) == true

invariant avs_should_adjust_false_at_exact_target
try std.testing.expect(avs_should_adjust(TARGET_MV, TARGET_MV, HYSTERESIS_MV) == false);
assert avs_should_adjust(TARGET_MV, TARGET_MV, HYSTERESIS_MV) == false

invariant avs_status_init_disabled
given status = avs_status_init()
try std.testing.expect(status.state == AvsState.disabled);
then status.state == AvsState.disabled

invariant avs_status_enable_sets_mode
given status = avs_status_init()
try std.testing.expect(config = avs_config_manual(950));
try std.testing.expect(result = avs_status_enable(status, config));
try std.testing.expect(result.mode == AvsMode.manual);
and config = avs_config_manual(950)
and result = avs_status_enable(status, config)
then result.mode == AvsMode.manual

invariant avs_status_adjust_changes_level
given status = avs_status_init()
try std.testing.expect(result = avs_status_adjust(status, 25));
try std.testing.expect(result.level == 25);
and result = avs_status_adjust(status, 25)
then result.level == 25

invariant avs_is_control_pin_monotonic
try std.testing.expect(avs_control_pin_for_bit(3) > avs_control_pin_for_bit(2));
assert avs_control_pin_for_bit(3) > avs_control_pin_for_bit(2)

invariant avs_control_pin_for_bit_start_at_offset
try std.testing.expect(avs_control_pin_for_bit(0) == CONTROL_PIN_OFFSET);
assert avs_control_pin_for_bit(0) == CONTROL_PIN_OFFSET

// ============================================================================
// Benchmarks
Expand Down
Loading