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
/// One recognised leaf of a `VariantDispatch` hit arm: what the arm computes
/// from the variant's Int payload.
#[derive(Clone, PartialEq)]
enum ArmLeaf {
/// Return the projected payload unchanged.
Proj,
/// Combine the payload with a boxed constant through a contracted host:
/// `k op x` when `const_first`, else `x op k`.
HostOp {
role: HostRole,
k: i64,
const_first: bool,
},
}
/// The straight-line integer shape of one function inside a composition's call
/// closure. Every shape is unary (`Int -> Int`), non-recursive, branch-free, and
/// its simulation lemma is provable over the caller's composed code table by the
/// probe's straight-line skeleton (rcases the host/callee `Option`, cite, close).
#[derive(Clone)]
enum LeafShape {
/// `[localGet 0, localGet 0, call add]` — model `x + x`.
SelfSum { add_idx: u32 },
/// `[localGet 0, call c1, ..., call cm]` (m >= 1), each `ci` a user function
/// in the closure — model `cm (... (c1 x))`. The composition point.
Chain { calls: Vec<u32> },
}
/// One function in a composition caller's transitive call closure: its verbatim
/// body (for the shared `CodeTbl`), its self index, and its recognised shape.
#[derive(Clone)]
struct ClosureEntry {
name: String,
self_idx: u32,
type_idx: u32,
nlocals: usize,
code_entry_bytes: Vec<u8>,
ops: Vec<Op>,
shape: LeafShape,
}
#[derive(Clone, PartialEq)]
enum VerbatimDefault {
Null,
F64Bits(u64),
Array {
type_idx: u32,
data_idx: u32,
bytes: Vec<u8>,
},
}
#[derive(Clone, PartialEq)]
enum StringEqDefault {
Input,
Verbatim(VerbatimDefault),
}
type StringEqVerbatimChain = (
Vec<(VerbatimDefault, VerbatimDefault)>,
StringEqDefault,
u32,
);
#[derive(Clone, PartialEq)]
enum ConstructorField {
Local(u32),
Null,
}