All issues

Search results

infs real-infc integration tests silently skip on Windows CI: infc resolved at target/debug while the Windows leg builds --target x86_64-pc-windows-gnu

testsUnit, fuzzing, performance, etc.Unit, fuzzing, performance, etc.

Status: Open.

#369 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

infs single-file run does not resolve [wasm-dependencies]

Status: Open.

Bug

#367 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

Umbrella: proof-mode e2e readiness — any valid program + any spec => dischargeable .v

proof-modeinfc --mode proof / wasm-to-v / hassert obligation pipelineinfc --mode proof / wasm-to-v / hassert obligation pipeline

Status: Open.

Task

#366 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

wasm-to-v: GC composite types silently emit garbage; unwrap aborts on malformed foreign wasm

Status: Open.

Bug

#365 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

Linker envelope: accept real-toolchain externals (own globals/data/tables; integer width conversions) for proof mode

Status: Open.

Feature

#363 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

Disposition of feat/wasm-verifier-e2e (draft PR #235): superseded by the hassert pipeline

Status: Open.

Task

#364 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

Cross-module specs: allow obligations to reference linked external functions (post-link T_app) + write-set contracts

Status: Open.

Feature

#362 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

Codegen panics (todo!) on accepted programs: strings, unit literals, Stmt::TypeDef, Expr::Type, complex assignment targets

Status: Open.

Bug

#360 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

CI: type-check generated .v against the real wasm-verifier + stub-drift gate

Status: Open.

Task

#359 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

wasm-to-v: emit compilable proof skeletons (Admitted.) instead of Qed. on open proofs

Status: Open.

Task

#358 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

Narrow-scalar @ and spec params emit unconstrained obligations (missing range antecedents)

Status: Open.

Bug

#357 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026

Spec bodies that compute degrade to HA_true silently (vacuous obligation, no diagnostic)

Status: Open.

Bug

#356 In Inferara/inference;

· 0xGeorgii opened on Aug 8, 2026