argumentcomputer / argumentcomputer/RustFFI.lean
Are the integers really signed or unsigned?
オープン
- 主要言語
- Lean
- スター
- 17
- フォーク
- 2
- PR マージ指標
- 30日以内にマージされた PR はありません
説明
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 🤯
コントリビューションガイド
このリポジトリのコントリビューションガイドは索引されていません
調査の方向性
src/lib.rs の 2 行目と Main.lean の 2 行目にあるパラメーター定義を比較し、Rust FFI 境界が値をどのように表現して渡しているかを追跡します。符号の不一致が意図的なものかバグなのかを判断します。問題の解決策が文書化され、変更が必要な場合は定義に一貫性がある状態をもって完了とします。
索引モデルが issue の本文から書いたものです。
評価
- 技術スタック
- rust
- 領域
- compilers
- issue の種類
- バグ
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 活発さ
- 停滞
- 明瞭さ
- 説明が足りない
- 初心者へのやさしさ
- 30/100