RISC-V Semantics Commit Change Analysis

[Stevengre]

This section provides a detailed analysis of 62 commits in the RISC-V Semantics project, spanning 4 months (March-June 2025) from version v0.1.51 to v0.1.112 (specifically, from commit 082c5f9 to 42176ce). Among these 62 commits, 36 commits (58%) were authored by JianHong Zhao, with the remaining 26 commits contributed by team members Tamás Tóth, Julian Kuners, and automated dependency updates. This analysis is crucial because REVM verification relies on compiling REVM to RISC-V, which in turn requires formal verification-ready RISC-V semantics.

These commits collectively enable formal verification of real-world REVM code compiled to RISC-V, addressing the significant challenge that even simple Rust programs become complex when compiled through ZK toolchains to RISC-V, let alone production REVM implementations with their intricate state management and cryptographic operations.

Major Improvement Directions for Formal Verification

These 62 commits systematically transform RISC-V Semantics into a production-ready formal verification platform through four key improvement directions:

1. Architecture Foundations for Verification

Core Infrastructure for Reliable Formal Verification

• Migration from Poetry to UV package manager (faster, more reliable builds)
  • v0.1.96: [Commit 711f12b] - "Migrate from poetry to uv"
  • v0.1.100: [Commit fb931c8] - "fix version of uv in CI"
  • v0.1.99: [Commit c77e2a5] - "Fix version in uv.lock"
  • v0.1.102: [Commit 0d09047] - "Update dependency: deps/k_release"
• Extensible prover architecture enabling pluggable verification backends
  • v0.1.101: [Commit fca8f9f] - "Add extensible prover implementation"
• ELF file handling consolidation for better program analysis
  • v0.1.86: [Commit 25b7057] - "Consolidate ELF file handling under class ELF"
• Build system and infrastructure improvements
  • v0.1.95: [Commit 07180df] - "Remove attribute source_dir from SymTools"
  • v0.1.89: [Commit d411af1] - "Write temporary test data into separate folders by default"
  • v0.1.88: [Commit 759923e] - "Inline the <test> cell"

2. Python Toolchain Enhancements

Enhanced Development and Verification Tools

• kriscv-asm command for test case generation and debugging
  • v0.1.57: [Commit 76f893a] - "Add command kriscv-asm <instruction>"
• Enhanced symbolic execution tools with configuration management
  • v0.1.90: [Commit cba2d2b] - "Enable instantiating symbolic config"
  • v0.1.104: [Commit db011d7] - "Add optimize_kcfg parameter in SymTool"
  • v0.1.93: [Commit c2d312e] - "Add property proof_show to SymTools"
  • v0.1.68: [Commit 85e3216] - "Add option --depth to kriscv run"
  • v0.1.59: [Commit 74dc542] - "Allow --temp-dir option for test-prove"
• Enhanced debugging capabilities with bug report integration
  • v0.1.58: [Commit 1e43e19] - "Enhance SymTools with bug report integration"
• CI/CD improvements for reliable verification workflows
  • v0.1.55: [Commit 0526095] - "Add job for notifying dependents"
• Runtime and tool organization
  • v0.1.53: [Commit 344cc7e] - "Factor out runtime from Tools"
  • v0.1.51: [Commit 79552f6] - "Add option --zero-init"

3. RISC-V Semantics Completeness & Optimization for Formal Verification

Complete RISC-V Instruction Set Coverage & Semantic Optimizations

• Division operation implementation (DIV/DIVU) for complete arithmetic support
  • v0.1.111: [Commit efe1f78] - "Add division operations for RISC-V semantics"
• MUL instruction family implementation* for M-extension coverage
  • v0.1.52: [Commit b8bf5d2] - "Implement MUL* instructions"
• Type system refactoring (Word → Int) for simplified formal reasoning
  • v0.1.91: [Commit f680218] - "Refactor RISC-V semantics to replace Word with Int"
  • v0.1.71: [Commit 883fd6e] - "Remove the format attribute from Word"
  • v0.1.73: [Commit 0c40c65] - "Make Word shift operations total"
  • v0.1.74: [Commit 8090120] - "Avoid ambiguity for Word expressions"
• Sparse bytes support for efficient memory modeling in verification
  • v0.1.62: [Commit c6b16ef] - "Support symbolic sparse bytes generation via SparseBytes"
• Symbolic execution foundation for formal property checking
  • v0.1.54: [Commit ae15f5d] - "Add symbolic execution support"
• Memory operation improvements (loadBytes/storeBytes) for precise modeling
  • v0.1.70: [Commit ec95dd6] - "Better loadBytes for symbolic execution"
  • v0.1.69: [Commit 3a2bbc0] - "Better storeBytes for symbolic execution"
  • v0.1.60: [Commit 98eea27] - "Add symbolic execution rules for readByteBF in sparse-bytes.md"
  • v0.1.61: [Commit 2755c4c] - "Add writeByteBF simplification rules"
• Branch handling refactoring for cleaner control flow semantics
  • v0.1.87: [Commit 202c19a] - "Transform function branchPC to effect function #PC_BRANCH"
• Function interface improvements
  • v0.1.112: [Commit 42176ce] - "Move the memory to the end in functions"

4. Simplification Rules for Symbolic Execution Acceleration

40+ Optimization Rules for Faster Constraint Solving

• Byte operation simplifications (comprehensive rule set)
  • v0.1.110: [Commit ddf2811] - "Simp rule 4 int2bytes o bytes2int"
  • v0.1.109: [Commit 940f257] - "Remove redundant requirement for substr o int2bytes"
  • v0.1.106: [Commit 471d05f] - "Refine simp rule for Bytes2Int o Int2Byes"
  • v0.1.105: [Commit 3804716] - "Add simplification rule for Bytes2Int &Int 4294967295"
  • v0.1.98: [Commit 570e0f4] - "Add simp rules for revsersed substrBytes concat"
  • v0.1.97: [Commit 2fc0603] - "Add simp rules 4 Bytes2Int o Int2Bytes and substrBytes o Int2Bytes"
  • v0.1.85: [Commit bb2934c] - "Add simp rules for Int2Bytes o Bytes2Int"
  • v0.1.84: [Commit 4c53805] - "Add simp rules for Bytes2Int o |Int o Bytes2Int"
  • v0.1.83: [Commit 803850d] - "simplify patterns Bytes2Int o <<Int & Bytes2Int o >>Int & chop"
  • v0.1.82: [Commit c157326] - "Add simp rules for replaceAtBytes"
  • v0.1.81: [Commit e2369f6] - "Add simp rules for substrBytes(A +Bytes B, I, J)"
  • v0.1.78: [Commit 66ddeca] - "Simplify pattern Bytes2Int o substrBytes &Int 65280"
  • v0.1.63: [Commit 8f5e5b7] - "Add Byte simplification rules from evm semantics"
• Integer arithmetic optimizations for faster constraint solving
  • v0.1.108: [Commit f5738c0] - "Simp rulle 4 >> 0"
  • v0.1.107: [Commit 123a234] - "Simp rule 4 complex (X + Y & 4294967295) + Z & 4294967295"
  • v0.1.103: [Commit c72b80f] - "Simp rule 4 (A +Int B) &Int 4294967295 <Int A"
  • v0.1.94: [Commit cf4108d] - "Add simp rules 4 &Int assoc"
  • v0.1.77: [Commit 79bf2fd] - "Add simp rule to eliminate SignExtend"
  • v0.1.75: [Commit 72ad19b] - "Add simp rule for <<Int o <<Int"
• Sparse bytes and memory optimizations
  • v0.1.76: [Commit 4dcaa6f] - "Tackle unexpected pattern for pickfront and dropfront"
  • v0.1.72: [Commit 58d1958] - "Add new lemmas for substrBytes and update pickFront rule"
  • v0.1.67: [Commit 60f10e1] - "Add simplification rule for storing symbolic bytes"
• Dependency updates for latest optimizations
  • v0.1.92: [Commit 0949ca5] - "Update dependency: deps/k_release"
  • v0.1.80, v0.1.79: [Commits a5b98f5, 81d5723] - "Update dependency: deps/k_release"
  • v0.1.66, v0.1.65, v0.1.64: [Commits 778e705, 53567c0, 951e6e7] - "Update dependency: deps/k_release"
  • v0.1.56: [Commit 9f4184e] - "Update dependency: deps/k_release"

---

Detailed Commit Analysis

Latest Commits (June 2025)

1. Commit 42176ce (v0.1.112) - "Move the memory to the end in functions"

• Purpose: Adjust function parameter order, moving memory parameter to the end
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/riscv.md - Updated instruction semantics to use new parameter order for memory operations, affecting load/store instructions and their interaction with memory
  • src/kriscv/kdist/riscv-semantics/sparse-bytes.md - Refactored sparse bytes operations to consistently place memory parameter at the end, improving API consistency across all memory manipulation functions
  • src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md - Updated simplification rules to match new parameter ordering for functions like pickFront, dropFront, writeBytesBF, ensuring all lemmas work with the new function signatures
  • src/kriscv/term_builder.py - Modified Python term builder to generate function calls with correct parameter order, updating all memory-related function call constructions
  • Test files and specification files - Updated all test cases and specifications to use new parameter ordering, ensuring compatibility with the refactored function signatures
• Functional Improvements:
  • Unified function interface by moving memory parameter to the end
  • Changed parameter order for loadBytes and storeBytes functions
  • Updated all related sparse bytes operation functions

2. Commit efe1f78 (v0.1.111) - "Add division operations for RISC-V semantics"

• Purpose: Add division operation support to RISC-V semantics
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/riscv.md - Added complete implementation of DIV and DIVU instructions with proper handling of division by zero (returning -1 for signed, all 1s for unsigned) and overflow cases (signed division of most negative number by -1)
  • src/kriscv/kdist/riscv-semantics/word.md - Added /Word and /uWord syntax definitions for signed and unsigned word division operations, including proper type annotations and operator precedence
  • src/tests/integration/test_functions.py - Added comprehensive test suite with 83 lines covering all division scenarios: normal division, division by zero, overflow conditions, and edge cases for both signed and unsigned operations
• Functional Improvements:
  • Implemented signed division DIV and unsigned division DIVU instructions
  • Properly handled special cases for division by zero and overflow
  • Added 83 lines of comprehensive test code

3. Commit ddf2811 (v0.1.110) - "Simp rule 4 int2bytes o bytes2int"

• Purpose: Add simplification rules for byte and integer conversion
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added substr-reverse-bytes rule to simplify substring operations on reversed bytes and int2bytes-bytes2int-pad-zeros rule to optimize conversion chains that involve padding with zeros
  • src/tests/integration/test-data/specs/int2bytes-bytes2int.k - Added test specifications to verify the new simplification rules work correctly in various scenarios involving byte-to-integer and integer-to-byte conversions
• Functional Improvements:
  • Added substr-reverse-bytes and int2bytes-bytes2int-pad-zeros simplification rules
  • Optimized byte operation performance in symbolic execution

4. Commit 940f257 (v0.1.109) - "Remove redundant requirement for substr o int2bytes"

• Purpose: Remove redundant requirements for substr o int2bytes
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Removed unnecessary condition 0 <=Int Start from substr-int2bytes rule, making the rule more broadly applicable by eliminating overly restrictive constraints
  • src/tests/integration/test-data/specs/bytes-int.k - Updated test specifications to reflect the more general rule and added test cases that verify the rule works correctly without the redundant constraint
• Functional Improvements:
  • Removed redundant conditions in substr-int2bytes rule
  • Made simplification rules more general

5. Commit f5738c0 (v0.1.108) - "Simp rulle 4 >> 0"

• Purpose: Simplify right shift by 0 operations
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md - Added rule [rsh-0]: X >>Int 0 => X to eliminate unnecessary right shift by zero operations and removed some non-negative number constraints that were overly restrictive
• Functional Improvements:
  • Added rule [rsh-0]: X >>Int 0 => X simplification rule
  • Removed some unnecessary non-negative constraints

6. Commit 123a234 (v0.1.107) - "Simp rule 4 complex (X + Y & 4294967295) + Z & 4294967295"

• Purpose: Simplify complex 32-bit addition and bitwise operation expressions
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md - Added sophisticated simplification rules to handle complex arithmetic expressions involving 32-bit masking, particularly for nested addition and bitwise AND operations
  • src/kriscv/kdist/riscv-semantics/lemmas/word-simplifications.md - Added non-negativity rules for Bool2Word conversions and other word-level operations to enable more aggressive optimization
  • .gitignore - Updated to exclude additional build artifacts and temporary files generated during development
• Functional Improvements:
  • Added simplification rules for complex addition and bitwise operation combinations
  • Added non-negativity rules for Bool2Word
  • Improved .gitignore file

7. Commit 471d05f (v0.1.106) - "Refine simp rule for Bytes2Int o Int2Byes"

• Purpose: Improve byte to integer conversion simplification rules
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Removed the overly restrictive 0 <=Int V constraint from bytes2int-int2bytes rule, allowing the rule to apply to negative values as well, which is safe for byte conversion operations
• Functional Improvements:
  • Removed 0 <=Int V constraint from bytes2int-int2bytes rule
  • Resolved issue Fix unsimplified bytes2int o int2bytes patterns. #137

8. Commit 3804716 (v0.1.105) - "Add simplification rule for Bytes2Int &Int 4294967295"

• Purpose: Add simplification rules for byte to integer with 32-bit mask operations
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added bytes2int-ffffffff rule that simplifies Bytes2Int(B, LE, Unsigned) &Int 4294967295 to Bytes2Int(substrBytes(B, 0, 4), LE, Unsigned) when byte array length is greater than 4, effectively extracting only the first 4 bytes for 32-bit operations
• Functional Improvements:
  • Added bytes2int-ffffffff simplification rule
  • Optimized 32-bit mask operations

9. Commit db011d7 (v0.1.104) - "Add optimize_kcfg parameter in SymTool"

• Purpose: Add configuration graph optimization parameter to symbolic tools
• Modified Files:
  • src/kriscv/symtools.py - Added optimize_kcfg parameter to the SymTools class constructor and passed it to the underlying prover, allowing users to enable/disable control flow graph optimization based on their specific verification needs
• Functional Improvements:
  • Added optimize_kcfg parameter
  • Improved control flow graph optimization strategy for symbolic execution

10. Commit c72b80f (v0.1.103) - "Simp rule 4 (A +Int B) &Int 4294967295 <Int A"

• Purpose: Simplify inequality comparisons for addition operations with 32-bit mask
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md - Added new inequality simplification rules for expressions involving addition and 32-bit masking, particularly for overflow detection patterns
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Fixed bug in bytes2int-upperbound rule where the condition was incorrectly specified, correcting the upper bound calculation for byte-to-integer conversions
• Functional Improvements:
  • Added new inequality simplification rules
  • Fixed bug in bytes2int-upperbound rule

11. Commit 0d09047 (v0.1.102) - "Update dependency: deps/k_release"

• Purpose: Update K dependency version
• Modified Files:
  • deps/k_release - Updated to newer version of K framework to get latest bug fixes and performance improvements
  • deps/uv_release - Updated UV package manager dependency to maintain compatibility with latest version
  • uv.lock - Refreshed lock file to reflect new dependency versions and their transitive dependencies
• Functional Improvements:
  • Updated dependency versions to get latest features

12. Commit fca8f9f (v0.1.101) - "Add extensible prover implementation"

• Purpose: Add extensible prover implementation
• Modified Files:
  • src/kriscv/kprovex/ - Added complete new module with extensible prover implementation including __init__.py for module initialization, api.py for plugin API definitions, _default.py for semantics-agnostic default implementations, _loader.py for dynamic plugin loading, and _kprovex.py for main prover logic based on APRProver
  • src/kriscv/symtools.py - Integrated the new extensible prover into the symbolic tools framework, allowing users to choose between different prover implementations
• Functional Improvements:
  • Added new kprovex module implementing extensible prover based on APRProver
  • Includes plugin API definition, semantics-agnostic defaults, plugin loader, etc.
  • Architecture designed for upstream contribution

13. Commit fb931c8 (v0.1.100) - "fix version of uv in CI"

• Purpose: Fix UV version in CI
• Modified Files:
  • .github/actions/with-docker/Dockerfile - Fixed UV version specification in Docker build to ensure consistent package manager version across all CI environments
  • .github/workflows/test.yml - Updated GitHub Actions workflow to use pinned UV version, preventing CI failures due to version mismatches
  • deps/uv2nix - Added new dependency for UV to Nix conversion, enabling better integration with Nix-based builds
  • deps/uv_release - Added versioning file for UV package manager to track and manage UV updates systematically
• Functional Improvements:
  • Fixed UV version, improving CI stability

14. Commit c77e2a5 (v0.1.99) - "Fix version in uv.lock"

• Purpose: Fix lock file version
• Modified Files:
  • uv.lock - Massive update with 500+ lines changed, fixing version inconsistencies across all dependencies, resolving conflicts between direct and transitive dependencies, and ensuring reproducible builds
• Functional Improvements:
  • Fixed dependency version inconsistency issues

15. Commit 570e0f4 (v0.1.98) - "Add simp rules for reversed substrBytes concat"

• Purpose: Add simplification rules for reversed byte string concatenation
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added 29 lines of sophisticated simplification rules for handling reversed byte string concatenation patterns, particularly for operations like substrBytes(A +Bytes B, I, J) where the result can be optimized based on the relationship between indices and byte string lengths
• Functional Improvements:
  • Added 29 lines of new simplification rules
  • Optimized reversed byte string concatenation operations

16. Commit 2fc0603 (v0.1.97) - "Add simp rules 4 Bytes2Int o Int2Bytes and substrBytes o Int2Bytes"

• Purpose: Add simplification rules for byte-integer conversion
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added rules to simplify Bytes2Int(Int2Bytes(...)) patterns where the conversion chain can be eliminated or simplified, particularly for cases where the byte representation is immediately converted back to integer
  • src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md - Added complementary integer simplification rules to handle the mathematical aspects of byte-integer conversion chains
• Functional Improvements:
  • Optimized conversion operations between bytes and integers

Major Architecture Changes

17. Commit 711f12b (v0.1.96) - "Migrate from poetry to uv"

• Purpose: Migrate from Poetry to UV package manager
• Modified Files:
  • Removed poetry.lock (2166 lines) - Deleted old Poetry lock file with all its dependency specifications and version constraints
  • Added uv.lock (1555 lines) - New UV lock file with streamlined dependency management, faster resolution, and better conflict handling
  • pyproject.toml - Updated build configuration to use UV instead of Poetry, including new tool configuration sections and dependency specifications
  • Makefile - Updated build targets to use UV commands instead of Poetry, including installation, development setup, and testing commands
  • flake.nix - Updated Nix configuration to integrate with UV, providing better reproducibility and cross-platform compatibility
  • nix/ directory structure - Added complete Nix overlay system with kriscv-specific configurations and build system integrations
• Functional Improvements:
  • Adopted more modern package management tool
  • Improved build system and CI configuration
  • Added Nix build system support

18. Commit 07180df (v0.1.95) - "Remove attribute source_dir from SymTools"

• Purpose: Remove source directory attribute from symbolic tools
• Modified Files:
  • src/kriscv/symtools.py - Removed source_dir attribute from SymTools class, simplifying the API by eliminating the need for users to specify source directories explicitly
  • Multiple test specification files - Updated all test cases that previously relied on explicit source directory specification to use the new simplified API
• Functional Improvements:
  • Simplified symbolic tools API
  • Removed unnecessary source directory dependency

19. Commit cf4108d (v0.1.94) - "Add simp rules 4 &Int assoc"

• Purpose: Add associativity simplification rules for bitwise operations
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md - Added 12 lines of new simplification rules implementing associativity and commutativity for bitwise AND operations, enabling more aggressive optimization of complex bitwise expressions
• Functional Improvements:
  • Added 12 lines of new simplification rules
  • Optimized bitwise operation performance

20. Commit c2d312e (v0.1.93) - "Add property proof_show to SymTools"

• Purpose: Add proof display property to symbolic tools
• Modified Files:
  • src/kriscv/symtools.py - Added proof_show property to control proof output display, allowing users to enable/disable detailed proof information during symbolic execution
  • src/kriscv/tools.py - Updated tool integration to respect proof display settings and route proof output appropriately
  • src/kriscv/utils.py - Added utility functions for proof formatting and display, including proper handling of proof trees and step-by-step execution traces
• Functional Improvements:
  • Added 69 lines of new code
  • Enhanced proof display functionality
  • Added symbolic configuration tests

21. Commit 0949ca5 (v0.1.92) - "Update dependency: deps/k_release"

• Purpose: Update K dependency version
• Modified Files:
  • deps/k_release - Updated to newer K framework version to get latest bug fixes, performance improvements, and new features for better semantic analysis
• Functional Improvements:
  • Obtained latest K framework features

22. Commit f680218 (v0.1.91) - "Refactor RISC-V semantics to replace Word with Int"

• Purpose: Refactor RISC-V semantics to replace Word with Int
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/riscv.md - Comprehensive refactoring of all instruction semantics to use Int instead of Word for program counter, memory addresses, and register values, simplifying type management
  • src/kriscv/kdist/riscv-semantics/word.md - Updated Word module to work with Int-based system while maintaining backward compatibility for existing Word operations
  • src/kriscv/term_builder.py - Modified Python term builder to generate Int-based terms instead of Word-based terms, updating all term construction logic
  • src/kriscv/tools.py - Updated tools to use Int-based semantics, including configuration parsing and result formatting
  • Multiple test files - Updated all test cases to use Int-based expectations and assertions instead of Word-based ones
• Functional Improvements:
  • Changed program counter, memory addresses, register values to use Int
  • Simplified type handling
  • Affected 17 files, optimized code structure

23. Commit cba2d2b (v0.1.90) - "Enable instantiating symbolic config"

• Purpose: Enable symbolic configuration instantiation
• Modified Files:
  • src/kriscv/__main__.py - Added command-line interface for symbolic configuration instantiation, allowing users to create symbolic configurations from ELF files
  • src/kriscv/sparse_bytes.py - Enhanced sparse bytes implementation to support symbolic byte generation and manipulation
  • src/kriscv/symtools.py - Added symbolic configuration instantiation methods to symbolic tools, enabling creation of symbolic initial states
  • src/kriscv/term_builder.py - Updated term builder to handle symbolic configuration construction with proper variable binding and constraint generation
  • src/kriscv/tools.py - Added tools for symbolic configuration management, including validation and serialization
  • Added src/tests/integration/test_config_from_elf.py - New test suite with 104 lines testing symbolic configuration instantiation from ELF files, including various scenarios and edge cases
• Functional Improvements:
  • Added symbolic configuration instantiation capability
  • Refactored toolchain to support symbolic execution
  • Added 104 lines of configuration test cases

24. Commit d411af1 (v0.1.89) - "Write temporary test data into separate folders by default"

• Purpose: Write temporary test data into separate folders by default
• Modified Files:
  • src/tests/conftest.py - Modified test configuration to create separate temporary directories for each test worker, preventing race conditions and test interference by ensuring each test has its own isolated workspace
• Functional Improvements:
  • Resolved race conditions between test workers
  • Improved test reliability

25. Commit 759923e (v0.1.88) - "Inline the <test> cell"

• Purpose: Inline the test cell
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/riscv.md - Inlined test cell configurations directly into the main semantics file, ensuring user-specified configuration parts have a single root node for better parsing
  • Multiple test specification files - Updated all test specifications to work with the inlined test cell structure, maintaining compatibility while improving organization
• Functional Improvements:
  • Ensured user-specified configuration part has single root node
  • Optimized serialization of parseable claims

26. Commit 202c19a (v0.1.87) - "Transform function branchPC to effect function #PC_BRANCH"

• Purpose: Transform branch PC function to effect function
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/riscv.md - Refactored branch PC handling from a pure function branchPC to an effect function #PC_BRANCH, improving semantic consistency and enabling better optimization of branch instructions
• Functional Improvements:
  • Refactored branch handling logic
  • Improved semantic consistency

27. Commit 25b7057 (v0.1.86) - "Consolidate ELF file handling under class ELF"

• Purpose: Consolidate ELF file handling under ELF class
• Modified Files:
  • src/kriscv/elf_parser.py - Added 124 lines of new ELF class implementation, consolidating all ELF file operations including parsing, symbol resolution, and section handling into a single cohesive interface
  • src/kriscv/__main__.py - Updated command-line interface to use the new ELF class for file operations
  • src/kriscv/term_builder.py - Modified term builder to use consolidated ELF interface for symbol resolution and address mapping
  • src/kriscv/tools.py - Updated tools to use the new ELF class for file handling and configuration generation
• Functional Improvements:
  • Added 124 lines of code
  • Consolidated ELF file handling logic
  • Improved code organization structure

Optimization and Simplification Rules

28. Commit bb2934c (v0.1.85) - "Add simp rules for Int2Bytes o Bytes2Int"

• Purpose: Add simplification rules for integer-byte conversion
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added 9 lines of new simplification rules for Int2Bytes(Bytes2Int(...)) patterns, optimizing round-trip conversions that can be eliminated or simplified
• Functional Improvements:
  • Added 9 lines of new simplification rules

29. Commit 4c53805 (v0.1.84) - "Add simp rules for Bytes2Int o |Int o Bytes2Int"

• Purpose: Add simplification rules for byte-integer bitwise OR operations
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added sophisticated simplification rules for complex expressions involving byte-to-integer conversion, bitwise OR operations, and conversion back to bytes
• Functional Improvements:
  • Optimized complex byte bitwise operations

30. Commit 803850d (v0.1.83) - "simplify patterns Bytes2Int o <<Int & Bytes2Int o >>Int & chop"

• Purpose: Simplify byte-integer shift operation patterns
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added rules to simplify Bytes2Int(B) << N and Bytes2Int(B) >> N patterns, along with chop operations that can be optimized when combined with byte operations
• Functional Improvements:
  • Optimized shift operation handling

31. Commit c157326 (v0.1.82) - "Add simp rules for replaceAtBytes"

• Purpose: Add simplification rules for byte replacement
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added rules to optimize replaceAtBytes operations, particularly for cases where the replacement can be simplified or combined with other byte operations
• Functional Improvements:
  • Optimized byte replacement operations

32. Commit e2369f6 (v0.1.81) - "Add simp rules for substrBytes(A +Bytes B, I, J)"

• Purpose: Add simplification rules for substring of byte concatenation
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added rules to simplify substring operations on concatenated byte strings, optimizing cases where the substring can be taken directly from one of the components
• Functional Improvements:
  • Optimized substring operations on byte concatenation

33-35. Commits a5b98f5, 81d5723 (v0.1.80, v0.1.79) - "Update dependency: deps/k_release"

• Purpose: Update K dependency version
• Functional Improvements:
  • Maintained compatibility with latest K framework

36. Commit 66ddeca (v0.1.78) - "Simplify pattern Bytes2Int o substrBytes &Int 65280"

• Purpose: Simplify byte-integer bitwise AND with 65280
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Added specific optimization for Bytes2Int(substrBytes(...)) & 65280 patterns, which commonly occur in byte manipulation operations
• Functional Improvements:
  • Optimized specific bitwise operation patterns

37. Commit 79bf2fd (v0.1.77) - "Add simp rule to eliminate SignExtend"

• Purpose: Add simplification rules to eliminate sign extension
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md - Added rules to eliminate redundant sign extension operations, particularly when the value is already in the correct format
• Functional Improvements:
  • Optimized sign extension handling

38. Commit 4dcaa6f (v0.1.76) - "Tackle unexpected pattern for pickfront and dropfront"

• Purpose: Handle unexpected patterns for pickfront and dropfront
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md - Added rules to handle edge cases in pickfront and dropfront operations that weren't covered by existing simplifications
• Functional Improvements:
  • Improved sparse byte front-end operations

39. Commit 72ad19b (v0.1.75) - "Add simp rule for <<Int o <<Int"

• Purpose: Add simplification rules for consecutive left shifts
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md - Added rule to combine consecutive left shifts: (X << A) << B becomes X << (A + B) when safe
• Functional Improvements:
  • Optimized consecutive left shift operations

40. Commit 8090120 (v0.1.74) - "Avoid ambiguity for Word expressions"

• Purpose: Avoid ambiguity in Word expressions
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/word.md - Updated Word expression parsing to eliminate ambiguity in operator precedence and associativity rules
• Functional Improvements:
  • Improved Word expression parsing

41. Commit 0c40c65 (v0.1.73) - "Make Word shift operations total"

• Purpose: Make Word shift operations total
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/word.md - Made Word shift operations total functions by defining behavior for all possible shift amounts, including out-of-range values
• Functional Improvements:
  • Improved shift operation definitions

42. Commit 58d1958 (v0.1.72) - "Add new lemmas for substrBytes and update pickFront rule"

• Purpose: Add new lemmas for sub-byte strings and update pickFront rule
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md - Added new lemmas for substrBytes operations and updated pickFront rule to handle more cases correctly
• Functional Improvements:
  • Added new sparse byte simplification rules

43. Commit 883fd6e (v0.1.71) - "Remove the format attribute from Word"

• Purpose: Remove format attribute from Word
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/word.md - Removed the format attribute from Word definitions, simplifying the Word type and eliminating unnecessary complexity
• Functional Improvements:
  • Simplified Word definition

Symbolic Execution Improvements

44. Commit ec95dd6 (v0.1.70) - "Better loadBytes for symbolic execution"

• Purpose: Improve loadBytes operation for symbolic execution
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/sparse-bytes.md - Enhanced loadBytes implementation for symbolic execution by adding better handling of symbolic addresses and symbolic memory content
• Functional Improvements:
  • Optimized memory loading in symbolic execution

45. Commit 3a2bbc0 (v0.1.69) - "Better storeBytes for symbolic execution"

• Purpose: Improve storeBytes operation for symbolic execution
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/sparse-bytes.md - Enhanced storeBytes implementation for symbolic execution by improving handling of symbolic writes and memory aliasing
• Functional Improvements:
  • Optimized memory storing in symbolic execution

46. Commit 85e3216 (v0.1.68) - "Add option --depth to kriscv run"

• Purpose: Add depth option to kriscv run
• Modified Files:
  • src/kriscv/__main__.py - Added --depth command-line option to control execution depth in symbolic execution and simulation modes
  • src/kriscv/tools.py - Updated tools to respect depth limits and provide appropriate feedback when limits are reached
• Functional Improvements:
  • Enhanced runtime control options

47. Commit 60f10e1 (v0.1.67) - "Add simplification rule for storing symbolic bytes"

• Purpose: Add simplification rules for symbolic byte storage
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md - Added rules to optimize symbolic byte storage operations, particularly for cases where symbolic values can be reasoned about statically
• Functional Improvements:
  • Optimized symbolic byte storage operations

48-50. Commits 778e705, 53567c0, 951e6e7 (v0.1.66, v0.1.65, v0.1.64) - "Update dependency: deps/k_release"

• Purpose: Update K dependency version
• Functional Improvements:
  • Maintained compatibility with latest K framework

51. Commit 8f5e5b7 (v0.1.63) - "Add Byte simplification rules from evm semantics"

• Purpose: Add byte simplification rules from EVM semantics
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md - Ported proven byte simplification rules from EVM semantics, including optimizations for byte array operations that have been battle-tested in Ethereum verification
• Functional Improvements:
  • Leveraged optimization experience from EVM semantics

52. Commit c6b16ef (v0.1.62) - "Support symbolic sparse bytes generation via SparseBytes"

• Purpose: Support symbolic sparse bytes generation via SparseBytes
• Modified Files:
  • src/kriscv/sparse_bytes.py - Added 190 lines of new code implementing complete sparse bytes support with symbolic generation capabilities, including efficient representation of sparse memory regions
  • src/kriscv/term_builder.py - Updated term builder to handle sparse bytes construction and manipulation
  • src/tests/unit/test_sparse_bytes.py - Added 152 lines of comprehensive unit tests covering all aspects of sparse bytes functionality
• Functional Improvements:
  • Added complete sparse bytes support
  • Significantly enhanced symbolic execution capabilities

53. Commit 2755c4c (v0.1.61) - "Add writeByteBF simplification rules"

• Purpose: Add writeByteBF simplification rules
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md - Added simplification rules for writeByteBF operations, optimizing byte-level write operations in sparse memory representations
• Functional Improvements:
  • Optimized byte write operations

54. Commit 98eea27 (v0.1.60) - "Add symbolic execution rules for readByteBF in sparse-bytes.md"

• Purpose: Add symbolic execution rules for readByteBF in sparse bytes
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/sparse-bytes.md - Added symbolic execution rules for readByteBF operations, enabling better symbolic reasoning about byte-level memory reads
• Functional Improvements:
  • Improved byte reading in symbolic execution

55. Commit 74dc542 (v0.1.59) - "Allow --temp-dir option for test-prove"

• Purpose: Allow temporary directory option for test-prove
• Modified Files:
  • src/kriscv/symtools.py - Added --temp-dir option to test-prove command, allowing users to specify custom temporary directories for proof artifacts
• Functional Improvements:
  • Enhanced test tool flexibility

56. Commit 1e43e19 (v0.1.58) - "Enhance SymTools with bug report integration"

• Purpose: Enhance symbolic tools with bug report integration
• Modified Files:
  • src/kriscv/symtools.py - Added bug_report parameter to symbolic tools, enabling automatic bug report generation when verification fails or encounters errors
• Functional Improvements:
  • Added bug_report parameter
  • Improved debugging capabilities

57. Commit 76f893a (v0.1.57) - "Add command kriscv-asm <instruction>"

• Purpose: Add kriscv-asm instruction command
• Modified Files:
  • src/kriscv/devtools.py - Added new development tool for generating assembly instructions, including encoding and decoding capabilities
  • pyproject.toml - Added new console script entry point for the kriscv-asm command
• Functional Improvements:
  • Added assembly instruction generation tool
  • Convenient for building test cases

58. Commit 9f4184e (v0.1.56) - "Update dependency: deps/k_release"

• Purpose: Update K dependency version
• Functional Improvements:
  • Kept dependencies up to date

59. Commit 0526095 (v0.1.55) - "Add job for notifying dependents"

• Purpose: Add job for notifying dependents
• Modified Files:
  • .github/workflows/update.yml - Added GitHub Actions job to automatically notify dependent projects when new versions are released
• Functional Improvements:
  • Improved CI/CD workflow

60. Commit ae15f5d (v0.1.54) - "Add symbolic execution support"

• Purpose: Add symbolic execution support
• Modified Files:
  • src/kriscv/kdist/plugin.py - Added plugin support for symbolic execution, enabling extensible symbolic execution capabilities
  • src/kriscv/kdist/riscv-semantics/riscv.md - Updated RISC-V semantics to support symbolic execution with proper symbolic state handling
  • src/kriscv/symtools.py - Added 101 lines of new symbolic execution tools, including configuration, execution, and result analysis
  • src/tests/integration/test_prove.py - Added 58 lines of integration tests for symbolic execution and proof capabilities
• Functional Improvements:
  • Added complete symbolic execution support
  • Significantly enhanced verification capabilities

61. Commit 344cc7e (v0.1.53) - "Factor out runtime from Tools"

• Purpose: Factor out runtime from Tools
• Modified Files:
  • src/kriscv/tools.py - Refactored tools to separate runtime concerns from tool logic, improving code organization and enabling better testing
• Functional Improvements:
  • Improved code organization structure

62. Commit b8bf5d2 (v0.1.52) - "Implement MUL* instructions"

• Purpose: Implement MUL* instructions
• Modified Files:
  • src/kriscv/kdist/riscv-semantics/riscv-disassemble.md - Added disassembly support for M extension multiply instructions including MUL, MULH, MULHU, and MULHSU
  • src/kriscv/kdist/riscv-semantics/riscv-instructions.md - Added instruction definitions and encoding information for all multiply instructions
  • src/kriscv/kdist/riscv-semantics/riscv.md - Implemented complete semantics for multiply instructions with proper handling of overflow and signed/unsigned variants
  • src/kriscv/kdist/riscv-semantics/word.md - Added word-level multiply operations and helper functions
  • src/tests/integration/test_functions.py - Added 126 lines of comprehensive tests covering all multiply instruction variants and edge cases
• Functional Improvements:
  • Added M extension disassembler support
  • Implemented MUL, MULH, MULHU, MULHSU instructions
  • Added comprehensive multiplication tests

63. Commit 79552f6 (v0.1.51) - "Add option --zero-init"

• Purpose: Add zero initialization option
• Modified Files:
  • src/kriscv/tools.py - Added --zero-init option to initialize memory and registers to zero at startup, useful for deterministic testing and debugging
• Functional Improvements:
  • Enhanced initialization options