spec: Add initial tooling to check data formats, prepare for more elaborate type checking

[RobinJadoul]

I've included some various fixed for minor issues encountered while checking the current spec files here, because they felt too minor to make a bunch of separate PRs for.

[RobinJadoul]

Still a couple open-ish questions, and a few things to improve, but I think we're at a good point to do a full review and maybe split off the remaining work (signature checking, "constant" columns (for PAGE), better casting checks) for later PRs

[greptile-apps]

Greptile Overview

Greptile Summary

This PR introduces a Python-based type checking tool (chip.py) for validating the TOML specification files and fixes various data format inconsistencies discovered during development.

Key changes:

• New type checker: Added spec/tooling/chip.py, a comprehensive type checking tool that validates TOML spec files with range-based type checking for expressions, virtual column definitions, and constraints
• Type system enhancement: Extended config.toml with explicit range definitions for all basic types (Bit, Byte, Half, Word, etc.) to enable proper type checking; removed unused B35 type
• Data format corrections: Fixed multiple inconsistencies across spec files:
  • Changed precomputed fields from string "true" to boolean true throughout
  • Corrected multiplicity formats from strings like "-μ" to proper array syntax ["-", "μ"]
  • Fixed string literals to numeric literals where appropriate (e.g., "0" → 0 in mul.toml)
  • Changed multiplicity to cond for template constraints in memw.toml and shift.toml
• Type corrections: Fixed several type mismatches:
  • Changed offset type from Word to DWordWL in branch.toml
  • Added explicit casts for literals being added to typed arrays (e.g., timestamp + 0 → timestamp + ["cast", 0, "DWordWL"])
  • Fixed cast placement in multiplication expressions to avoid casting arrays to more limbs
• Constraint fixes:
  • Added missing multiplicity = 1 fields for several IS_BYTE interaction constraints
  • Fixed indexing issues (e.g., unmasked_low_byte no longer incorrectly indexed)
  • Split overly broad iterator ranges into separate constraints with proper multiplicities in memw.toml
  • Changed not operator to explicit subtraction ["-", 1, X] for consistency
• Minor cleanups: Removed commented-out debug code, added missing newlines at EOF, added TODO note about IS_BYTE constraints for fini

Confidence Score: 5/5

• This PR is safe to merge - it introduces tooling for better validation and fixes data format issues
• All changes are quality improvements that add type checking capability and fix format inconsistencies. The new type checker is well-structured with proper error handling. The TOML fixes correct genuine issues (boolean vs string, proper array syntax, type mismatches) that would be caught by the new tooling. No logical changes to the actual specification, only format corrections.
• No files require special attention

Important Files Changed

Filename	Overview
spec/src/branch.toml	Fixed type from Word to DWordWL for offset, corrected indexing for unmasked_low_byte, fixed multiplicity format
spec/src/config.toml	Added range definitions for type checking, removed unused B35 type, removed erroneous count field
spec/src/cpu.toml	Added missing multiplicity fields, fixed cast operations for type checking, corrected subtraction syntax
spec/src/memw.toml	Changed multiplicity to cond for template constraints, split single constraint into three with proper iterator ranges
spec/tooling/chip.py	New type checking tool that validates TOML spec files with range-based type checking

Sequence Diagram

sequenceDiagram
    participant User
    participant chip.py
    participant Config
    participant Chip
    participant TypeChecker
    participant Environment

    User->>chip.py: Run with config.toml + spec files
    chip.py->>Config: Load config.toml
    Config->>Config: Parse type definitions with ranges
    Config-->>chip.py: Return type system
    
    loop For each spec file
        chip.py->>Chip: Load spec TOML file
        Chip->>Chip: Parse variables (input, output, virtual)
        Chip->>Chip: Parse constraints (arith, template, interaction)
        Chip-->>chip.py: Return chip specification
    end
    
    loop For each chip
        chip.py->>Chip: typecheck()
        Chip->>Environment: Create with typemap
        
        loop For each virtual variable
            Chip->>TypeChecker: typecheck virtual definition
            TypeChecker->>TypeChecker: Check iterator ranges
            TypeChecker->>TypeChecker: Verify coverage of all indices
            TypeChecker->>TypeChecker: Validate expression types
            TypeChecker-->>Chip: Return type or error
        end
        
        loop For each constraint
            Chip->>TypeChecker: typecheck constraint
            TypeChecker->>TypeChecker: Expand iterators
            TypeChecker->>TypeChecker: Check expression types match
            TypeChecker->>TypeChecker: Validate ranges
            TypeChecker-->>Chip: Return signatures or error
        end
        
        Chip-->>chip.py: Return type signatures
    end
    
    chip.py->>User: Report errors or success

Loading

[erik-3milabs]

I propose we additionally test that either

1. the range of base == range of type, or
2. base is a literal.

[RobinJadoul]

Doesn't work, due to things like one-hot assumptions

[erik-3milabs]

Got an example?

[RobinJadoul]

If you're e.g. computing b * x + (1 - b) * y for some bit b and (say) DWordBLs x and y, the range goes outside Byte range, so casting to DWordWL would fail; because we can't see into the b and 1 - b being mutually exclusive
The situation only gets worse if you get things like (1 - STORE - LOAD) * x + (1 - BLT - BEQ) * y or similar things in the CPU

[erik-3milabs]

I'm leaving this open for easy retrieval if we wish to continue this discussion later.

[erik-3milabs]

Got an example?