test/f2a-import-closure.py

1#!/usr/bin/env python3

2"""F2a witness channel 4 -- the TRANSITIVE import closure of the passive core.

4WHY TRANSITIVE, AND WHY THIS EXISTS AT ALL.

6F1a's gate arm 6 and SD-P4's gate arm 3 both check DIRECT imports: they read one

7file's `(import ...)` form and refuse a forbidden library there. That is a real

8check and it stays. It is also blind to the case that matters most at a trust

9boundary -- a module that reaches the author runtime through an innocent-looking

10intermediary. F1a's blocking review closed the umbrella-import hole for

11`(sigil doc)` specifically and left the general transitive question open as

12informational "for F2/P0". F2a is that phase, so this walks the whole graph.

14WHAT IT REFUSES TO DO: guess. A library that resolves to no file and is not in

15`NATIVE_LEAVES` below stops the walk with a failure. A closure that silently

16skips what it cannot find reports "clean" for the wrong reason, and "clean"

17because we could not look is indistinguishable from "clean" -- which is the

18single most repeated instrument failure in this estate.

20WHAT IT DOES NOT CLAIM, stated plainly because a broad claim that is almost true

21invites nobody to look for the gap:

23 * It is a claim about MODULES, not about primitives. Nothing here prevents a

24 primitive from existing, and reading a manuscript does use a reader. The

25 RUNTIME witness is what establishes that reading is not evaluating; this arm

26 cannot.

27 * It does not follow `include`, `cond-expand`, or re-exports. A library that

28 reaches a forbidden module only through one of those is invisible to this

29 walk. Stated because an unstated gap in a passivity claim is worse than a

30 narrower claim honestly drawn.

31 * `NATIVE_LEAVES` is a hole BY DESIGN: anything reachable only through a

32 declared leaf is unwalked. The result line reports how many leaves were

33 actually HIT, so a transcript shows whether the hole was entered at all

34 rather than how many entries the dict happens to contain.

35 * It is a claim about REACHABILITY OF MODULES in the source graph, not about

36 what the VM can do. Nothing here prevents a primitive from existing.

38NO I/O MODULE IS IN THE CLOSURE, AND THAT IS AN OUTCOME OF THIS TOOL RATHER THAN

39AN ASSUMPTION BEHIND IT. The first version of the passive core imported

40`(sigil language)` (for the `#lang` header scan) and `(sigil error)` (for

41`exception-message`). Both look inert in an import list. This walk reported 17

42modules including `(sigil fs)`, `(sigil io)`, `(sigil socket)` and the async

43scheduler. The header offset became a caller-supplied parameter and

44`exception-message` came from `(sigil core)` instead, and the closure is now the

45list this tool prints -- which the gate reads, so no number is written down here

46to go stale.

48So the forbidden set below is the EVALUATION SIDE specifically: the author

49runtime, the semantic models, the verifier and its subprocess reach, and the

50renderers that pull the verifier in.

51"""

53import os

54import re

55import sys

57# Library name -> reason it legitimately has no source file in these roots.

58# Every entry is a decision someone made; an unlisted unresolvable library is an

59# error, not a leaf.

60NATIVE_LEAVES = {

61 "(sigil compiler)": "VM-provided; the reader and the language-header scanner live here",

62}

64# The I/O modules are HERE, in the walker, rather than only in a `grep` over its

65# output. They were previously refused by a single grep in gate-f2a.sh keyed on

66# the walker printing exactly two leading spaces -- an absence assertion with no

67# positive control, that a change to this file's output format would have

68# silenced permanently and silently. In the dict they get the walker's own

69# reached-via trail, and the gate's grep becomes a second opinion rather than the

70# only one.

71FORBIDDEN = {

72 "(sigil fs)": "filesystem access; the caller reads the file, not this module",

73 "(sigil io)": "port I/O; reaches the socket and scheduler layers",

74 "(sigil socket)": "network access",

75 "(sigil process)": "subprocess execution",

76 "(sigil shell)": "shell execution",

77 "(sigil doc author)": "the author-facing command vocabulary",

78 "(sigil doc private author-runtime)": "the author runtime itself",

79 "(sigil doc model)": "constructing semantic records is the lowering side",

80 "(sigil doc verify)": "runs example code in subprocesses",

81 "(sigil doc presentation)": "reaches (sigil doc verify)",

82 "(sigil doc render html)": "reaches (sigil doc presentation)",

83 "(sigil doc render typst)": "reaches (sigil doc presentation)",

84 "(sigil doc print)": "reaches the print toolchain",

85 "(folio doc model)": "the frozen semantic model; would drag (sigil doc model) in",

86 "(folio doc publication)": "lowers to semantic records",

87}

89LIB_RE = re.compile(r"\(([a-z][a-z0-9-]*(?:\s+[a-z0-9-]+)+)\)")

92def strip_comments(text):

93 """Drop whole-line comments only.

95 NOT everything after the first `;`: a semicolon inside a string literal

96 would truncate real code, and a truncated import form is an import this walk

97 never sees. Same reasoning as gate-f1a.sh arm 7, which learned it the hard

98 way by matching its own explanatory prose.

99 """

100 return "\n".join(l for l in text.split("\n") if not l.lstrip().startswith(";"))

101

102

103def imports_of(path):

104 text = strip_comments(open(path, "r", encoding="utf-8").read())

105 out = []

106 i = 0

107 while True:

108 i = text.find("(import", i)

109 if i < 0:

110 break

111 depth = 0

112 j = i

113 while j < len(text):

114 if text[j] == "(":

115 depth += 1

116 elif text[j] == ")":

117 depth -= 1

118 if depth == 0:

119 break

120 j += 1

121 form = text[i:j + 1]

122 for m in LIB_RE.finditer(form):

123 name = "(" + " ".join(m.group(1).split()) + ")"

124 if name != "(import)":

125 out.append(name)

126 i = j + 1

127 return out

128

129

130def resolve(name, roots):

131 parts = name[1:-1].split()

132 rel = os.path.join(*parts) + ".sgl"

133 for root in roots:

134 candidate = os.path.join(root, rel)

135 if os.path.isfile(candidate):

136 return candidate

137 return None

138

139

140def main():

141 if len(sys.argv) < 3:

142 print("usage: f2a-import-closure.py <root-library> <source-root>...", file=sys.stderr)

143 sys.exit(1)

144 root_lib = sys.argv[1]

145 roots = sys.argv[2:]

146 for r in roots:

147 if not os.path.isdir(r):

148 print("F2A_IMPORT_CLOSURE RED: source root %r does not exist; the walk "

149 "would report every library in it as unresolvable" % r, file=sys.stderr)

150 sys.exit(1)

151

152 start = resolve(root_lib, roots)

153 if start is None:

154 print("F2A_IMPORT_CLOSURE RED: cannot resolve the ROOT library %s in %r"

155 % (root_lib, roots), file=sys.stderr)

156 sys.exit(1)

157

158 seen = {}

159 unresolved = []

160 leaves_hit = set()

161 order = []

162 pending = [(root_lib, start, ["<root>"])]

163 while pending:

164 name, path, trail = pending.pop()

165 if name in seen:

166 continue

167 seen[name] = trail

168 order.append(name)

169 if path is None:

170 continue

171 for dep in imports_of(path):

172 if dep in seen:

173 continue

174 dpath = resolve(dep, roots)

175 if dpath is None:

176 if dep not in NATIVE_LEAVES:

177 unresolved.append((dep, name))

178 continue

179 leaves_hit.add(dep)

180 pending.append((dep, dpath, trail + [name]))

181

182 # BOTH FAILURE CLASSES ARE REPORTED, THEN THE WALK FAILS ONCE.

183 #

184 # An earlier version returned on `unresolved` before ever looking for

185 # forbidden modules, which made the gate's own positive control unfalsifiable

186 # in the direction that mattered: planting `(sigil process)` one level down

187 # produced an UNRESOLVED failure (the plant drags `(sigil io)` in, which

188 # reaches `(sigil socket)`) and never printed FORBIDDEN at all. The walk

189 # failed for a true reason and reported the wrong one -- which is the same

190 # defect as a check that passes for the wrong reason, wearing a red coat.

191 violations = [n for n in order if n in FORBIDDEN]

192 for v in violations:

193 print(" FORBIDDEN: %s (%s)\n reached via: %s"

194 % (v, FORBIDDEN[v], " -> ".join(seen[v] + [v])), file=sys.stderr)

195 for dep, via in unresolved:

196 print(" UNRESOLVED: %s (imported by %s)" % (dep, via), file=sys.stderr)

197 if violations or unresolved:

198 print("F2A_IMPORT_CLOSURE RED: %d forbidden module(s) reachable, %d "

199 "librar(ies) unresolvable. A forbidden module is a passivity "

200 "breach; an unresolvable one means the walk could not look, and "

201 "\"clean because I could not look\" is indistinguishable from "

202 "clean." % (len(violations), len(unresolved)), file=sys.stderr)

203 sys.exit(1)

204

205 # NON-VACUITY. A walk that visited one module would report a clean closure

206 # for free. The floor is not a magic number: it is "more than the root plus

207 # its direct imports", i.e. the walk demonstrably recursed.

208 direct = len(set(imports_of(start)))

209 if len(order) <= direct + 1:

210 print("F2A_IMPORT_CLOSURE RED: closure is %d modules and the root has %d "

211 "direct imports -- the walk did not recurse, so a violation one "

212 "level down would be invisible" % (len(order), direct), file=sys.stderr)

213 sys.exit(1)

214

215 # `leaves` is the count actually HIT during this walk, not the size of the

216 # dict. It printed `len(NATIVE_LEAVES)` -- a constant 1 -- so the gate

217 # transcript read "leaves=1" while the walk had entered no leaf at all, and a

218 # reader would reasonably conclude one library was legitimately unresolvable.

219 print("F2A_IMPORT_CLOSURE modules=%d direct=%d forbidden=0 leaves=%d"

220 % (len(order), direct, len(leaves_hit)))

221 for n in sorted(order):

222 print(" " + n)

223

224

225if __name__ == "__main__":

226 main()