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 7ee0d8e898..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 @@ -556,7 +557,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 +580,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 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) 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 *)