chore: use built-in SAT solver for CBMC proofs (#781)

Invoking an external solver is not necessarily cheaper in terms of CPU or memory usage.
aws · Apr 25, 2024 · 42f7af6 · 42f7af6
1 parent cb22f6a
commit 42f7af6
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/.github/workflows/proof_ci.yaml b/.github/workflows/proof_ci.yaml
@@ -152,8 +152,6 @@ jobs:
           echo "$(pwd)" >> $GITHUB_PATH
       - name: Run CBMC proofs
         shell: bash
-        env:
-          EXTERNAL_SAT_SOLVER: kissat
         working-directory: ${{ env.PROOFS_DIR }}
         run: ${{ env.RUN_CBMC_PROOFS_COMMAND }}
       - name: Check repository visibility

diff --git a/aws-encryption-sdk-specification b/aws-encryption-sdk-specification
+0 −5		.github/CODEOWNERS
+0 −4		.github/PULL_REQUEST_TEMPLATE.md
+1 −1		.github/workflows/ci_static-analysis.yaml
+1 −7		.gitignore
+0 −2		.prettierignore
+0 −91		README.md
+1 −1		changes/2020-05-13_remove-keyring-trace/change.md
+8 −8		changes/2020-06-09_wrapping-key-identifiers/change.md
+0 −301		changes/2022-06-19_seperate_material_providers/background.md
+0 −130		changes/2022-06-19_seperate_material_providers/change.md
+0 −441		changes/2022-11-14_encryption_context_on_decrypt/background.md
+0 −259		changes/2022-11-14_encryption_context_on_decrypt/encryption_context_use_cases.md
+0 −360		changes/2022-11-14_encryption_context_on_decrypt/proposal.md
+0 −217		changes/2023-06-19_thread_safe_cache/background.md
+0 −196		changes/2023-06-19_thread_safe_cache/change.md
+0 −286		changes/2023_7_12_update-keystore-structure/background.md
+0 −150		changes/2023_7_12_update-keystore-structure/proposal.md
+1 −1		ci/prettify.sh
+0 −100		client-apis/client.md
+9 −58		client-apis/decrypt.md
+31 −94		client-apis/encrypt.md
+178 −0		compliance/framework/aws-kms/aws-kms-key-arn.txt
+79 −0		compliance/framework/aws-kms/aws-kms-key-arn/2.5.toml
+47 −0		compliance/framework/aws-kms/aws-kms-key-arn/2.8.toml
+52 −0		compliance/framework/aws-kms/aws-kms-key-arn/2.9.toml
+123 −0		compliance/framework/aws-kms/aws-kms-mrk-are-unique.txt
+48 −0		compliance/framework/aws-kms/aws-kms-mrk-are-unique/2.5.toml
+233 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider.txt
+14 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.5.toml
+102 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.6.toml
+182 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.7.toml
+50 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.8.toml
+106 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key-provider/2.9.toml
+225 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key.txt
+81 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.10.toml
+63 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.11.toml
+14 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.5.toml
+64 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.6.toml
+12 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.7.toml
+12 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.8.toml
+179 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-master-key/2.9.toml
+194 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings.txt
+98 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings/2.5.toml
+163 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-multi-keyrings/2.6.toml
+311 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.txt
+14 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.5.toml
+42 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.6.toml
+258 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.7.toml
+217 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring/2.8.toml
+212 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring.txt
+14 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.5.toml
+61 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.6.toml
+12 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.7.toml
+258 −0		compliance/framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring/2.8.toml
+110 −0		compliance/framework/aws-kms/aws-kms-mrk-match-for-decrypt.txt
+48 −0		compliance/framework/aws-kms/aws-kms-mrk-match-for-decrypt/2.5.toml
+3 −1		data-format/message-body.md
+46 −68		data-format/message-header.md
+1 −4		data-format/message.md
+0 −44		framework/README.md
+89 −449		framework/algorithm-suites.md
+0 −112		framework/aws-kms/aws-kms-discovery-keyring.md
+0 −403		framework/aws-kms/aws-kms-hierarchical-keyring.md
+0 −166		framework/aws-kms/aws-kms-keyring.md
+30 −29		framework/aws-kms/aws-kms-mrk-aware-multi-keyrings.md
+36 −36		framework/aws-kms/aws-kms-mrk-aware-symmetric-keyring.md
+20 −20		framework/aws-kms/aws-kms-mrk-aware-symmetric-region-discovery-keyring.md
+1 −1		framework/aws-kms/aws-kms-mrk-match-for-decrypt.md
+0 −109		framework/aws-kms/aws-kms-multi-keyrings.md
+0 −267		framework/aws-kms/aws-kms-rsa-keyring.md
+0 −636		framework/branch-key-store.md
+4 −3		framework/caching-cmm.md
+8 −57		framework/cmm-interface.md
+0 −110		framework/commitment-policy.md
+13 −91		framework/cryptographic-materials-cache.md
+25 −48		framework/default-cmm.md
+24 −41		framework/keyring-interface.md
+395 −0		framework/kms-keyring.md
+16 −10		framework/local-cryptographic-materials-cache.md
+12 −9		framework/multi-keyring.md
+24 −35		framework/raw-aes-keyring.md
+6 −6		framework/raw-rsa-keyring.md
+0 −104		framework/required-encryption-context-cmm.md
+0 −162		framework/storm-tracking-cryptographic-materials-cache.md
+8 −239		framework/structures.md
+0 −38		framework/synchronized-local-cryptographic-materials-cache.md
+0 −113		framework/transitive-requirements.md
+0 −0		proposals/2020-07-01_aws-kms-keyring-redesign/background.md
+3 −3		proposals/2020-07-01_aws-kms-keyring-redesign/change.md
+0 −68		proposals/2022-10-27_rsa-keyring-v2/proposal.md
+12 −20		util/extract.js
+1 −1		util/report.js
+0 −17		util/specification_extract.sh