From 8f9a32f340552ad6940036c5357a26db11f3a921 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 14 Oct 2021 14:47:23 -0700 Subject: [PATCH 1/2] fix weird universe constraints being generated by f_equal --- .../coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v index 5322b4c4a1..3f8deb7889 100644 --- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v +++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v @@ -72,7 +72,13 @@ Qed. Theorem unfold_fold_IRT As Ds D : forall u, unfoldIRT As Ds D (foldIRT As Ds D u) = u. Proof. - revert Ds; induction D; try destruct u; simpl; f_equal; try easy. + revert Ds; induction D; intros; try destruct u; simpl(*; f_equal; try easy*). + (* For some reason using `f_equal` above generates universe constraints like + `prod.u0 < eq.u0` which cause problems later on when it is assumed that + `eq.u0 = Coq.Relations.Relation_Definitions.1 <= prod.u0` by + `returnM_injective`. The easiest solution is just to not use `f_equal` + here, and rewrite by the relevant induction hypotheses instead. *) + all: try rewrite IHD; try rewrite IHD1; try rewrite IHD2; try rewrite H; try easy. (* All that remains is the IRT_BVVec case, which requires functional extensionality and the fact that genBVVec and atBVVec define an isomorphism *) intros; rewrite <- (gen_at_BVVec _ _ _ u). From 07481e125eb92d2ea54a5d601b693dc261eec02e Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 14 Oct 2021 15:29:48 -0700 Subject: [PATCH 2/2] Add a Coq source file that just imports everything else. The purpose of this is to catch the situation where we have a latent universe inconsistency. --- saw-core-coq/coq/_CoqProject | 2 ++ .../coq/handwritten/CryptolToCoq/Everything.v | 17 +++++++++++++++++ 2 files changed, 19 insertions(+) create mode 100644 saw-core-coq/coq/handwritten/CryptolToCoq/Everything.v diff --git a/saw-core-coq/coq/_CoqProject b/saw-core-coq/coq/_CoqProject index 05fc311a82..36e05a2881 100644 --- a/saw-core-coq/coq/_CoqProject +++ b/saw-core-coq/coq/_CoqProject @@ -13,3 +13,5 @@ handwritten/CryptolToCoq/SAWCorePrelude_proofs.v handwritten/CryptolToCoq/SAWCorePreludeExtra.v handwritten/CryptolToCoq/SAWCoreScaffolding.v handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v + +handwritten/CryptolToCoq/Everything.v diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/Everything.v b/saw-core-coq/coq/handwritten/CryptolToCoq/Everything.v new file mode 100644 index 0000000000..158d66d2b8 --- /dev/null +++ b/saw-core-coq/coq/handwritten/CryptolToCoq/Everything.v @@ -0,0 +1,17 @@ +(* This file imports everything together in order to make sure + that there are no universe inconsistencies *) + +(* generated *) +From CryptolToCoq Require Import CryptolPrimitivesForSAWCore. +From CryptolToCoq Require Import SAWCorePrelude. + +(* handwritten *) +From CryptolToCoq Require Import CompM. +From CryptolToCoq Require Import CompMExtra. +From CryptolToCoq Require Import CoqVectorsExtra. +From CryptolToCoq Require Import CryptolPrimitivesForSAWCoreExtra. +From CryptolToCoq Require Import SAWCoreBitvectors. +From CryptolToCoq Require Import SAWCorePrelude_proofs. +From CryptolToCoq Require Import SAWCorePreludeExtra. +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.