Skip to content

Commit 879485b

Browse files
chathhorn-galoischathhorn-galois
committed
saw-core-coq: remove duplicate imports.
1 parent 7bdbdaa commit 879485b

12 files changed

+0
-241
lines changed

‎otherTests/saw-core-coq/test_arithmetic.log.good‎

Lines changed: 0 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
15-
Import CryptolPrimitivesForSAWCore.
1614

1715

1816
(** Code generated by saw-core-coq *)
@@ -39,9 +37,7 @@ Import VectorNotations.
3937

4038
(** Post-preamble section specified by you *)
4139
From CryptolToCoq Require Import SAWCorePrelude.
42-
Import SAWCorePrelude.
4340
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
44-
Import CryptolPrimitivesForSAWCore.
4541

4642

4743
(** Code generated by saw-core-coq *)
@@ -66,9 +62,7 @@ Import VectorNotations.
6662

6763
(** Post-preamble section specified by you *)
6864
From CryptolToCoq Require Import SAWCorePrelude.
69-
Import SAWCorePrelude.
7065
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
71-
Import CryptolPrimitivesForSAWCore.
7266

7367

7468
(** Code generated by saw-core-coq *)
@@ -93,9 +87,7 @@ Import VectorNotations.
9387

9488
(** Post-preamble section specified by you *)
9589
From CryptolToCoq Require Import SAWCorePrelude.
96-
Import SAWCorePrelude.
9790
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
98-
Import CryptolPrimitivesForSAWCore.
9991

10092

10193
(** Code generated by saw-core-coq *)
@@ -120,9 +112,7 @@ Import VectorNotations.
120112

121113
(** Post-preamble section specified by you *)
122114
From CryptolToCoq Require Import SAWCorePrelude.
123-
Import SAWCorePrelude.
124115
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
125-
Import CryptolPrimitivesForSAWCore.
126116

127117

128118
(** Code generated by saw-core-coq *)
@@ -148,9 +138,7 @@ Import VectorNotations.
148138

149139
(** Post-preamble section specified by you *)
150140
From CryptolToCoq Require Import SAWCorePrelude.
151-
Import SAWCorePrelude.
152141
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
153-
Import CryptolPrimitivesForSAWCore.
154142

155143

156144
(** Code generated by saw-core-coq *)
@@ -175,9 +163,7 @@ Import VectorNotations.
175163

176164
(** Post-preamble section specified by you *)
177165
From CryptolToCoq Require Import SAWCorePrelude.
178-
Import SAWCorePrelude.
179166
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
180-
Import CryptolPrimitivesForSAWCore.
181167

182168

183169
(** Code generated by saw-core-coq *)
@@ -201,9 +187,7 @@ Import VectorNotations.
201187

202188
(** Post-preamble section specified by you *)
203189
From CryptolToCoq Require Import SAWCorePrelude.
204-
Import SAWCorePrelude.
205190
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
206-
Import CryptolPrimitivesForSAWCore.
207191

208192

209193
(** Code generated by saw-core-coq *)
@@ -227,9 +211,7 @@ Import VectorNotations.
227211

228212
(** Post-preamble section specified by you *)
229213
From CryptolToCoq Require Import SAWCorePrelude.
230-
Import SAWCorePrelude.
231214
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
232-
Import CryptolPrimitivesForSAWCore.
233215

234216

235217
(** Code generated by saw-core-coq *)
@@ -252,9 +234,7 @@ Import VectorNotations.
252234

253235
(** Post-preamble section specified by you *)
254236
From CryptolToCoq Require Import SAWCorePrelude.
255-
Import SAWCorePrelude.
256237
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
257-
Import CryptolPrimitivesForSAWCore.
258238

259239

260240
(** Code generated by saw-core-coq *)
@@ -277,9 +257,7 @@ Import VectorNotations.
277257

278258
(** Post-preamble section specified by you *)
279259
From CryptolToCoq Require Import SAWCorePrelude.
280-
Import SAWCorePrelude.
281260
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
282-
Import CryptolPrimitivesForSAWCore.
283261

284262

285263
(** Code generated by saw-core-coq *)
@@ -317,9 +295,7 @@ Import VectorNotations.
317295

318296
(** Post-preamble section specified by you *)
319297
From CryptolToCoq Require Import SAWCorePrelude.
320-
Import SAWCorePrelude.
321298
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
322-
Import CryptolPrimitivesForSAWCore.
323299

324300

325301
(** Code generated by saw-core-coq *)

‎otherTests/saw-core-coq/test_boolean.log.good‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
15-
Import CryptolPrimitivesForSAWCore.
1614

1715

1816
(** Code generated by saw-core-coq *)
@@ -34,9 +32,7 @@ Import VectorNotations.
3432

3533
(** Post-preamble section specified by you *)
3634
From CryptolToCoq Require Import SAWCorePrelude.
37-
Import SAWCorePrelude.
3835
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
39-
Import CryptolPrimitivesForSAWCore.
4036

4137

4238
(** Code generated by saw-core-coq *)
@@ -59,9 +55,7 @@ Import VectorNotations.
5955

6056
(** Post-preamble section specified by you *)
6157
From CryptolToCoq Require Import SAWCorePrelude.
62-
Import SAWCorePrelude.
6358
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
64-
Import CryptolPrimitivesForSAWCore.
6559

6660

6761
(** Code generated by saw-core-coq *)
@@ -90,9 +84,7 @@ Import VectorNotations.
9084

9185
(** Post-preamble section specified by you *)
9286
From CryptolToCoq Require Import SAWCorePrelude.
93-
Import SAWCorePrelude.
9487
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
95-
Import CryptolPrimitivesForSAWCore.
9688

9789

9890
(** Code generated by saw-core-coq *)
@@ -117,9 +109,7 @@ Import VectorNotations.
117109

118110
(** Post-preamble section specified by you *)
119111
From CryptolToCoq Require Import SAWCorePrelude.
120-
Import SAWCorePrelude.
121112
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
122-
Import CryptolPrimitivesForSAWCore.
123113

124114

125115
(** Code generated by saw-core-coq *)

‎otherTests/saw-core-coq/test_cryptol_module_simple.log.good‎

Lines changed: 0 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -1,57 +1 @@
11
Loading file "test_cryptol_module_simple.saw"
2-
3-
(** Mandatory imports from saw-core-coq *)
4-
From Stdlib Require Import Lists.List.
5-
From Stdlib Require Import String.
6-
From Stdlib Require Import Vectors.Vector.
7-
From CryptolToCoq Require Import SAWCoreScaffolding.
8-
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
9-
Import VectorNotations.
10-
11-
(** Post-preamble section specified by you *)
12-
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
14-
From CryptolToCoq Require Import SAWCorePreludeExtra.
15-
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
16-
Import CryptolPrimitivesForSAWCore.
17-
From CryptolToCoq Require Import CryptolPrimitivesForSAWCoreExtra.
18-
19-
20-
(** Code generated by saw-core-coq *)
21-
22-
Section Simple .
23-
Definition addOne (x : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool :=
24-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
25-
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in
26-
CryptolPrimitivesForSAWCore.ecPlus var__1 (CryptolPrimitivesForSAWCore.PRingSeqBool var__0) x (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 (CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0)).
27-
28-
Definition addTwo (x : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (y : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool :=
29-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
30-
CryptolPrimitivesForSAWCore.ecPlus (CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool) (CryptolPrimitivesForSAWCore.PRingSeqBool var__0) x y.
31-
32-
Definition isZero (x : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) : Init.Datatypes.bool :=
33-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
34-
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in
35-
CryptolPrimitivesForSAWCore.ecEq var__1 (CryptolPrimitivesForSAWCore.PEqSeqBool var__0) x (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum SAWCoreScaffolding.Zero) var__1 (CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0)).
36-
37-
Definition maxVal (x : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (y : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool :=
38-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
39-
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in
40-
if CryptolPrimitivesForSAWCore.ecGt var__1 (CryptolPrimitivesForSAWCore.PCmpSeqBool var__0) x y then x else y.
41-
42-
Definition encrypt (a : CryptolPrimitivesForSAWCore.Num) (key : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (plaintext : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) :=
43-
let var__0 := CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool in
44-
CryptolPrimitivesForSAWCore.seqMap var__0 var__0 a (fun (pt : var__0) => let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
45-
CryptolPrimitivesForSAWCore.ecXor var__0 (CryptolPrimitivesForSAWCore.PLogicSeqBool var__1) pt key) plaintext.
46-
47-
Definition decrypt (a : CryptolPrimitivesForSAWCore.Num) (key : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (ciphertext : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : CryptolPrimitivesForSAWCore.seq a (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) :=
48-
let var__0 := CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool in
49-
CryptolPrimitivesForSAWCore.seqMap var__0 var__0 a (fun (ct : var__0) => let var__1 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
50-
CryptolPrimitivesForSAWCore.ecXor var__0 (CryptolPrimitivesForSAWCore.PLogicSeqBool var__1) ct key) ciphertext.
51-
52-
Definition roundtrip (u1266 : CryptolPrimitivesForSAWCore.Num) (k : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool) (ip : CryptolPrimitivesForSAWCore.seq u1266 (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) Init.Datatypes.bool)) : Init.Datatypes.bool :=
53-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
54-
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in
55-
CryptolPrimitivesForSAWCore.ecEq (CryptolPrimitivesForSAWCore.seq u1266 var__1) (CryptolPrimitivesForSAWCore.PEqSeq u1266 var__1 (CryptolPrimitivesForSAWCore.PEqSeqBool var__0)) (decrypt u1266 k (encrypt u1266 k ip)) ip.
56-
57-
End Simple .

‎otherTests/saw-core-coq/test_cryptol_primitives.log.good‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import SAWCorePreludeExtra.
1514

1615

‎otherTests/saw-core-coq/test_lambda.log.good‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,7 @@ Import VectorNotations.
1010

1111
(** Post-preamble section specified by you *)
1212
From CryptolToCoq Require Import SAWCorePrelude.
13-
Import SAWCorePrelude.
1413
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
15-
Import CryptolPrimitivesForSAWCore.
1614

1715

1816
(** Code generated by saw-core-coq *)
@@ -38,9 +36,7 @@ Import VectorNotations.
3836

3937
(** Post-preamble section specified by you *)
4038
From CryptolToCoq Require Import SAWCorePrelude.
41-
Import SAWCorePrelude.
4239
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
43-
Import CryptolPrimitivesForSAWCore.
4440

4541

4642
(** Code generated by saw-core-coq *)
@@ -66,9 +62,7 @@ Import VectorNotations.
6662

6763
(** Post-preamble section specified by you *)
6864
From CryptolToCoq Require Import SAWCorePrelude.
69-
Import SAWCorePrelude.
7065
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
71-
Import CryptolPrimitivesForSAWCore.
7266

7367

7468
(** Code generated by saw-core-coq *)
@@ -93,9 +87,7 @@ Import VectorNotations.
9387

9488
(** Post-preamble section specified by you *)
9589
From CryptolToCoq Require Import SAWCorePrelude.
96-
Import SAWCorePrelude.
9790
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
98-
Import CryptolPrimitivesForSAWCore.
9991

10092

10193
(** Code generated by saw-core-coq *)
@@ -123,9 +115,7 @@ Import VectorNotations.
123115

124116
(** Post-preamble section specified by you *)
125117
From CryptolToCoq Require Import SAWCorePrelude.
126-
Import SAWCorePrelude.
127118
From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
128-
Import CryptolPrimitivesForSAWCore.
129119

130120

131121
(** Code generated by saw-core-coq *)

0 commit comments

Comments
 (0)