Skip to content

[Compiler Enhancement] Infer mutability through internal calls#1925

Merged
Th0rgal merged 4 commits into
lfglabs-dev:mainfrom
duncancmt:dcmt/mutability
May 23, 2026
Merged

[Compiler Enhancement] Infer mutability through internal calls#1925
Th0rgal merged 4 commits into
lfglabs-dev:mainfrom
duncancmt:dcmt/mutability

Conversation

@duncancmt
Copy link
Copy Markdown
Contributor

Summary

  • Infer read/write effects across internal helper calls before validating view and pure mutability.
  • Add pure support to the verity_contract function syntax and propagate it into generated function specs.
  • Generate _is_pure facts for pure macro functions and include pure facts in bundled _effects theorems.
  • Add feature coverage for internal-call mutability inference and macro pure ABI emission.

Test Plan

  • lake build
  • python3 scripts/check_lean_hygiene.py
  • python3 scripts/check_axioms.py
  • python3 scripts/generate_print_axioms.py --check
  • python3 scripts/generate_verification_status.py --check
  • FOUNDRY_PROFILE=difftest forge test

Related Issues

#734

This is still in support of Bacon-labs/tamago#6

Infer function read/write effects across internal calls before mutability validation.

Add macro support for pure function declarations and generated _is_pure facts.

Co-Authored-By: Codex <codex@openai.com>
@duncancmt duncancmt requested a review from Th0rgal as a code owner May 20, 2026 12:00
@vercel
Copy link
Copy Markdown

vercel Bot commented May 20, 2026

@duncancmt is attempting to deploy a commit to the LFG Labs Team on Vercel.

A member of the Team first needs to authorize it.

@Th0rgal Th0rgal merged commit d678e1e into lfglabs-dev:main May 23, 2026
33 of 37 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants