Search results

#setArgsFromStack may set operandConstant in locals which makes locals may store operand instead of only Values

Status: Open.

#1070 In runtimeverification/mir-semantics;

· Stevengre opened on Apr 18, 2026

Reloading proof crashes on with nix installation

bugSomething isn't workingSomething isn't working

Status: Open.

Bug

#1067 In runtimeverification/mir-semantics;

· dkcumming opened on Apr 16, 2026

Unify #traverseProjection value representation to eliminate singleton Range round-trips

area:semanticsK semantics definitionsK semantics definitions

kind:refactorCode restructuringCode restructuring

priority:p1Important but not most urgentImportant but not most urgent

status:triageNew, not yet organizedNew, not yet organized

type:taskWell-scoped, directly executable workWell-scoped, directly executable work

Status: Open.

#1011 In runtimeverification/mir-semantics;

· Stevengre opened on Apr 1, 2026

feat: add address allocation model for pointer-to-integer semantics

status:readyClear and approved by humanClear and approved by human

Status: Open.

#1002 In runtimeverification/mir-semantics;

· Stevengre opened on Mar 26, 2026

Nested transparent wrapper pointer casts produce incorrect projection chains

Status: Open.

#997 In runtimeverification/mir-semantics;

· Stevengre opened on Mar 20, 2026

No-LLVM-kompile approach causes 5x prove performance regression due to kore-rpc fallback

area:semanticsK semantics definitionsK semantics definitions

kind:perfPerformance improvementPerformance improvement

priority:p2Valuable but can waitValuable but can wait

status:iceboxValuable but not being pursued nowValuable but not being pursued now

type:bugUnexpected behavior or regressionUnexpected behavior or regression

Status: Open.

#992 In runtimeverification/mir-semantics;

· Stevengre opened on Mar 18, 2026

Inline Ty indices: replace ty(Int) references with actual type data

area:semanticsK semantics definitionsK semantics definitions

area:typesType systemType system

priority:p2Valuable but can waitValuable but can wait

status:triageNew, not yet organizedNew, not yet organized

type:featureNew capability or enhancementNew capability or enhancement

Status: Open.

#991 In runtimeverification/mir-semantics;

· Stevengre opened on Mar 17, 2026

[FEAT] Add performance benchmarking and profiling infrastructure

Status: Open.

#970 In runtimeverification/mir-semantics;

· Stevengre opened on Mar 4, 2026

Incrementally integrate external Rust test suites into mir-semantics CI

Status: Open.

#964 In runtimeverification/mir-semantics;

· Stevengre opened on Mar 2, 2026

Remove mutability tracking from MIR semantics

Status: Open.

#949 In runtimeverification/mir-semantics;

· Stevengre opened on Feb 26, 2026

Semantics of iterator core code

bugSomething isn't workingSomething isn't working

Status: Open.

#914 In runtimeverification/mir-semantics;

· dkcumming opened on Jan 19, 2026

feat: support panic

Status: Open.

#899 In runtimeverification/mir-semantics;

· Stevengre opened on Dec 17, 2025