Search results

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

There is no jvm_fresh_cryptol_var

easyIssues that are expected to be easy to resolve and might therefore be good for new contributorsIssues that are expected to be easy to resolve and might therefore be good for new contributors

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

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

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.

#3192 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 24, 2026

·  

Someday

set_solver_cache_path "" should disable the solver cache

easyIssues that are expected to be easy to resolve and might therefore be good for new contributorsIssues that are expected to be easy to resolve and might therefore be good for new contributors

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: 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.

#3190 In GaloisInc/saw-script;

· danmatichuk opened on Apr 23, 2026

·  

current: normal

yosys_import fails on SystemVerilog files with parameterized modules

subsystem: hardwareIssues related to verification of hardwareIssues related to verification of hardware

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.

#3187 In GaloisInc/saw-script;

· brianhuffman opened on Apr 23, 2026

Deprecate and remove all uses of YosysSequential type in SAWScript

subsystem: hardwareIssues related to verification of hardwareIssues related to verification of hardware

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.

#3186 In GaloisInc/saw-script;

· brianhuffman opened on Apr 22, 2026

·  

current: advanced

Solver versions are re-extracted on every go

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

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

Status: Open.

#3178 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 21, 2026

·  

current: normal

Allow importing of Yosys circuits with black-boxed submodules

subsystem: hardwareIssues related to verification of hardwareIssues related to verification of hardware

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

Status: Open.

#3169 In GaloisInc/saw-script;

· brianhuffman opened on Apr 16, 2026

Crash passing Cryptol module handles to SAWScript functions

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

regressionSomething that used to work, but now doesn'tSomething that used to work, but now doesn't

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-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and execution

topics: error-handlingIssues involving the way SAW responds to an error conditionIssues involving the way SAW responds to an error condition

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.

#3167 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 16, 2026

·  

current: severe

crux-mir-comp crash with uninterpreted value passed to function (eval on BoundVarExpr produced non-Variable?)

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.

#3166 In GaloisInc/saw-script;

· RyanGlScott opened on Apr 16, 2026

·  

current: advanced

Cryptol.sawcore defines type-level mod incorrectly

missing cryptol featuresIssues about features in Cryptol that don't work in SAWIssues about features in Cryptol that don't work in SAW

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

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

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

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

Status: Open.

#3161 In GaloisInc/saw-script;

· brianhuffman opened on Apr 14, 2026

·  

current: advanced