AeneasVerif

誰かが対応中かもしれないイシューは最後に並べています。 すべて日付順に表示

• Bug: char literals are extracted to Lean without escaping

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 2/5 1〜3時間 初心者へのやさしさ 78/100

  AeneasVerif/aeneas#1467 · 2026年10月19日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Uncaught `Invalid_argument "Can't get the list of fields of this adt"` when code builds a variant of an opaque enum

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 3/5 1〜2日 初心者へのやさしさ 55/100

  AeneasVerif/aeneas#1463 · 2026年10月16日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: `There should be no bottoms in the value` on `if true { panic!() }`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 42/100

  AeneasVerif/aeneas#1462 · 2026年10月16日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Internal error in `simplify_loop_output_conts` when code after a loop reads one field of a tuple loop variable

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 22/100

  AeneasVerif/aeneas#1459 · 2026年10月16日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Lean backend: references to crate-level items lose the crate prefix and can resolve to a same-named definition in a module

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  AeneasVerif/aeneas#1458 · 2026年10月16日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Missing backwards function in Lean backend with iterators

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 5/5 1週間以上 初心者へのやさしさ 22/100

  AeneasVerif/aeneas#1437 · 2026年10月14日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Uncaught exception: `CFailure`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  AeneasVerif/aeneas#1435 · コメント 1 件 · 2026年10月13日 に作成

  メンテナーはふだん 1 日以内に返信

• Model for `core::num::NonZero`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 18/100

  AeneasVerif/aeneas#1418 · 2026年10月12日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Lean backend emits namespace references captured by structure fields and local binders

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 45/100

  AeneasVerif/aeneas#1411 · コメント 1 件 · 2026年10月9日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: user `Drop` impls never run, so a destructor's effect is silently lost

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 5/5 1週間以上 初心者へのやさしさ 15/100

  AeneasVerif/aeneas#1410 · 2026年10月9日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: `<[T]>::contains` model calls `eq(needle, element)`, but core calls `eq(element, needle)`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 2/5 1〜3時間 初心者へのやさしさ 72/100

  AeneasVerif/aeneas#1409 · 2026年10月9日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: elabDoMatch: duplicate binder

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  AeneasVerif/aeneas#1406 · 2026年10月8日 に作成

  メンテナーはふだん 1 日以内に返信

• Support typed copies

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement

  難易度 5/5 1週間以上 初心者へのやさしさ 12/100

  AeneasVerif/aeneas#1405 · コメント 1 件 · 2026年10月8日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Internal error in `InterpMatchCtxs` when joining loop contexts over non-opaque wrapper holding borrow

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 22/100

  AeneasVerif/aeneas#1399 · 2026年10月5日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: `[CONST; N]` repeat of a non-`Copy` type

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  AeneasVerif/aeneas#1450 · コメント 5 件 · 2026年10月5日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: fieldless enum variant written into an array is translated as `()` when a later loop borrows the array

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  AeneasVerif/aeneas#1395 · 2026年10月3日 に作成

  メンテナーはふだん 1 日以内に返信

• Feature request: Translate inline asm using Kraken

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  AeneasVerif/aeneas#1396 · コメント 3 件 · 2026年10月3日 に作成

  メンテナーはふだん 1 日以内に返信

• Isabelle/HOL backend: contribution proposal

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 8/100

  AeneasVerif/aeneas#1389 · 2026年10月1日 に作成

  メンテナーはふだん 1 日以内に返信

• Formulate specs for unsigned integers in terms of `Int` instead of `Nat`?

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 5/5 1週間以上 初心者へのやさしさ 18/100

  AeneasVerif/aeneas#1387 · 2026年10月1日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: uncaught `CFailure` in `PrePasses.update_array_default` when an impl's trait is removed by Charon's `--exclude`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 45/100

  AeneasVerif/aeneas#1375 · 2026年9月27日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: `vec![x]` requires an unused external type `core::mem::maybe_uninit::MaybeUninit`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  AeneasVerif/aeneas#1370 · 2026年9月26日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: internal error at `InterpReduceCollapse.ml:1137` on `if let Some(x) = slice.get(i)` inside a loop

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  AeneasVerif/aeneas#1369 · 2026年9月26日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: internal error at `InterpMatchCtxs.ml:230` when joining contexts that hold a struct of borrowed slices

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  AeneasVerif/aeneas#1368 · 2026年9月26日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: no `partial_fixpoint` monotonicity lemma for `loop`, so recursion through a loop does not elaborate

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 1〜2日 初心者へのやさしさ 35/100

  AeneasVerif/aeneas#1367 · 2026年9月26日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: `@[discriminant]` instances are declared in the root namespace and clash across extractions

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 半日 初心者へのやさしさ 62/100

  AeneasVerif/aeneas#1366 · コメント 1 件 · 2026年9月26日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: error when matching contexts

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 5/5 1週間以上 初心者へのやさしさ 15/100

  AeneasVerif/aeneas#1349 · 2026年9月16日 に作成

  メンテナーはふだん 1 日以内に返信

• Lean backend: type-decl holding a `Box<dyn Iterator>` field is refused with "Dynamic trait types are not supported yet" — minimal repro (charon translates it fine)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  AeneasVerif/aeneas#1343 · 2026年9月10日 に作成

  メンテナーはふだん 1 日以内に返信

• Docs: Documentation still recommends deprecated `#setup_aeneas_simps`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 78/100

  AeneasVerif/aeneas#1324 · 2026年8月30日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Nested items within anonymous const items (const `_`) generate invalid Lean identifiers

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 35/100

  AeneasVerif/aeneas#1323 · リアクション 1 件 · 2026年8月30日 に作成

  メンテナーはふだん 1 日以内に返信

• Internal error (Interp.ml:609) on `<[T]>::get` inside a loop

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 34/100

  AeneasVerif/aeneas#1319 · 2026年8月28日 に作成

  メンテナーはふだん 1 日以内に返信

• Improve documentation (discoverability?) for beginners

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 3/5 1〜2日 初心者へのやさしさ 35/100

  AeneasVerif/aeneas#1295 · リアクション 5 件 · 2026年8月24日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Could not match the contexts` on a loop

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 18/100

  AeneasVerif/aeneas#1282 · 2026年8月21日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: A generic struct whose field mentions one instantiation of itself produces an invalid `mutual inductive`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 45/100

  AeneasVerif/aeneas#1281 · 2026年8月21日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Comparisons are emitted as Prop

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 45/100

  AeneasVerif/aeneas#1279 · 2026年8月21日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: `IScalar.rem` is falsely modeled as non-panicking for MIN % (-1)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 2/5 1〜3時間 初心者へのやさしさ 55/100

  AeneasVerif/aeneas#1275 · 2026年8月20日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Closure returning reference argument fails with non-endable abstraction

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 18/100

  AeneasVerif/aeneas#1266 · 2026年8月15日 に作成

  メンテナーはふだん 1 日以内に返信

• Feature request: `async`

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement

  難易度 5/5 1週間以上 初心者へのやさしさ 12/100

  AeneasVerif/aeneas#1265 · 2026年8月15日 に作成

  メンテナーはふだん 1 日以内に返信

• Feature request: Add support for mutually recursive functions and trait implementations

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement

  難易度 5/5 1週間以上 初心者へのやさしさ 15/100

  AeneasVerif/aeneas#1264 · コメント 1 件 · 2026年8月15日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Matching an indexed `enum` value fails during expansion

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 45/100

  AeneasVerif/aeneas#1253 · コメント 1 件 · 2026年8月11日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Distinct lifetimes in `Option<&T>::as_ref()` trigger internal error

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 22/100

  AeneasVerif/aeneas#1252 · 2026年8月11日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: ` u8 as char` fails to translate

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 3/5 半日 初心者へのやさしさ 45/100

  AeneasVerif/aeneas#1251 · 2026年8月10日 に作成

  メンテナーはふだん 1 日以内に返信

• Lean backend emits a `sorry`-named structure with error-hole fields for the dyn-compatible trait `digest::DynDigest` instead of failing cleanly

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 42/100

  AeneasVerif/aeneas#1243 · 2026年7月31日 に作成

  メンテナーはふだん 1 日以内に返信

• Items depending on a failed-to-translate derived impl are still emitted, producing ill-typed Lean with dangling identifiers and inline `sorry /- ERROR: ... -/` bodies

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 30/100

  AeneasVerif/aeneas#1242 · コメント 1 件 · 2026年7月31日 に作成

  メンテナーはふだん 1 日以内に返信

• Uncaught `Not_found` in `extract_function_call` (Extract.ml) when a called trait method's declaration is missing — partially written output files are left on disk

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 40/100

  AeneasVerif/aeneas#1241 · コメント 1 件 · 2026年7月31日 に作成

  メンテナーはふだん 1 日以内に返信

• Uncaught `Not_found` in `ty_has_mut_borrow_for_region_in_pred` (TypesUtils.ml) when translating functions generic over a large trait-clause web with outlives predicates (arkworks `Pairing`)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 4/5 3〜5日 初心者へのやさしさ 32/100

  AeneasVerif/aeneas#1239 · コメント 1 件 · 2026年7月31日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: Nested borrows: selecting a `&'static [u8]` constant by match, and the single-variant case silently folds

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 5/5 1週間以上 初心者へのやさしさ 12/100

  AeneasVerif/aeneas#1234 · 2026年7月27日 に作成

  メンテナーはふだん 1 日以内に返信

• scalar_tac does not see through the *.rMax / *.rMin constants (no scalar_tac_simps equations)

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 2/5 1〜3時間 初心者へのやさしさ 70/100

  AeneasVerif/aeneas#1233 · 2026年7月27日 に作成

  メンテナーはふだん 1 日以内に返信

• Bug: A Rust struct field named `mk` collides with the generated Lean constructor and breaks the whole file

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  bug

  難易度 3/5 1〜2日 初心者へのやさしさ 45/100

  AeneasVerif/aeneas#1231 · 2026年7月25日 に作成

  メンテナーはふだん 1 日以内に返信

• Feature request: Full support for Higher ranked trait bounds

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル
  enhancement translation

  難易度 5/5 1週間以上 初心者へのやさしさ 15/100

  AeneasVerif/aeneas#1227 · コメント 2 件 · 2026年7月23日 に作成

  メンテナーはふだん 1 日以内に返信

• Merge the `Error` variants

  オープン

  ⋯この Issue の問題を報告

  • 何か問題がありますか？

  • すでに着手されている
  • 初心者向けではない
  • 古い・無効
  • その他…
  • 送信 キャンセル

  難易度 4/5 3〜5日 初心者へのやさしさ 25/100

  AeneasVerif/aeneas#1225 · コメント 18 件 · リアクション 1 件 · 2026年7月20日 に作成

  メンテナーはふだん 1 日以内に返信