game-server-admin/scripts/gen_abi_expected.py at 5d498cc2f78072c834dbc4fe47901adb5705ad21 · hyperpolymath/game-server-admin · GitHub

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
#!/usr/bin/env python3
# SPDX-License-Identifier: AGPL-3.0-or-later
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# gen_abi_expected.py — extract the canonical C-ABI layout numbers from the
# machine-checked Idris2 model (src/interface/abi/Layout.idr) and emit a Zig
# source file (src/interface/ffi/src/abi_layout_expected.zig) consumed by the
# Zig-side cross-check (abi_layout.zig).
#
# Layout.idr is the single source of truth: it carries the proofs (NoOverlap,
# AllFieldsAligned, SizeAligned, SizeCoversFields). This script lifts the same
# `MkFieldDesc name offset size align` / `MkStructLayout [...] total align`
# constants into Zig so the compiler can assert `@offsetOf`/`@sizeOf`/`@alignOf`
# of the canonical extern structs agree with the proven model.
#
# Run from the repository root:
#   python3 scripts/gen_abi_expected.py
# The build/CI re-runs this and `git diff --exit-code`s the result to guarantee
# the Zig expectations never drift from the Idris proofs.

import re
import sys
import pathlib

# Idris layout variable (lowerCamel, without the "Layout" suffix) -> Zig struct
# type name. Drives both extraction and the emitted const names.
STRUCTS = {
    "serverHandle": "ServerHandle",
    "probeResult": "ProbeResult",
    "configField": "ConfigField",
    "a2mlConfig": "A2MLConfig",
    "gameProfile": "GameProfile",
    "serverOctad": "ServerOctad",
    "fingerprint": "Fingerprint",
    "driftReport": "DriftReport",
}

FIELD_RE = re.compile(
    r'MkFieldDesc\s+"(?P<name>\w+)"\s+(?P<offset>\d+)\s+(?P<size>\d+)\s+(?P<align>\d+)'
)


def parse_layout(text, var):
    """Return (fields, total_size, struct_align) for `<var>Layout`."""
    # Match:  <var>Layout = MkStructLayout [ ...fields... ] <total> <align>
    block_re = re.compile(
        r'\b' + re.escape(var) + r'Layout\s*=\s*MkStructLayout\s*\[(?P<body>.*?)\]\s*'
        r'(?P<total>\d+)\s+(?P<align>\d+)',
        re.DOTALL,
    )
    m = block_re.search(text)
    if not m:
        raise SystemExit(f"error: could not find {var}Layout in Layout.idr")
    fields = []
    for fm in FIELD_RE.finditer(m.group("body")):
        name = fm.group("name")
        if name.startswith("padding"):
            continue  # implicit C padding; not a real extern-struct field
        fields.append(
            (name, int(fm.group("offset")), int(fm.group("size")), int(fm.group("align")))
        )
    return fields, int(m.group("total")), int(m.group("align"))


def main():
    root = pathlib.Path(__file__).resolve().parent.parent
    layout_idr = root / "src" / "interface" / "abi" / "Layout.idr"
    out_zig = root / "src" / "interface" / "ffi" / "src" / "abi_layout_expected.zig"

    text = layout_idr.read_text(encoding="utf-8")

    out = []
    out.append("// SPDX-License-Identifier: AGPL-3.0-or-later")
    out.append("// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>")
    out.append("//")
    out.append("// @generated by scripts/gen_abi_expected.py from src/interface/abi/Layout.idr")
    out.append("// DO NOT EDIT. Regenerate with: python3 scripts/gen_abi_expected.py")
    out.append("//")
    out.append("// Canonical C-ABI layout numbers lifted from the machine-checked Idris2 model")
    out.append("// (GSA.ABI.Layout). Consumed by abi_layout.zig to assert that the Zig extern")
    out.append("// structs agree, byte-for-byte, with the proven Idris layout.")
    out.append("")
    out.append("pub const Field = struct {")
    out.append("    name: []const u8,")
    out.append("    offset: u32,")
    out.append("    size: u32,")
    out.append("    alignment: u32,")
    out.append("};")
    out.append("")
    out.append("pub const StructExpect = struct {")
    out.append("    name: []const u8,")
    out.append("    total_size: u32,")
    out.append("    struct_align: u32,")
    out.append("    fields: []const Field,")
    out.append("};")
    out.append("")

    names = []
    for var, zig_name in STRUCTS.items():
        fields, total, align = parse_layout(text, var)
        names.append(zig_name)
        out.append(f"pub const {zig_name} = StructExpect{{")
        out.append(f'    .name = "{zig_name}",')
        out.append(f"    .total_size = {total},")
        out.append(f"    .struct_align = {align},")
        out.append("    .fields = &.{")
        for (fn, off, sz, al) in fields:
            out.append(
                f'        .{{ .name = "{fn}", .offset = {off}, .size = {sz}, .alignment = {al} }},'
            )
        out.append("    },")
        out.append("};")
        out.append("")

    out.append("pub const all = [_]StructExpect{ " + ", ".join(names) + " };")
    out.append("")

    out_zig.write_text("\n".join(out), encoding="utf-8")
    print(f"wrote {out_zig.relative_to(root)} ({len(names)} structs)")


if __name__ == "__main__":
    sys.exit(main())