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
/// Symbolically execute a body-consumed fuel recursion's step arm — a
/// straight-line stack program ending in the host `add` — and recover
/// `(sub, add, rec_first, other)`: which host helpers are the descent/combinator,
/// which side of the `add` the recursive result sits on, and what the other
/// operand is. The descent is pinned to `sub(input, box 1)` = `n-1`; anything the
/// evaluator cannot account for (foreign locals, a second add, a non-descent
/// self-call argument) fails, so the recogniser stays fail-closed.
fn parse_body_step(
ops: &[Op],
box_idx: u32,
self_idx: u32,
host_roles: &std::collections::HashMap<u32, HostRole>,
) -> Option<(u32, u32, bool, BodyOperand)> {
use Op::*;
#[derive(Clone, Copy, PartialEq)]
enum V {
Input,
IntLit(i64),
Boxed(i64),
Descent,
Rec,
}
// The step is `<push operand A> <push operand B> add`; the trailing `add`
// combines the top two stack values.
let (last, init) = ops.split_last()?;
let Call(add_idx) = last else { return None };
if !matches!(
host_roles.get(add_idx),
Some(HostRole::Add) | Some(HostRole::Mul)
) {
return None;
}
let mut st: Vec<V> = Vec::new();
let mut sub_idx: Option<u32> = None;
for op in init {
match op {
LocalGet(0) => st.push(V::Input),
I64Const(k) => st.push(V::IntLit(*k)),
Call(idx) if *idx == box_idx => {
let V::IntLit(k) = st.pop()? else { return None };
st.push(V::Boxed(k));
}
Call(idx) if *idx == self_idx => {
if st.pop()? != V::Descent {
return None;
}
st.push(V::Rec);
}
Call(idx) if host_roles.get(idx) == Some(&HostRole::Sub) => {
let b = st.pop()?;
let a = st.pop()?;
if a != V::Input || b != V::Boxed(1) {
return None;
}
if sub_idx.is_some_and(|s| s != *idx) {
return None;
}
sub_idx = Some(*idx);
st.push(V::Descent);
}
_ => return None,
}
}
// exactly the two `add` operands remain.
let [a, b] = st.as_slice() else { return None };
let operand = |v: &V| match v {
V::Input => Some(BodyOperand::Input),
V::Boxed(k) => Some(BodyOperand::Const(*k)),
_ => None,
};
let (rec_first, other) = if *a == V::Rec {
(true, operand(b)?)
} else if *b == V::Rec {
(false, operand(a)?)
} else {
return None;
};
Some((sub_idx?, *add_idx, rec_first, other))
}
/// The combinator operator of each `X__fuel` model definition's else-branch:
/// `+` (add) or `*` (mul). The bytes cannot distinguish the bignum helpers, so
/// this is the producer's source of the operation. Lean derives and checks the
/// corresponding standard face from the emitted plan. The descent (`n - 1`)
/// uses `-`, so it never
/// confuses the scan; the recognised body shapes carry no other arithmetic.
fn model_step_ops(model_files: &[(String, String)]) -> std::collections::HashMap<String, char> {
let mut ops = std::collections::HashMap::new();
for (path, content) in model_files {
if !path.ends_with(".lean") {
continue;
}
let lines: Vec<&str> = content.lines().collect();
for i in 0..lines.len() {
let Some(rest) = lines[i].trim().strip_prefix("def ") else {
continue;
};
let Some(fuel_pos) = rest.find("__fuel ") else {
continue;
};
let name = rest[..fuel_pos].to_string();
for l in lines.iter().skip(i).take(8) {
if let Some(p) = l.find("else ") {
let els = &l[p + 5..];
let op = if els.contains('*') {
Some('*')
} else if els.contains('+') {
Some('+')
} else {
None
};
if let Some(op) = op {
ops.insert(name.clone(), op);
}
break;
}
}
}
}
ops
}