From 63557299ad3a704e22aaf005fa595fb7627c08fd Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 9 Jul 2026 19:51:46 -0400 Subject: [PATCH 1/3] Whitespace only --- saw-central/src/SAWCentral/Prover/Exporter.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/saw-central/src/SAWCentral/Prover/Exporter.hs b/saw-central/src/SAWCentral/Prover/Exporter.hs index 7ee0d8e898..a3cfc662f2 100644 --- a/saw-central/src/SAWCentral/Prover/Exporter.hs +++ b/saw-central/src/SAWCentral/Prover/Exporter.hs @@ -556,7 +556,7 @@ writeRocqSAWCorePrelude outputFile notations skips = do mm <- scGetModuleMap sc m <- scFindModule sc nameOfSAWCorePrelude let configuration = rocqTranslationConfiguration notations skips - m' <- Rocq.translateSAWModule sc configuration mm m + m' <- Rocq.translateSAWModule sc configuration mm m let doc = vcat [ Rocq.preamble configuration, m'] case outputFile of "" -> print doc @@ -579,7 +579,7 @@ writeRocqCryptolPrimitivesForSAWCore cryFile notations skips = do withImportSAWCorePreludeExtra $ withImportSAWCorePrelude $ rocqTranslationConfiguration notations skips - m' <- Rocq.translateSAWModule sc configuration mm m + m' <- Rocq.translateSAWModule sc configuration mm m let doc = vcat [ Rocq.preamble configuration, m'] case cryFile of "" -> print doc From 39f477c7560c4ac62679994426a0d9d20d49cb31 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 9 Jul 2026 19:23:00 -0400 Subject: [PATCH 2/3] saw-core-rocq: Simply proofs of minNat_min and maxNat_max This is done for symmetry with `addNat_add` and `mulNat_mul`, whose proofs are similarly trivial. --- .../rocq/handwritten/CryptolToRocq/SAWCorePreludeExtra.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCorePreludeExtra.v b/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCorePreludeExtra.v index f13c18cf30..7d46db9584 100644 --- a/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCorePreludeExtra.v +++ b/saw-core-rocq/rocq/handwritten/CryptolToRocq/SAWCorePreludeExtra.v @@ -27,14 +27,16 @@ Proof. induction x; induction y; simpl; congruence. Defined. +(* NOTE: minNat is now defined as Rocq min, so this is trivial *) Theorem minNat_min : forall x y, minNat x y = min x y. Proof. - induction x; induction y; simpl; auto. + reflexivity. Defined. +(* NOTE: maxNat is now defined as Rocq max, so this is trivial *) Theorem maxNat_max : forall x y, maxNat x y = max x y. Proof. - induction x; induction y; simpl; auto. + reflexivity. Defined. (* NOTE: addNat is now defined as Rocq plus, so this is trivial *) From 39a4ac080e5379ba7f656611c8673d4f33e4c2f0 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 9 Jul 2026 19:51:21 -0400 Subject: [PATCH 3/3] saw-core-rocq: Repair solveUnsafeAssert There were two problems: 1. It was never brought into scope when `write_rocq_term` was used to generate Rocq code due to a missing `CryptolPrimitivesForSAWCoreExtra` import. We fix this by adding the import to the top of the generated file. 2. The definition of `solveUnsafeAssert` itself was not properly simplifying proof goals. It is unclear to me if this is a change brought on by more recent versions of Rocq, but in any case, repairing this appears to be a matter of being more precise with `unfold`s and `rewrite`s. Fixes #3336. --- .../saw-core-rocq/test_arithmetic.log.good | 12 ++++++++++ .../saw-core-rocq/test_boolean.log.good | 10 ++++++++ otherTests/saw-core-rocq/test_lambda.log.good | 5 ++++ .../saw-core-rocq/test_literals.log.good | 14 +++++++++++ .../saw-core-rocq/test_offline_rocq.log.good | 6 +++++ .../saw-core-rocq/test_records.log.good | 15 ++++++++++++ .../saw-core-rocq/test_sequences.log.good | 23 +++++++++++++++++++ otherTests/saw-core-rocq/test_tuples.log.good | 7 ++++++ .../saw-core-rocq/test_typelevel.log.good | 4 ++++ saw-central/src/SAWCentral/Prover/Exporter.hs | 1 + .../CryptolPrimitivesForSAWCoreExtra.v | 15 ++++++------ 11 files changed, 105 insertions(+), 7 deletions(-) diff --git a/otherTests/saw-core-rocq/test_arithmetic.log.good b/otherTests/saw-core-rocq/test_arithmetic.log.good index 92f91fd606..df2d2a3f1e 100644 --- a/otherTests/saw-core-rocq/test_arithmetic.log.good +++ b/otherTests/saw-core-rocq/test_arithmetic.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -42,6 +43,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -69,6 +71,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -96,6 +99,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -123,6 +127,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -151,6 +156,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -178,6 +184,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -204,6 +211,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -230,6 +238,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -255,6 +264,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -280,6 +290,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -320,6 +331,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_boolean.log.good b/otherTests/saw-core-rocq/test_boolean.log.good index f9cc379d1c..14ef72966c 100644 --- a/otherTests/saw-core-rocq/test_boolean.log.good +++ b/otherTests/saw-core-rocq/test_boolean.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -37,6 +38,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -62,6 +64,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -93,6 +96,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -120,6 +124,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -147,6 +152,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -171,6 +177,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -195,6 +202,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -219,6 +227,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -243,6 +252,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_lambda.log.good b/otherTests/saw-core-rocq/test_lambda.log.good index 925cd28e75..6de5b7b3c9 100644 --- a/otherTests/saw-core-rocq/test_lambda.log.good +++ b/otherTests/saw-core-rocq/test_lambda.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -41,6 +42,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -69,6 +71,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -96,6 +99,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -126,6 +130,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_literals.log.good b/otherTests/saw-core-rocq/test_literals.log.good index 96163080c8..7c4d4f406f 100644 --- a/otherTests/saw-core-rocq/test_literals.log.good +++ b/otherTests/saw-core-rocq/test_literals.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -37,6 +38,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -70,6 +72,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -109,6 +112,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -145,6 +149,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -176,6 +181,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -203,6 +209,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -228,6 +235,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -252,6 +260,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -277,6 +286,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -302,6 +312,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -327,6 +338,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -352,6 +364,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -376,6 +389,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_offline_rocq.log.good b/otherTests/saw-core-rocq/test_offline_rocq.log.good index 7092fadb74..90abf9f6ee 100644 --- a/otherTests/saw-core-rocq/test_offline_rocq.log.good +++ b/otherTests/saw-core-rocq/test_offline_rocq.log.good @@ -14,6 +14,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -46,6 +47,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -71,6 +73,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -99,6 +102,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -126,6 +130,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -154,6 +159,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_records.log.good b/otherTests/saw-core-rocq/test_records.log.good index f06badd290..6b024a0b3b 100644 --- a/otherTests/saw-core-rocq/test_records.log.good +++ b/otherTests/saw-core-rocq/test_records.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -41,6 +42,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -66,6 +68,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -94,6 +97,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -120,6 +124,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -148,6 +153,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -173,6 +179,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -198,6 +205,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -226,6 +234,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -250,6 +259,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -278,6 +288,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -308,6 +319,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -333,6 +345,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -366,6 +379,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -403,6 +417,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_sequences.log.good b/otherTests/saw-core-rocq/test_sequences.log.good index 18c0f08e10..61d88c4ed5 100644 --- a/otherTests/saw-core-rocq/test_sequences.log.good +++ b/otherTests/saw-core-rocq/test_sequences.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -40,6 +41,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -66,6 +68,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -90,6 +93,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -117,6 +121,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -146,6 +151,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -174,6 +180,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -202,6 +209,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -231,6 +239,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -259,6 +268,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -287,6 +297,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -317,6 +328,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -346,6 +358,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -374,6 +387,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -403,6 +417,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -432,6 +447,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -465,6 +481,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -498,6 +515,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -526,6 +544,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -555,6 +574,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -585,6 +605,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -613,6 +634,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -642,6 +664,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_tuples.log.good b/otherTests/saw-core-rocq/test_tuples.log.good index 94af2ba011..56c9e02cd0 100644 --- a/otherTests/saw-core-rocq/test_tuples.log.good +++ b/otherTests/saw-core-rocq/test_tuples.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -40,6 +41,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -67,6 +69,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -95,6 +98,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -124,6 +128,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -151,6 +156,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -178,6 +184,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/otherTests/saw-core-rocq/test_typelevel.log.good b/otherTests/saw-core-rocq/test_typelevel.log.good index 20d264233d..679d6e8c97 100644 --- a/otherTests/saw-core-rocq/test_typelevel.log.good +++ b/otherTests/saw-core-rocq/test_typelevel.log.good @@ -13,6 +13,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -38,6 +39,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -63,6 +65,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) @@ -87,6 +90,7 @@ Import VectorNotations. (** Post-preamble section specified by you *) From CryptolToRocq Require Import SAWCorePrelude. From CryptolToRocq Require Import CryptolPrimitivesForSAWCore. +From CryptolToRocq Require Import CryptolPrimitivesForSAWCoreExtra. (** Code generated by saw-core-rocq *) diff --git a/saw-central/src/SAWCentral/Prover/Exporter.hs b/saw-central/src/SAWCentral/Prover/Exporter.hs index a3cfc662f2..9b71c9db8d 100644 --- a/saw-central/src/SAWCentral/Prover/Exporter.hs +++ b/saw-central/src/SAWCentral/Prover/Exporter.hs @@ -465,6 +465,7 @@ writeRocqTerm :: TopLevel () writeRocqTerm name notations skips path t = do let configuration = + withImportCryptolPrimitivesForSAWCoreExtra $ withImportCryptolPrimitivesForSAWCore $ withImportSAWCorePrelude $ rocqTranslationConfiguration notations skips diff --git a/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v b/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v index 6618801648..12da775d24 100644 --- a/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v +++ b/saw-core-rocq/rocq/handwritten/CryptolToRocq/CryptolPrimitivesForSAWCoreExtra.v @@ -49,14 +49,15 @@ Defined. Ltac solveUnsafeAssertStep := match goal with | [ |- context [ Succ ] ] => unfold Succ - | [ |- context [ addNat _ _ ] ] => rewrite addNat_add - | [ |- context [ mulNat _ _ ] ] => rewrite mulNat_mul - | [ |- context [ subNat _ _ ] ] => rewrite subNat_sub - | [ |- context [ maxNat _ _ ] ] => rewrite maxNat_max - | [ |- context [ minNat _ _ ] ] => rewrite minNat_min + | [ |- context [ Eq ] ] => unfold Eq + | [ |- context [ addNat ?m ?n ] ] => rewrite (addNat_add m n) + | [ |- context [ mulNat ?m ?n ] ] => rewrite (mulNat_mul m n) + | [ |- context [ subNat ?m ?n ] ] => rewrite (subNat_sub m n) + | [ |- context [ maxNat ?m ?n ] ] => rewrite (maxNat_max m n) + | [ |- context [ minNat ?m ?n ] ] => rewrite (minNat_min m n) | [ n : Num |- _ ] => destruct n - | [ |- Eq Num (TCNum _) (TCNum _) ] => apply Eq_TCNum - | [ |- Eq Num _ _ ] => reflexivity + | [ |- @eq Num (TCNum _) (TCNum _) ] => apply Eq_TCNum + | [ |- @eq Num _ _ ] => reflexivity | [ |- min ?n ?n = _ ] => rewrite (min_nn n) | [ |- min ?n (S ?n) = _ ] => rewrite (min_nSn n) | [ |- min (S ?n) ?n = _ ] => rewrite (min_Snn n)