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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
/// An `Int` literal for Lean source: negatives parenthesised so `.i64Const -7`
/// does not misparse; non-negatives bare (byte-identical to the shipped `0`).
fn lean_int_lit(k: i64) -> String {
if k < 0 {
format!("({k})")
} else {
k.to_string()
}
}
/// `i128` variant for anti-vacuity guard values, which can exceed `i64` for a
/// multiplication recursion (`Int` in Lean is unbounded, so the wide value is a
/// faithful guard).
fn lean_int_lit128(k: i128) -> String {
if k < 0 {
format!("({k})")
} else {
k.to_string()
}
}
/// The `CodeTbl` VALUE (the `fun fn => ...` lambda, no `def` wrapper) a
/// certified body decodes to. This is the term the checker splices, verbatim,
/// into `CheckerWitness.lean` and pins with `rfl` against
/// `manifest.obligations.map (·.code)`, so a `{name}Code` def in the cert's
/// `Module.lean` that diverges from the bytes fails the kernel witness. Kept
/// byte-identical to the RHS `render_code_def` emits so the emitted `Module.lean`
/// is unchanged.
fn render_code_value(c: &Cert) -> String {
match c.inner() {
Cert::Recursive {
self_idx,
nlocals,
carrier,
box_idx,
add_idx,
sub_idx,
base_k,
rec_first,
other,
..
} => {
let base = lean_int_lit(*base_k);
// The step arm pushes the two `add` operands (the recursive result and
// the other operand) in their recognised order, then calls `add`.
let rec_ops = format!(
".localGet 0, .i64Const 1, .call {box_idx}, .call {sub_idx}, .call {self_idx}"
);
let other_ops = match other {
BodyOperand::Input => ".localGet 0".to_string(),
BodyOperand::Const(k) => format!(".i64Const {}, .call {box_idx}", lean_int_lit(*k)),
};
let (a_ops, b_ops) = if *rec_first {
(&rec_ops, &other_ops)
} else {
(&other_ops, &rec_ops)
};
let step = format!("{a_ops}, {b_ops}, .call {add_idx}");
format!(
"fun fn =>\n \
if fn = {self_idx} then some ⟨1, {nlocals},\n \
[ .localGet 0, .structGet {carrier} 1, .refIsNull,\n \
.ifElse [.localGet 0, .structGet {carrier} 0, .i64Const 0, .i64LeS]\n \
[.localGet 0, .structGet {carrier} 2, .i32Const 0, .i32LtS],\n \
.ifElse [.i64Const {base}, .call {box_idx}]\n \
[{step}] ]⟩\n else none",
)
}
Cert::AccumulatorRecursive {
self_idx,
nlocals,
carrier,
box_idx,
add_idx,
sub_idx,
..
} => format!(
"fun fn =>\n \
if fn = {self_idx} then some ⟨2, {nlocals},\n \
[ .localGet 0, .structGet {carrier} 1, .refIsNull,\n \
.ifElse [.localGet 0, .structGet {carrier} 0, .i64Const 0, .i64LeS]\n \
[.localGet 0, .structGet {carrier} 2, .i32Const 0, .i32LtS],\n \
.ifElse [.localGet 1]\n \
[.localGet 0, .i64Const 1, .call {box_idx}, .call {sub_idx}, \
.localGet 1, .localGet 0, .call {add_idx}, .returnCall {self_idx}] ]⟩\n else none",
),
Cert::AdtConstructor {
self_idx,
nlocals,
ops,
..
}
| Cert::FieldProjection {
self_idx,
nlocals,
ops,
..
}
| Cert::WidenedIntMatch {
self_idx,
nlocals,
ops,
..
}
| Cert::VerbatimWidenedMatch {
self_idx,
nlocals,
ops,
..
}
| Cert::VerbatimVariantDispatch {
self_idx,
nlocals,
ops,
..
}
| Cert::StringEqVerbatimMatch {
self_idx,
nlocals,
ops,
..
}
| Cert::StringConcatVerbatimMatch {
self_idx,
nlocals,
ops,
..
}
| Cert::ExprFragment {
self_idx,
nlocals,
ops,
..
}
| Cert::VariantDispatch {
self_idx,
nlocals,
ops,
..
} => format!(
"fun fn =>\n \
if fn = {self_idx} then some ⟨{arity}, {nlocals}, {body}⟩ else none",
arity = c.arity(),
body = render_ops_value(ops),
),
Cert::Composition { closure, .. } => render_closure_code_value(closure),
// Shared code table over the whole SCC: one `if fn = self then …` arm per
// member, in `self_idx` order. Each arm is the fixed mutual body shape
// (base boxes the member's literal; the else tail-calls the member's
// cross target on `n-1`) — the same lossless template `Cert::Recursive`
// uses, so it is byte-identical to the recognised bytes and to the term
// the checker re-derives.
Cert::MutualRecursion {
scc,
carrier,
box_idx,
sub_idx,
..
} => {
let mut s = String::from("fun fn =>\n ");
for (i, m) in scc.iter().enumerate() {
let kw = if i == 0 { "if" } else { "else if" };
let base = lean_int_lit(m.base_k);
s.push_str(&format!(
"{kw} fn = {self_idx} then some ⟨1, {nlocals},\n \
[ .localGet 0, .structGet {carrier} 1, .refIsNull,\n \
.ifElse [.localGet 0, .structGet {carrier} 0, .i64Const 0, .i64LeS]\n \
[.localGet 0, .structGet {carrier} 2, .i32Const 0, .i32LtS],\n \
.ifElse [.i64Const {base}, .call {box_idx}]\n \
[.localGet 0, .i64Const 1, .call {box_idx}, .call {sub_idx}, .returnCall {cross}] ]⟩\n ",
self_idx = m.self_idx,
nlocals = m.nlocals,
cross = m.cross_idx,
));
}
s.push_str("else none");
s
}
Cert::NonRecursive { .. } => unreachable!(),
}
}
/// The multi-entry `CodeTbl` VALUE for a composition: one `if fn = i then …`
/// arm per function in the caller's whole call closure, in `self_idx` order.
/// The checker re-derives this from the bytes and pins the WHOLE table with one
/// `rfl`, so every callee body the caller's proof reduces through is byte-bound.
fn render_closure_code_value(closure: &[ClosureEntry]) -> String {
let mut s = String::from("fun fn =>\n ");
for (i, e) in closure.iter().enumerate() {
let kw = if i == 0 { "if" } else { "else if" };
s.push_str(&format!(
"{kw} fn = {idx} then some ⟨1, {nlocals}, {body}⟩\n ",
idx = e.self_idx,
nlocals = e.nlocals,
body = render_ops_value(&e.ops),
));
}
s.push_str("else none");
s
}
/// The host-table arms for a composition closure: each carrier-`add` helper the
/// closure calls wired to the `add` contract parameter, terminated by `none`.
/// v1 leaves consume only `add`; the arms grow with the leaf vocabulary.
fn compose_host_arms(closure: &[ClosureEntry]) -> String {
let mut adds: Vec<u32> = closure
.iter()
.filter_map(|e| match e.shape {
LeafShape::SelfSum { add_idx } => Some(add_idx),
LeafShape::Chain { .. } => None,
})
.collect();
adds.sort_unstable();
adds.dedup();
let mut s = String::new();
for (i, a) in adds.iter().enumerate() {
let kw = if i == 0 { "if" } else { "else if" };
s.push_str(&format!("{kw} fn = {a} then some (2, add)\n "));
}
s.push_str("else none");
s
}