Skip to content

PROGRESS_LOG.md

Latest commit

 

History

History
98 lines (81 loc) · 11.8 KB

PROGRESS_LOG.md

File metadata and controls

98 lines (81 loc) · 11.8 KB
Raw

Progress Log

This is the live tail of the progress log. The full historical log (857 dated entries, through 2026-06-28) has been moved verbatim to docs/PROGRESS_ARCHIVE.md.

The July 2026 cleanup and composition-readiness work (Phases 1–6: substrate unification, the shared interaction package, de-monolithing, deleting the observation layer, the interaction-monad external boundary, and this documentation/freeze phase) is recorded — one dated entry per decision — in docs/DECISIONS.md, alongside ROADMAP.md.

2026-09-28 — enum conversion preserves narrow checked arithmetic

  • First unresolved report a2e9dc3f-5e48-4a10-b96b-17c04a7beadc evaluates EN(a + b) with uint8 values 200 and 100. Solc panics 0x11 while the model previously widened the add, produced 300, and then panicked 0x21 on enum range.
  • Lower the enumFromUInt operand through the env-aware path at its inferred integer type and apply that type's checked cleanup before the enum range check.
  • Witness and Forge controls cover overflow precedence, a safe narrow sum, and an ordinary uint256 out-of-range conversion that must remain Panic(0x21).

2026-09-28 — target-type bare literals in tuple components

  • First unresolved report a0a02eb1-5aff-4f5a-bf1e-33135a291d7b binds a bare hex literal to a bytes4 component of a tuple declaration. The single-binding form was already target-typed, while tuple lowering used dynamic-bytes literal lowering and panicked at assignment.
  • Extend the existing per-component tuple target-typing path for bare hex/string literals at bytesN targets. Declaration and assignment forms share the fix; ordinary tuple components retain their existing env-less lowering.
  • Forge controls cover hex and string declarations plus tuple assignment.

2026-09-28 — immediate calls through returned internal function pointers

  • First unresolved report 229edb9e-733e-4d71-8ff2-75efe2d34cfe uses a bare return g()(7). The arbitrary-callee pointer dispatcher already handled this expression inside binary contexts, but the generic return fallback skipped the internal-call expression hoister and failed checked-executable generation.
  • Route generic returns and matching local initializers through that hoister. Teach argument-position ANF discovery that an arbitrary-callee call whose callee has an internal function type is an internal single-return call, so the same shape works in eager argument positions such as abi.encode and nested immediate calls. Keep initializer declarations in statement-list scope.
  • The exact submission and direct-return Lean witness pass. End-to-end importer controls for direct return, initializer, abi.encode, and nested calls all agree with solc/EVM; the four-case Forge suite passes. Full queue replay fixes the first report and a later direct-invocation report, with no prior NO_DIVERGENCE regression; three later storage-pointer consumers advance from fail-closed to their independent runtime gaps and remain open.

2026-09-28 — fixed-bytes compound-assignment cleanup

  • First unresolved report 68e6a639-0f42-4f50-a7a1-96ac0b31aa18 shows that bytes4 b = 0x11223344; b <<= 8 retains the shifted-out byte instead of storing 0x22334400. The compound-assignment cleanup table covered narrow integers and enums but omitted fixed bytes.
  • Add a fixed-bytes value cleanup that masks the computed word to the LValue's byte width, and select it for bytesN/fixedBytes targets. This preserves the existing single-evaluation compound-assignment path for locals and storage.
  • The exact submission, Lean regression, and five-case Forge suite pass. Controls cover local, mapping, state, and fixed-array LValues plus right shift. The full 927-submission replay changes only this report from SOUNDNESS_GAP to NO_DIVERGENCE.

2026-09-28 — conditional external-function selectors

  • First-file report: d75fdb5e-bb86-4da1-bdc3-02dfc810c999 (2026-07-24 21:22:14 UTC), (c ? this.f : this.g).selector.
  • Type member access from the checked external-function receiver; distribute selector resolution over a conditional while retaining the condition and branch choice. Existing direct named-selector purity behavior remains covered.
  • Solc-imported witness and Forge controls cover both branches and the direct pure selector. The original submission and later assignment-condition report 42948632 now agree with the EVM. All 927 queue cases replayed: two become NO_DIVERGENCE; one exposes a separate narrow-arithmetic SOUNDNESS_GAP after type acceptance; other verdicts unchanged.
  • Targeted Lean build and contest sample suite passed. Full build validation recorded in the PR.

2026-09-28 — discarded selector preserves receiver side effects

  • First unresolved report 7ca2655c-8f3b-4154-90fa-047df41aaf69 uses h().f.selector;, where h() writes storage. Selector resolution replaced the entire member expression with a literal before lowering, erasing the call and its observable state change.
  • In expression-statement position the selector value is discarded. When the selector is known, retain and resolve the call-valued receiver as the statement so its effects and failures occur. Do the same before a return when the selector is the whole returned value, optionally under explicit casts.
  • The first report and a later return-expression report change from wrong-state soundness gaps to agreement. Lean resolver witnesses and pinned-solc 0.8.35 Forge controls cover both forms.

Most recent archived entries

  • 2026-06-28 07:55:01 PDT - typechecker/custom-error-static-acceptedness - paired custom-error static acceptedness against pinned solc and the common checker. Added invalid solc lanes for reserved Error/Panic names, duplicate error parameter names, unknown custom-error reverts, free custom-error overloading, data-location annotations on error parameters, and local-error shadowing of a free error with the wrong argument shape; added customErrorStaticDisciplineMatches covering those rejections plus accepted named custom-error arguments, require with custom-error payloads, file/contract error shadowing with matching local shapes, and dynamic string error payloads. Verification: lake build SolidCore.Spine.L00_SourceSolidity.TypeCheck; focused custom-error harness with solc_rejects=ok, forge=ok, and lean=ok; lake build SolidCore.Spine.L00_SourceSolidity.Checked; pinned-solc AST audit with sources=93, rendered_sources=93, unimplemented_node_types=0, unclassified_child_fields=0, and render_failures=0; full paired replay with forge_interpreter_compare=pass, status=0, cases=93, and paired_cases_passed=yes; manifest parse reports cases=93, solc_rejects=227, and lean_evals=374; Python compilation, shell syntax, scoped no-sorry/no-admit/no-axiom scan, git diff --check, and generated-cache cleanup are green.
  • 2026-06-28 07:19:52 PDT - typechecker/try-catch-static-acceptedness - paired try/catch static acceptedness against pinned solc and the common checker. Added invalid solc lanes for internal function calls, low-level calls, array push calls, literals, return-type mismatch, missing catch clauses, invalid bytes return locations, duplicate try return names, bad catch Error header, duplicate Error/Panic catches, and duplicate low-level catches; added tryCatchStaticDisciplineMatches covering those rejections plus accepted external-function, contract-member, bytes-memory return, Error/Panic/bytes catch, and contract-creation try forms. Verification: lake build SolidCore.Spine.L00_SourceSolidity.TypeCheck; focused try-catch harness with solc_rejects=ok, forge=ok, and lean=ok; lake build SolidCore.Spine.L00_SourceSolidity.Checked; pinned-solc AST audit with sources=93, rendered_sources=93, unimplemented_node_types=0, unclassified_child_fields=0, and render_failures=0; full paired replay with forge_interpreter_compare=pass, status=0, cases=93, and paired_cases_passed=yes; manifest parse reports cases=93, solc_rejects=220, and lean_evals=373; Python compilation, shell syntax, scoped no-sorry/no-admit/no-axiom scan, git diff --check, and generated-cache cleanup are green.
  • 2026-06-28 06:44:01 PDT - typechecker/event-static-acceptedness - paired event static acceptedness against pinned solc and the common checker. The shared source-declarations fixture now imports accepted external-function event parameters, three-indexed non-anonymous events, and four-indexed anonymous events; invalid lanes require pinned-solc rejection of mapping event parameters, free mapping events, internal-function event parameters, non-anonymous events with four indexed params, anonymous event .selector, and unknown emitted events. Added eventStaticDisciplineMatches and a manifest eval for the common checker. Verification: lake build SolidCore.Spine.L00_SourceSolidity.TypeCheck; focused source-declarations harness with solc_rejects=ok, forge=ok, and lean=ok; lake build SolidCore.Spine.L00_SourceSolidity.Checked; pinned-solc AST audit with sources=93, rendered_sources=93, unimplemented_node_types=0, unclassified_child_fields=0, and render_failures=0; full paired replay with forge_interpreter_compare=pass, status=0, cases=93, and paired_cases_passed=yes; manifest parse reports cases=93, solc_rejects=205, and lean_evals=372; Python compilation, shell syntax, scoped no-sorry/no-admit/no-axiom scan, git diff --check, and generated-cache cleanup are green.
  • 2026-06-28 06:08:31 PDT - compaction-resume/typechecker-status - resumed after compaction to answer how close the common Solidity typechecker is to full solc-faithful coverage; current checkpoint is the 93-case corpus with 199 pinned-solc rejection lanes and 371 Lean eval witnesses after the callable-header and fallback/receive override slice.
  • 2026-06-28 06:06:16 PDT - typechecker/callable-header-and-fallback-override-acceptedness - paired callable header and fallback/receive override acceptedness against pinned solc and the common checker. The shared source-declarations fixture now compiles accepted fallback and receive overrides, and invalid lanes require pinned-solc rejection of missing fallback override, payable-over-nonpayable fallback override, virtual constructors, virtual/payable free functions, and bodyless fallback declarations without virtual. Added callableHeaderAndOverrideDisciplineMatches and a manifest eval for the common checker. Verification: lake build SolidCore.Spine.L00_SourceSolidity.TypeCheck; focused source-declarations harness with solc_rejects=ok, forge=ok, and lean=ok; lake build SolidCore.Spine.L00_SourceSolidity.Checked; pinned-solc AST audit with sources=93, rendered_sources=93, unimplemented_node_types=0, unclassified_child_fields=0, and render_failures=0; full paired replay with forge_interpreter_compare=pass, status=0, cases=93, and paired_cases_passed=yes; manifest parse reports cases=93, solc_rejects=199, and lean_evals=371; Python compilation, shell syntax, scoped no-sorry/no-admit/no-axiom scan, git diff --check, and generated-cache cleanup are green.

2026-09-28 — encodeCall singleton arithmetic follow-up

  • Credited report 13324306-3e94-4a9e-9fd9-76d258d7a67f still diverged at PR 75's merge commit: the importer unwraps (a+b), while the previous fix and hand-built witness matched a singleton tuple only.
  • Add plain-expression encodeCall arms to both cleanup-routing predicates and env-aware lowering. Preserve the operand's own type width. Witness covers actual importer shape plus original tuple shape, safe and overflowing cases.
  • Twelve real solc/Foundry/importer controls (uint8/int8; single/nested/tuple; safe/overflow) pass. Original submission now agrees. Full build and queue replay results are recorded in the PR; existing first-file credit remains unchanged.