Skip to content

Print Z_bneg as logical negation in Rust and Zig - #2422

Draft
JasonGross wants to merge 1 commit into
masterfrom
codex/fix-2525-logical-negation
Draft

Print Z_bneg as logical negation in Rust and Zig#2422
JasonGross wants to merge 1 commit into
masterfrom
codex/fix-2525-logical-negation

Conversation

@JasonGross

Copy link
Copy Markdown
Collaborator

Summary

  • emit Rust Z_bneg as a zero comparison cast to the generated one-bit type
  • emit Zig Z_bneg with @intFromBool
  • track logical negation’s one-bit result for correct nested casts
  • add focused emitter regressions and regenerate the 60 affected Rust/Zig files

This fixes the latent emitter mismatch described in Scrutineer finding #2525. Each generated artifact changes one expression line.

Testing

  • opam exec --switch=rocq-9.1 -- make -j4 SKIP_BEDROCK2=1 src/Stringification/Rust.vo src/Stringification/Zig.vo
  • cargo test --offline
  • zig build
  • zig build test
  • git diff --check

The Cargo crate currently has no unit/doc tests, so Cargo validates full compilation; the exact emitted syntax is covered by the Rocq regression examples.

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.

Emit zero tests instead of integer bitwise complements, track the one-bit natural result for cast insertion, and add focused emitter regressions. Regenerate the affected Rust and Zig outputs.
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