Search results

unfolding_fix_once is unable to prove a simple theorem about a recursive function

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3218 In GaloisInc/saw-script;

· brianhuffman opened on May 4, 2026

·  

current: advanced

REPL :search should be able to include name patterns

needs designTechnical design work is needed for issue to progressTechnical design work is needed for issue to progress

subsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and execution

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3217 In GaloisInc/saw-script;

· sauclovian-g opened on May 4, 2026

·  

current: normal

SAWCore type error messages have too many @free annotations

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3216 In GaloisInc/saw-script;

· brianhuffman opened on May 4, 2026

·  

current: normal

Unify and generalize functions add_prelude_eqs/add_cryptol_eqs and add_prelude_defs/add_cryptol_defs

needs designTechnical design work is needed for issue to progressTechnical design work is needed for issue to progress

needs testIssues for which we should add a regression testIssues for which we should add a regression test

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

topics: saw-core namesIssues related to URI-based saw-core namesIssues related to URI-based saw-core names

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3213 In GaloisInc/saw-script;

· brianhuffman opened on May 1, 2026

·  

current: normal

Implement means to browse/query/search the set of defined SAWCore names

subsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-core

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: feature requestIssues requesting a new feature or capabilityIssues requesting a new feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3212 In GaloisInc/saw-script;

· brianhuffman opened on May 1, 2026

·  

current: normal

prove and prove_print should work with SAWCore terms of type Prop

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3211 In GaloisInc/saw-script;

· brianhuffman opened on May 1, 2026

·  

current: normal

parseUninterpretedSAW seems to be wrong for rationals.

needs testIssues for which we should add a regression testIssues for which we should add a regression test

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3206 In GaloisInc/saw-script;

· yav opened on Apr 28, 2026

·  

current: normal

Feature request: Report on all uses of unsafeAssert in imported Cryptol terms

subsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-core

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

unsoundnessIssues that can lead to unsoundness or false verificationIssues that can lead to unsoundness or false verification

Status: Open.

#3205 In GaloisInc/saw-script;

· brianhuffman opened on Apr 28, 2026

·  

current: advanced

test_timeout is unreliable

tooling: test infrastructureIssues involving test infrastructure or test execution, or making SAW more testableIssues involving test infrastructure or test execution, or making SAW more testable

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3204 In GaloisInc/saw-script;

· brianhuffman opened on Apr 28, 2026

·  

current: normal

Malformed term in test_cryptol_module_sha512

subsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-core

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

subsystem: saw-core-rocqIssues related to converting saw-core to Gallina for use with the Rocq theorem proverIssues related to converting saw-core to Gallina for use with the Rocq theorem prover

tech debtIssues that document or involve technical debtIssues that document or involve technical debt

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3198 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 25, 2026

·  

current: normal

crux-mir-comp slowdown with uninterpreted/overridden Cryptol functions on arrays

performanceIssues that involve or include performance problemsIssues that involve or include performance problems

subsystem: crucible-mir-compIssues related to compositional Rust verification with crucible-mir-comp or crux-mir-compIssues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3195 In GaloisInc/saw-script;

· samcowger opened on Apr 24, 2026

·  

current: advanced

There should be functions for extracting the LLVM/JVM/MIR types of LLVm/JVM/MIR values

needs testIssues for which we should add a regression testIssues for which we should add a regression test

subsystem: crucible-jvmIssues related to Java verification with crucible-jvmIssues related to Java verification with crucible-jvm

subsystem: crucible-llvmIssues related to LLVM bitcode verification with crucible-llvmIssues related to LLVM bitcode verification with crucible-llvm

subsystem: crucible-mirIssues related to Rust verification with crucible-mir and/or mir-jsonIssues related to Rust verification with crucible-mir and/or mir-json

subsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and execution

type: feature requestIssues requesting a new feature or capabilityIssues requesting a new feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3194 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 24, 2026

·  

Someday