blob: 937a15e53afbd56bf81fb2c59ffe3c531c36b9c7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [constants]
import Base.Primitives
structure OpaqueDefs where
/- [constants::X0] -/
def x0_body : Result UInt32 := Result.ret (UInt32.ofNatCore 0 (by intlit))
def x0_c : UInt32 := eval_global x0_body (by simp)
/- [core::num::u32::{9}::MAX] -/
def core_num_u32_max_body : Result UInt32 :=
Result.ret (UInt32.ofNatCore 4294967295 (by intlit))
def core_num_u32_max_c : UInt32 :=
eval_global core_num_u32_max_body (by simp)
/- [constants::X1] -/
def x1_body : Result UInt32 := Result.ret core_num_u32_max_c
def x1_c : UInt32 := eval_global x1_body (by simp)
/- [constants::X2] -/
def x2_body : Result UInt32 := Result.ret (UInt32.ofNatCore 3 (by intlit))
def x2_c : UInt32 := eval_global x2_body (by simp)
/- [constants::incr] -/
def incr_fwd (n : UInt32) : Result UInt32 :=
UInt32.checked_add n (UInt32.ofNatCore 1 (by intlit))
/- [constants::X3] -/
def x3_body : Result UInt32 := incr_fwd (UInt32.ofNatCore 32 (by intlit))
def x3_c : UInt32 := eval_global x3_body (by simp)
/- [constants::mk_pair0] -/
def mk_pair0_fwd (x : UInt32) (y : UInt32) : Result (UInt32 × UInt32) :=
Result.ret (x, y)
/- [constants::Pair] -/
structure pair_t (T1 T2 : Type) where
pair_x : T1
pair_y : T2
/- [constants::mk_pair1] -/
def mk_pair1_fwd (x : UInt32) (y : UInt32) : Result (pair_t UInt32 UInt32) :=
Result.ret { pair_x := x, pair_y := y }
/- [constants::P0] -/
def p0_body : Result (UInt32 × UInt32) :=
mk_pair0_fwd (UInt32.ofNatCore 0 (by intlit))
(UInt32.ofNatCore 1 (by intlit))
def p0_c : (UInt32 × UInt32) := eval_global p0_body (by simp)
/- [constants::P1] -/
def p1_body : Result (pair_t UInt32 UInt32) :=
mk_pair1_fwd (UInt32.ofNatCore 0 (by intlit))
(UInt32.ofNatCore 1 (by intlit))
def p1_c : pair_t UInt32 UInt32 := eval_global p1_body (by simp)
/- [constants::P2] -/
def p2_body : Result (UInt32 × UInt32) :=
Result.ret
((UInt32.ofNatCore 0 (by intlit)),
(UInt32.ofNatCore 1 (by intlit)))
def p2_c : (UInt32 × UInt32) := eval_global p2_body (by simp)
/- [constants::P3] -/
def p3_body : Result (pair_t UInt32 UInt32) :=
Result.ret
{
pair_x := (UInt32.ofNatCore 0 (by intlit)),
pair_y := (UInt32.ofNatCore 1 (by intlit))
}
def p3_c : pair_t UInt32 UInt32 := eval_global p3_body (by simp)
/- [constants::Wrap] -/
structure wrap_t (T : Type) where
wrap_val : T
/- [constants::Wrap::{0}::new] -/
def wrap_new_fwd (T : Type) (val : T) : Result (wrap_t T) :=
Result.ret { wrap_val := val }
/- [constants::Y] -/
def y_body : Result (wrap_t Int32) :=
wrap_new_fwd Int32 (Int32.ofNatCore 2 (by intlit))
def y_c : wrap_t Int32 := eval_global y_body (by simp)
/- [constants::unwrap_y] -/
def unwrap_y_fwd : Result Int32 :=
Result.ret y_c.wrap_val
/- [constants::YVAL] -/
def yval_body : Result Int32 := unwrap_y_fwd
def yval_c : Int32 := eval_global yval_body (by simp)
/- [constants::get_z1::Z1] -/
def get_z1_z1_body : Result Int32 :=
Result.ret (Int32.ofNatCore 3 (by intlit))
def get_z1_z1_c : Int32 := eval_global get_z1_z1_body (by simp)
/- [constants::get_z1] -/
def get_z1_fwd : Result Int32 :=
Result.ret get_z1_z1_c
/- [constants::add] -/
def add_fwd (a : Int32) (b : Int32) : Result Int32 :=
Int32.checked_add a b
/- [constants::Q1] -/
def q1_body : Result Int32 := Result.ret (Int32.ofNatCore 5 (by intlit))
def q1_c : Int32 := eval_global q1_body (by simp)
/- [constants::Q2] -/
def q2_body : Result Int32 := Result.ret q1_c
def q2_c : Int32 := eval_global q2_body (by simp)
/- [constants::Q3] -/
def q3_body : Result Int32 := add_fwd q2_c (Int32.ofNatCore 3 (by intlit))
def q3_c : Int32 := eval_global q3_body (by simp)
/- [constants::get_z2] -/
def get_z2_fwd : Result Int32 :=
do
let i ← get_z1_fwd
let i0 ← add_fwd i q3_c
add_fwd q1_c i0
/- [constants::S1] -/
def s1_body : Result UInt32 := Result.ret (UInt32.ofNatCore 6 (by intlit))
def s1_c : UInt32 := eval_global s1_body (by simp)
/- [constants::S2] -/
def s2_body : Result UInt32 := incr_fwd s1_c
def s2_c : UInt32 := eval_global s2_body (by simp)
/- [constants::S3] -/
def s3_body : Result (pair_t UInt32 UInt32) := Result.ret p3_c
def s3_c : pair_t UInt32 UInt32 := eval_global s3_body (by simp)
/- [constants::S4] -/
def s4_body : Result (pair_t UInt32 UInt32) :=
mk_pair1_fwd (UInt32.ofNatCore 7 (by intlit))
(UInt32.ofNatCore 8 (by intlit))
def s4_c : pair_t UInt32 UInt32 := eval_global s4_body (by simp)
|
