Skip to content

Make AMD64 field operations safe for in-place use - #2401

Draft
JasonGross wants to merge 1 commit into
masterfrom
codex/fix-2521-amd64-aliasing
Draft

Make AMD64 field operations safe for in-place use#2401
JasonGross wants to merge 1 commit into
masterfrom
codex/fix-2521-amd64-aliasing

Conversation

@JasonGross

Copy link
Copy Markdown
Collaborator

Summary

  • snapshot input limbs before executing the optimized schedules in the 43 affected AMD64 implementations
  • preserve support for both out1 == arg1 and out1 == arg2
  • document the in-place calling contract
  • add an exhaustive regression test covering all 620 shipped assembly implementations

The regression assembles each implementation, compares its distinct-buffer result with the corresponding generated C function, and then verifies both supported output/input aliasing forms. This addresses Scrutineer finding #2521.

Testing

  • fiat-amd64/test_aliasing.py
  • CC=clang fiat-amd64/test_aliasing.py
  • python3 -m py_compile fiat-amd64/test_aliasing.py
  • git diff --check

Both GCC and Clang runs report:

All 620 assembly files support output/input aliasing

The extracted Coq checker was not available locally because the isolated worktree lacked etc/coq-scripts/Makefile.vo_closure; clean CI should formally revalidate the modified hints. Existing performance ratio/footer metadata also predates the snapshot prologues and should be rebenchmarked before marking this ready.

Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.

@JasonGross

Copy link
Copy Markdown
Collaborator Author

Local review found no further patch changes necessary. I audited all 43 snapshot prologues for exact input coverage, stack-pointer balance, and separation between existing scratch space and the new snapshots. GCC and Clang runtime tests both pass all 620 assembly implementations. I also ran an alias-aware symbolic equivalence checker over all seven affected operation groups; every group passed the ordinary disjoint-buffer equivalence check and the out1 == arg1, out1 == arg2, and combined-alias configurations.

GitHub currently shows no completed failures. The full test-amd64 job is still queued; the completed platform jobs exercise only the lite AMD64 set, which does not include these 43 large-limb snapshots.

Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.

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.

1 participant