Act Rewrite

[zoep]

This PR introduces a major rewrite of Act, including substantial language, type system, and backend changes.

• Language & Syntax Changes

  • Constructors now support case splitting
  • Various stylistic and syntactic refinements

• Typechecker

  • Complete rewrite of the typechecker
  • New type inference system
  • Integration of an SMT backend to discharge entailment obligations, including:
    • Integer bound checking
    • Constructor precondition check
    • Array bounds check

• hevm backend

  • Support for new language features, including case expressions in constructors
  • Support for payable constructors and callvalue
  • Improved error reporting
  • Multiple bug fixes and improvements

• Rocq backend

• Support for contract creation

• Added more predicates and relations that encode properties of addresses

• Renamed relations for clarity

Miscellaneous:

• Support for Act spec spanning across multiple files

[Copilot]

Pull request overview

This PR introduces a comprehensive rewrite of Act, modernizing the language syntax and type system. It implements a new typechecker with SMT-backed constraint solving, updates the HEVM backend to support new language features, and renames the Coq backend to Rocq.

Changes:

• Complete typechecker rewrite with SMT-based entailment checking for integer bounds, constructor preconditions, and array bounds
• Language syntax changes including new constructor case splitting, updated keywords (transition/updates/creates), and payable constructors
• HEVM backend improvements with support for new language features and better error reporting

Reviewed changes

Copilot reviewed 105 out of 646 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/Act/Syntax/Untyped.hs	Updated AST representation with new syntax types and timing tags
src/Act/Syntax/Types.hs	New type system with TValueType and expanded ActType support
src/Act/Syntax/Typed.hs	Updated typed AST with new reference types and storage updates
src/Act/Traversals.hs	Added mapExp function and updated traversal functions for new AST
src/Act/Parse.y	Parser updated for new language syntax and keywords
src/Act/Lex.x	Lexer updated with new tokens and keywords
src/Act/Print.hs	Pretty printer updated for new AST structure
src/Act/Error.hs	Enhanced error reporting with position-aware error messages
src/Act/HEVM_utils.hs	HEVM utilities updated with payable constructor support
src/Act/Overflow.hs	New module for integer overflow checking
src/Act/Entailment.hs	New module for SMT-based entailment constraint checking
src/Act/Bounds.hs	Updated bounds checking for new type system
src/Act/Decompile.hs	Updated decompilation for new typed expressions
tests/	Removed obsolete test files for array operations
lib/ActLib.v	Simplified Env record in Rocq library
act.cabal	Updated dependencies and exposed modules
README.md	Enhanced documentation
Makefile	Updated test targets with new backend names

Comments suppressed due to low confidence (1)

src/Act/Syntax/Types.hs:1

• Corrected spelling of 'int2565' to 'int256'.

{-# LANGUAGE GADTs #-}

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.