argumentcomputer / argumentcomputer/RustFFI.lean

Are the integers really signed or unsigned?

Open
#5 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Lean
Stars
17
Forks
2
PR merge metrics
No merged PRs in 30d

Description

Rust code defines the parameters to be signed `i32`:

https://github.com/lurk-lab/RustFFI.lean/blob/af3a8f68d1657d4db9cac43e9bbba0bec1aaf1ad/src/lib.rs#L2

But Lean defines them to be unsigned `UInt32`:

https://github.com/lurk-lab/RustFFI.lean/blob/af3a8f68d1657d4db9cac43e9bbba0bec1aaf1ad/Main.lean#L2

How does that even work 🤯

Contributor guide

No contributing guide indexed for this repository

Research direction

Compare the parameter definitions at src/lib.rs line 2 and Main.lean line 2, then trace how the Rust FFI boundary represents and passes the values. Determine whether the signedness mismatch is intentional or a bug; done means the issue has a documented resolution and the definitions are consistent if a change is required.

Written by the indexing model from the issue text.

Assessment

Tech stack
rust
Domain
compilers
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
30/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.