Skip to content

Commit 7bdbdaa

Browse files
chathhorn-galoischathhorn-galois
committed
saw-core-coq: updated expected test output.
1 parent 1a77f86 commit 7bdbdaa

12 files changed

+1503
-1503
lines changed

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

Lines changed: 89 additions & 89 deletions
Large diffs are not rendered by default.

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

Lines changed: 33 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
Loading file "test_boolean.saw"
22

33
(** Mandatory imports from saw-core-coq *)
4-
From Coq Require Import Lists.List.
5-
From Coq Require Import String.
6-
From Coq Require Import Vectors.Vector.
4+
From Stdlib Require Import Lists.List.
5+
From Stdlib Require Import String.
6+
From Stdlib Require Import Vectors.Vector.
77
From CryptolToCoq Require Import SAWCoreScaffolding.
88
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
99
Import VectorNotations.
@@ -20,14 +20,14 @@ Import CryptolPrimitivesForSAWCore.
2020

2121

2222

23-
Definition TestBool : Coq.Init.Datatypes.bool :=
24-
CryptolPrimitivesForSAWCore.ecEq Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PEqBit (CryptolPrimitivesForSAWCore.ecOr Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecAnd Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Coq.Init.Datatypes.true Coq.Init.Datatypes.false) (CryptolPrimitivesForSAWCore.ecCompl Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Coq.Init.Datatypes.true)) Coq.Init.Datatypes.true.
23+
Definition TestBool : Init.Datatypes.bool :=
24+
CryptolPrimitivesForSAWCore.ecEq Init.Datatypes.bool CryptolPrimitivesForSAWCore.PEqBit (CryptolPrimitivesForSAWCore.ecOr Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecAnd Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Init.Datatypes.true Init.Datatypes.false) (CryptolPrimitivesForSAWCore.ecCompl Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Init.Datatypes.true)) Init.Datatypes.true.
2525

2626

2727
(** Mandatory imports from saw-core-coq *)
28-
From Coq Require Import Lists.List.
29-
From Coq Require Import String.
30-
From Coq Require Import Vectors.Vector.
28+
From Stdlib Require Import Lists.List.
29+
From Stdlib Require Import String.
30+
From Stdlib Require Import Vectors.Vector.
3131
From CryptolToCoq Require Import SAWCoreScaffolding.
3232
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
3333
Import VectorNotations.
@@ -44,15 +44,15 @@ Import CryptolPrimitivesForSAWCore.
4444

4545

4646

47-
Definition TestBool_NestedOps : Coq.Init.Datatypes.bool :=
48-
let var__0 := CryptolPrimitivesForSAWCore.ecEq Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PEqBit (CryptolPrimitivesForSAWCore.ecOr Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecAnd Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Coq.Init.Datatypes.true Coq.Init.Datatypes.false) (CryptolPrimitivesForSAWCore.ecCompl Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Coq.Init.Datatypes.true)) Coq.Init.Datatypes.true in
49-
CryptolPrimitivesForSAWCore.ecNotEq Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PEqBit (CryptolPrimitivesForSAWCore.ecXor Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecOr Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecAnd Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit var__0 var__0) (CryptolPrimitivesForSAWCore.ecCompl Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecCompl Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit var__0))) var__0) Coq.Init.Datatypes.true.
47+
Definition TestBool_NestedOps : Init.Datatypes.bool :=
48+
let var__0 := CryptolPrimitivesForSAWCore.ecEq Init.Datatypes.bool CryptolPrimitivesForSAWCore.PEqBit (CryptolPrimitivesForSAWCore.ecOr Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecAnd Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Init.Datatypes.true Init.Datatypes.false) (CryptolPrimitivesForSAWCore.ecCompl Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit Init.Datatypes.true)) Init.Datatypes.true in
49+
CryptolPrimitivesForSAWCore.ecNotEq Init.Datatypes.bool CryptolPrimitivesForSAWCore.PEqBit (CryptolPrimitivesForSAWCore.ecXor Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecOr Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecAnd Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit var__0 var__0) (CryptolPrimitivesForSAWCore.ecCompl Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecCompl Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit var__0))) var__0) Init.Datatypes.true.
5050

5151

5252
(** Mandatory imports from saw-core-coq *)
53-
From Coq Require Import Lists.List.
54-
From Coq Require Import String.
55-
From Coq Require Import Vectors.Vector.
53+
From Stdlib Require Import Lists.List.
54+
From Stdlib Require Import String.
55+
From Stdlib Require Import Vectors.Vector.
5656
From CryptolToCoq Require Import SAWCoreScaffolding.
5757
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
5858
Import VectorNotations.
@@ -69,21 +69,21 @@ Import CryptolPrimitivesForSAWCore.
6969

7070

7171

72-
Definition TestBool_Comparison : Coq.Init.Datatypes.bool :=
73-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH)))) in
74-
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Coq.Init.Datatypes.bool in
72+
Definition TestBool_Comparison : Init.Datatypes.bool :=
73+
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
74+
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in
7575
let var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 in
76-
let var__3 := CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xI (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH)))) in
77-
let var__4 := CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xI (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH))) in
76+
let var__3 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) in
77+
let var__4 := CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) in
7878
let var__5 := CryptolPrimitivesForSAWCore.ecNumber var__3 SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PLiteralInteger in
7979
let var__6 := CryptolPrimitivesForSAWCore.ecNumber var__4 SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PLiteralInteger in
80-
CryptolPrimitivesForSAWCore.ecAnd Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecLt var__1 (CryptolPrimitivesForSAWCore.PCmpSeqBool var__0) (CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2) (CryptolPrimitivesForSAWCore.ecNumber var__4 var__1 var__2)) (CryptolPrimitivesForSAWCore.ecAnd Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecGt SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PCmpInteger var__5 var__6) (CryptolPrimitivesForSAWCore.ecAnd Coq.Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecLtEq SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PCmpInteger var__6 var__5) (CryptolPrimitivesForSAWCore.ecGtEq SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PCmpInteger var__5 var__6))).
80+
CryptolPrimitivesForSAWCore.ecAnd Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecLt var__1 (CryptolPrimitivesForSAWCore.PCmpSeqBool var__0) (CryptolPrimitivesForSAWCore.ecNumber var__3 var__1 var__2) (CryptolPrimitivesForSAWCore.ecNumber var__4 var__1 var__2)) (CryptolPrimitivesForSAWCore.ecAnd Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecGt SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PCmpInteger var__5 var__6) (CryptolPrimitivesForSAWCore.ecAnd Init.Datatypes.bool CryptolPrimitivesForSAWCore.PLogicBit (CryptolPrimitivesForSAWCore.ecLtEq SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PCmpInteger var__6 var__5) (CryptolPrimitivesForSAWCore.ecGtEq SAWCoreScaffolding.Integer CryptolPrimitivesForSAWCore.PCmpInteger var__5 var__6))).
8181

8282

8383
(** Mandatory imports from saw-core-coq *)
84-
From Coq Require Import Lists.List.
85-
From Coq Require Import String.
86-
From Coq Require Import Vectors.Vector.
84+
From Stdlib Require Import Lists.List.
85+
From Stdlib Require Import String.
86+
From Stdlib Require Import Vectors.Vector.
8787
From CryptolToCoq Require Import SAWCoreScaffolding.
8888
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
8989
Import VectorNotations.
@@ -101,16 +101,16 @@ Import CryptolPrimitivesForSAWCore.
101101

102102

103103
Definition TestBool_Ite1 (u1217 : Type) {Inh_u1217 : SAWCoreScaffolding.Inhabited u1217} (_P : CryptolPrimitivesForSAWCore.PLiteral u1217) : u1217 :=
104-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH)))) in
105-
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Coq.Init.Datatypes.bool in
104+
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
105+
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in
106106
let var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 in
107-
if CryptolPrimitivesForSAWCore.ecLt var__1 (CryptolPrimitivesForSAWCore.PCmpSeqBool var__0) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xI (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH)))) var__1 var__2) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xI (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH))))) var__1 var__2) then CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat Coq.PArith.BinPos.xH)) u1217 _P else CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH))) u1217 _P.
107+
if CryptolPrimitivesForSAWCore.ecLt var__1 (CryptolPrimitivesForSAWCore.PCmpSeqBool var__0) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH)))) var__1 var__2) (CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO (Stdlib.PArith.BinPos.xI (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))))) var__1 var__2) then CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) u1217 _P else CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) u1217 _P.
108108

109109

110110
(** Mandatory imports from saw-core-coq *)
111-
From Coq Require Import Lists.List.
112-
From Coq Require Import String.
113-
From Coq Require Import Vectors.Vector.
111+
From Stdlib Require Import Lists.List.
112+
From Stdlib Require Import String.
113+
From Stdlib Require Import Vectors.Vector.
114114
From CryptolToCoq Require Import SAWCoreScaffolding.
115115
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
116116
Import VectorNotations.
@@ -127,9 +127,9 @@ Import CryptolPrimitivesForSAWCore.
127127

128128

129129

130-
Definition TestBool_Ite2 : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH))))) Coq.Init.Datatypes.bool :=
131-
let var__0 := CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH)))) in
132-
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Coq.Init.Datatypes.bool in
130+
Definition TestBool_Ite2 : 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 :=
131+
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
132+
let var__1 := CryptolPrimitivesForSAWCore.seq var__0 Init.Datatypes.bool in
133133
let var__2 := CryptolPrimitivesForSAWCore.PLiteralSeqBool var__0 in
134-
if Coq.Init.Datatypes.true then if Coq.Init.Datatypes.false then CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat Coq.PArith.BinPos.xH)) var__1 var__2 else CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xO Coq.PArith.BinPos.xH))) var__1 var__2 else CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Coq.PArith.BinPos.Pos.to_nat (Coq.PArith.BinPos.xI Coq.PArith.BinPos.xH))) var__1 var__2.
134+
if Init.Datatypes.true then if Init.Datatypes.false then CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat Stdlib.PArith.BinPos.xH)) var__1 var__2 else CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xO Stdlib.PArith.BinPos.xH))) var__1 var__2 else CryptolPrimitivesForSAWCore.ecNumber (CryptolPrimitivesForSAWCore.TCNum (Stdlib.PArith.BinPos.Pos.to_nat (Stdlib.PArith.BinPos.xI Stdlib.PArith.BinPos.xH))) var__1 var__2.
135135

0 commit comments

Comments
 (0)