Language design axes: full implementation (25 steps across 6 axes)#1731

Merged

Th0rgal merged 62 commits into

mainfrom

feature/language-design-axes-plan

Apr 22, 2026

Commits on Apr 13, 2026

docs: add language design axes implementation plan
claude
committed
feat(axis3): step 1a — auto-generate _is_view theorem for @[view] functions
claude
committed
feat(axis3): step 1b — add modifies(...) annotation with _frame theorem
claude
committed
feat(axis3): step 1c — add no_external_calls annotation with _no_calls theorem
claude
committed
feat(axis3): step 1d — annotation composition with _effects conjunction theorem
claude
committed
feat(axis2): step 2a — CEI static analysis with allow_post_interaction_writes opt-out
claude
committed
feat(axis2): step 2b — CEI escalation ladder with nonreentrant and cei_safe
claude
committed
feat(axis2): step 2c — requires(role) access control with _requires_role theorem
claude
committed
feat(axis1): step 3a — types section for semantic newtypes
claude
committed
feat(axis4): step 4a — storage namespace computation via kernel Keccak
claude
committed
feat(axis4): step 4b — opt-in storage_namespace slot offsetting
claude
committed
feat(axis4): step 4d — ABI + tooling integration for storage namespace
claude
committed
feat(axis6): step 6a — unsafe "reason" do block syntax
claude
committed
feat(axis6): step 6b — restricted operation gating outside unsafe blocks
claude
committed
feat(axis6): step 6c — trust report unsafe block entries + --deny-unsafe flag
claude
committed
feat(axis1): step 5a — inductive section in grammar for ADT declarations
claude
committed
feat(axis1): step 5b — ADT IR structures in compilation model
claude
committed
feat(axis1): steps 5c+5d — ADT storage encoding + Yul lowering
claude
committed
feat(axis1): step 5e — ADT ABI encoding as (uint8, uint256...) tuple
claude
committed
feat(axis4): step 4c — custom namespace override via storage_namespace "key"
claude
committed
feat(axis1): step 5f — tryExternalCall for non-reverting external calls
claude
committed
feat(axis3): steps 3b+3c — ParamType.newtypeOf + ValueType.newtype with Yul erasure
claude
committed
fix: resolve pre-existing build failures in Smoke.lean + IRInterpreter.lean
claude
committed
feat(axis1): wire ADT type definitions from syntax to ContractSpec (#1727 Step 5b)
claude
committed

Commits on Apr 14, 2026

Commits on Apr 15, 2026

Commits on Apr 21, 2026