-
-
Notifications
You must be signed in to change notification settings - Fork 17
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Emit contractspecv0 so Stellar tooling can type contract arguments
codegenBytecode emittingBytecode emittingenhancementNew feature or requestNew feature or requestStatus: Open.#466 In Inferara/inference;Support host function imports (host:: externs the embedder satisfies at runtime)
cliCommand line interface relatedCommand line interface relatedcodegenBytecode emittingBytecode emittingenhancementNew feature or requestNew feature or requestStatus: Open.#464 In Inferara/inference;unique_function_name can reintroduce a __ run into an emitted Definition name
rocq-translationwasm-to-v translation, hassert obligations, and the emitted .v contractwasm-to-v translation, hassert obligations, and the emitted .v contractStatus: Open.#448 In Inferara/inference;assume { f(x); } puts HA_app_ok in antecedent position, handing the prover trap-freedom for free
rocq-translationwasm-to-v translation, hassert obligations, and the emitted .v contractwasm-to-v translation, hassert obligations, and the emitted .v contractStatus: Open.#447 In Inferara/inference;The end-of-body vanilla-WASM contract is skipped whenever a plan declines an @
codegenBytecode emittingBytecode emittingStatus: Open.#446 In Inferara/inference;Payload-invariance has no regression gate for fixtures without a .v golden
rocq-translationwasm-to-v translation, hassert obligations, and the emitted .v contractwasm-to-v translation, hassert obligations, and the emitted .v contractStatus: Open.#445 In Inferara/inference;A037 misses named-constant and folded out-of-bounds indices, which the proof-mode translator already folds
static analysisStatic code analysisStatic code analysisStatus: Open.#442 In Inferara/inference;P016 is lexical: a reachability body calling a dynamically-indexing function can still carry a false obligation
static analysisStatic code analysisStatic code analysisStatus: Open.#441 In Inferara/inference;- Status: Open.#436 In Inferara/inference;
- Status: Open.#435 In Inferara/inference;
wasm-to-v: inference.spec_funcs indices are never range-checked, silently renumbering the call graph
Status: Open.#434 In Inferara/inference;linker/driver: the one-import-many-declarations write-set guard compares a single field, so a future contract field reintroduces the #333 miscompile silently
codegenBytecode emittingBytecode emittinglinkerLinkerLinkerneed-triageAn issue needs research to decide how to handle itAn issue needs research to decide how to handle itStatus: Open.#433 In Inferara/inference;