Repository navigation

Issues

New issue

Umbrella: proof-mode e2e readiness — any valid program + any spec => dischargeable .v
#366 · 0xGeorgii opened on Aug 8, 2026
Configurable, statically-known linear-memory size for generated WASM (CLI flag + [wasm] Inference.toml)
#221 · 0xGeorgii opened on Jun 6, 2026

wasm-to-v: name-handling follow-ups from #405 (stdlib import capture, embedded module name, spec-name over-rejection, stale hints and docs)
Inferara/inference#518 · opened on Oct 6, 2026
--import-memory: let a module import its linear memory from the host
Feature
Inferara/inference#512 · opened on Oct 1, 2026
continue; is reported as an undeclared variable, and compiles as a no-op when a binding named continue is in scope
Inferara/inference#505 · opened on Sep 29, 2026
Stellar: contractspecv0 has an empty doc for every method; /// doc comments never reach it
Inferara/inference#504 · opened on Sep 29, 2026
book: Stellar proving procedure says proofs/contract.wasm is the pre-rewrite module byte for byte, but a spec block makes it a superset
Inferara/inference#503 · opened on Sep 29, 2026
infs has no proof build for a stellar or spacewasm project without editing [build] target, and the refused proof build deletes the previous artifact
Inferara/inference#502 · opened on Sep 29, 2026
Overflow guards cost the ray-tracer benchmark 72% of its throughput
Inferara/inference#501 · opened on Sep 27, 2026
Allow bulk memory for SpaceWasm builds once nasa/spacewasm#54 ships
Inferara/inference#500 · opened on Sep 27, 2026
Check the SpaceWasm limits against upstream spacewasm-check once it exists
Inferara/inference#499 · opened on Sep 27, 2026
Measure whether SpaceWasm builds need their own unroll thresholds
Inferara/inference#498 · opened on Sep 27, 2026
Revisit WASI imports under infs run
Inferara/inference#478 · opened on Sep 23, 2026
exists/unique spec functions refuse an explicit -> () where an omitted return type is accepted
Inferara/inference#477 · opened on Sep 23, 2026
Report two unchecked host-module bounds to the SpaceWasm project
Inferara/inference#475 · opened on Sep 23, 2026
Proof-mode gate remedy names a flag infs users do not have (--target wasm32)
Inferara/inference#474 · opened on Sep 23, 2026
Delete the dead register_definition_from_external path in the type checker's symbol table
Inferara/inference#473 · opened on Sep 23, 2026
Stellar host binding: import-name mapping for non-identifier strings and Val wrapping (#324 remainder)
Inferara/inference#472 · opened on Sep 23, 2026
Let linked libraries call declared host imports (relax TransitiveHostImport)
Inferara/inference#471 · opened on Sep 23, 2026
Memory-touching host functions: frame conditions, and harness stubs that read guest memory
Inferara/inference#470 · opened on Sep 23, 2026
Proof mode for programs that bind host imports (Rocq axiomatization)
Inferara/inference#469 · opened on Sep 23, 2026
Linker survivor path: let a program mix host imports with statically linked modules
Inferara/inference#468 · opened on Sep 23, 2026
unique_function_name can reintroduce a __ run into an emitted Definition name
Inferara/inference#448 · opened on Aug 28, 2026
assume { f(x); } puts HA_app_ok in antecedent position, handing the prover trap-freedom for free
Inferara/inference#447 · opened on Aug 28, 2026
The end-of-body vanilla-WASM contract is skipped whenever a plan declines an @
Inferara/inference#446 · opened on Aug 28, 2026
Payload-invariance has no regression gate for fixtures without a .v golden
Inferara/inference#445 · opened on Aug 28, 2026
A037 misses named-constant and folded out-of-bounds indices, which the proof-mode translator already folds
Inferara/inference#442 · opened on Aug 26, 2026

Navigation Menu

Repository navigation

Issues

Issues

wasm-to-v: name-handling follow-ups from #405 (stdlib import capture, embedded module name, spec-name over-rejection, stale hints and docs)

--import-memory: let a module import its linear memory from the host

`continue;` is reported as an undeclared variable, and compiles as a no-op when a binding named `continue` is in scope

Stellar: `contractspecv0` has an empty doc for every method; `///` doc comments never reach it

book: Stellar proving procedure says `proofs/contract.wasm` is the pre-rewrite module byte for byte, but a `spec` block makes it a superset

infs has no proof build for a `stellar` or `spacewasm` project without editing `[build] target`, and the refused proof build deletes the previous artifact

Overflow guards cost the ray-tracer benchmark 72% of its throughput

Allow bulk memory for SpaceWasm builds once nasa/spacewasm#54 ships

Check the SpaceWasm limits against upstream `spacewasm-check` once it exists

Measure whether SpaceWasm builds need their own unroll thresholds

Revisit WASI imports under `infs run`

`exists`/`unique` spec functions refuse an explicit `-> ()` where an omitted return type is accepted

Report two unchecked host-module bounds to the SpaceWasm project

Proof-mode gate remedy names a flag infs users do not have (`--target wasm32`)

Delete the dead register_definition_from_external path in the type checker's symbol table

Stellar host binding: import-name mapping for non-identifier strings and Val wrapping (#324 remainder)

Let linked libraries call declared host imports (relax TransitiveHostImport)

Memory-touching host functions: frame conditions, and harness stubs that read guest memory

Proof mode for programs that bind host imports (Rocq axiomatization)

Linker survivor path: let a program mix host imports with statically linked modules

unique_function_name can reintroduce a __ run into an emitted Definition name

assume { f(x); } puts HA_app_ok in antecedent position, handing the prover trap-freedom for free

The end-of-body vanilla-WASM contract is skipped whenever a plan declines an @

Payload-invariance has no regression gate for fixtures without a .v golden

A037 misses named-constant and folded out-of-bounds indices, which the proof-mode translator already folds