Skip to content

Commit 356017a

Browse files
ci: fmt + clippy under stable 1.96 to make rust-ci green (follow-up) (#78)
* feat(abi): prove Conformant scaffold property (Layer 2 Semantics) Add Iseriser.ABI.Semantics proving the headline domain property: a generated -iser scaffold is Conformant exactly when all five required components (Manifest, Idris2 ABI, Zig FFI, Codegen, Rust CLI) are present. Conformant is built from genuine Data.List.Elem membership obligations with no catch-all constructor, so a scaffold missing any component has no witness. Includes a sound+complete decConformant : (s) -> Dec (Conformant s), a soundness fact certifyConformantSound, a positive control (completeIsConformant via explicit Elem positions), and a negative control (ffiMissingNotConformant : Not (Conformant ffiMissing)). Non-vacuity confirmed: a deliberately-false Has Ffi witness for the FFI-missing scaffold is rejected by idris2. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: add Layer-3 Invariants (generation soundness + conformance closure) Add Iseriser.ABI.Invariants over the existing Layer-2 Semantics model (Component/Scaffold/Has/Conformant). Two new, deeper, distinct theorems: 1. Generation soundness (correct-by-construction): genScaffold provably emits (s ** Conformant s) for any LanguageModel, with a corollary tying it back to the Layer-2 certifier (conformantCertifies). 2. Upward-closure / monotonicity: conformantStable proves Conformance is preserved under extension, via a genuine Elem-weakening lemma (elemAppendRight) — an algebraic closure law, not the Layer-2 decision. Includes a sound+complete Dec (decExtendConformant), a positive control (extendedGeneratedConformant) and a non-vacuity negative control (extendedBrokenNotConformant : Not ...). Builds clean with zero warnings; adversarial false proof rejected. No believe_me/postulate/assert_total. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: seal ABI<->FFI seam with Layer-4 soundness proof (FfiSeam) Add Iseriser.ABI.FfiSeam proving the resultToInt encoding is sound: - intToResult decoder + resultRoundTrip (lossless/faithful encoding) - resultToIntInjective derived from round-trip (distinct outcomes never collide on the wire) - positive controls (concrete decodes by Refl) and a machine-checked non-vacuity control (resultToInt Ok /= resultToInt Error) Genuine total proof: no believe_me/postulate/assert_total/etc. Registered in iseriser-abi.ipkg; package builds clean with zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi(iseriser): add Layer-5 capstone ABI soundness certificate Assemble the existing Layer-2/3/4 ABI proofs into one inhabited value, Iseriser.ABI.Capstone.abiContractDischarged : ABISound, with fields: - flagship : Conformant Semantics.completeScaffold (reuses Semantics.completeIsConformant) - invariant : Conformant (extend [Manifest] generatedScaffold) (reuses Invariants.extendedGeneratedConformant) - ffiInjective : resultToInt injectivity (reuses FfiSeam.resultToIntInjective) Pure composition of already-exported witnesses: if any prior layer were unsound the capstone would not typecheck. Adversarial check confirms a wrong-type witness in the flagship slot is rejected. %default total, SPDX, zero warnings. ipkg updated (Capstone listed last). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * ci: make CI green — bump rust-ci to standards@8dc2bf0 (toolchain: stable fix); port ABI-FFI gate Python->Bash (Python is estate-banned) Resolves the standing baseline CI reds (rust-ci toolchain error, governance Language/anti-pattern, governance workflow-lint) without altering the proven ABI. The Bash gate reproduces the former Python gate's verdict verbatim (validated across all -iser repos) and catches the same drift classes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * ci: adopt canonical Julia ABI-FFI gate (estate standard, matches verisimiser) in place of the interim Bash port * style: cargo fmt + clippy fixes (black_box -> std::hint::black_box; cmp_owned) — make rust-ci green * style: cargo fmt + clippy under stable 1.96 (CI toolchain) — black_box->std::hint, cmp_owned, empty-format; make rust-ci green on main --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 2ae2976 commit 356017a

10 files changed

Lines changed: 223 additions & 103 deletions

File tree

benches/iseriser_bench.rs

Lines changed: 12 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,9 @@
2121
// Run with:
2222
// cargo bench --bench iseriser_bench
2323

24-
use criterion::{black_box, criterion_group, criterion_main, Criterion};
24+
use criterion::{Criterion, criterion_group, criterion_main};
2525
use iseriser::manifest::{parse_manifest, validate};
26+
use std::hint::black_box;
2627

2728
// ---------------------------------------------------------------------------
2829
// Manifest TOML fixtures
@@ -100,8 +101,8 @@ description = "Gleam interop -iser targeting the BEAM runtime"
100101
fn bench_parse_minimal(c: &mut Criterion) {
101102
c.bench_function("parse_manifest/minimal", |b| {
102103
b.iter(|| {
103-
let m = parse_manifest(black_box(MINIMAL_MANIFEST))
104-
.expect("minimal manifest must parse");
104+
let m =
105+
parse_manifest(black_box(MINIMAL_MANIFEST)).expect("minimal manifest must parse");
105106
black_box(m);
106107
});
107108
});
@@ -111,8 +112,7 @@ fn bench_parse_minimal(c: &mut Criterion) {
111112
fn bench_parse_rich(c: &mut Criterion) {
112113
c.bench_function("parse_manifest/rich_20_primitives", |b| {
113114
b.iter(|| {
114-
let m = parse_manifest(black_box(RICH_MANIFEST))
115-
.expect("rich manifest must parse");
115+
let m = parse_manifest(black_box(RICH_MANIFEST)).expect("rich manifest must parse");
116116
black_box(m);
117117
});
118118
});
@@ -122,8 +122,7 @@ fn bench_parse_rich(c: &mut Criterion) {
122122
fn bench_parse_gleam(c: &mut Criterion) {
123123
c.bench_function("parse_manifest/gleam_beam_target", |b| {
124124
b.iter(|| {
125-
let m = parse_manifest(black_box(GLEAM_MANIFEST))
126-
.expect("gleam manifest must parse");
125+
let m = parse_manifest(black_box(GLEAM_MANIFEST)).expect("gleam manifest must parse");
127126
black_box(m);
128127
});
129128
});
@@ -139,7 +138,8 @@ fn bench_validate_valid(c: &mut Criterion) {
139138
c.bench_function("validate/valid_manifest", |b| {
140139
b.iter(|| {
141140
let result = validate(black_box(&manifest));
142-
black_box(result.expect("valid manifest must pass validation"));
141+
result.expect("valid manifest must pass validation");
142+
black_box(());
143143
});
144144
});
145145
}
@@ -150,7 +150,8 @@ fn bench_validate_rich(c: &mut Criterion) {
150150
c.bench_function("validate/rich_20_primitives", |b| {
151151
b.iter(|| {
152152
let result = validate(black_box(&manifest));
153-
black_box(result.expect("rich manifest must pass validation"));
153+
result.expect("rich manifest must pass validation");
154+
black_box(());
154155
});
155156
});
156157
}
@@ -200,8 +201,7 @@ fn bench_scan_repo(c: &mut Criterion) {
200201

201202
c.bench_function("scan_repo/iseriser_root", |b| {
202203
b.iter(|| {
203-
let recs = iseriser::scan::scan_repo(black_box(&repo_root))
204-
.expect("scan must succeed");
204+
let recs = iseriser::scan::scan_repo(black_box(&repo_root)).expect("scan must succeed");
205205
black_box(recs);
206206
});
207207
});
@@ -218,11 +218,7 @@ criterion_group!(
218218
bench_parse_gleam,
219219
);
220220

221-
criterion_group!(
222-
validate_benches,
223-
bench_validate_valid,
224-
bench_validate_rich,
225-
);
221+
criterion_group!(validate_benches, bench_validate_valid, bench_validate_rich,);
226222

227223
criterion_group!(
228224
abi_benches,

src/abi/idris_emitter.rs

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -198,11 +198,9 @@ fn find_data_keyword(src: &str) -> Option<usize> {
198198
let mut search_from = 0;
199199
while let Some(pos) = src[search_from..].find("data") {
200200
let abs = search_from + pos;
201-
let before_ok = abs == 0
202-
|| matches!(bytes[abs - 1], b'\n' | b' ' | b'\t');
201+
let before_ok = abs == 0 || matches!(bytes[abs - 1], b'\n' | b' ' | b'\t');
203202
let after = abs + 4;
204-
let after_ok = after < bytes.len()
205-
&& matches!(bytes[after], b' ' | b'\t' | b'\n');
203+
let after_ok = after < bytes.len() && matches!(bytes[after], b' ' | b'\t' | b'\n');
206204
if before_ok && after_ok {
207205
return Some(abs);
208206
}
@@ -292,10 +290,7 @@ fn skip_gadt_block(src: &str) -> usize {
292290
let header_end = match where_pos {
293291
Some(w) => {
294292
// Consume through the rest of that line.
295-
src[w..]
296-
.find('\n')
297-
.map(|i| w + i + 1)
298-
.unwrap_or(src.len())
293+
src[w..].find('\n').map(|i| w + i + 1).unwrap_or(src.len())
299294
}
300295
None => {
301296
// No `where` — single-line `data Foo : ...`. Consume through eol.
@@ -372,10 +367,7 @@ fn parse_to_int_equations(src: &str) -> Result<BTreeMap<String, BTreeMap<String,
372367
/// Extract the head variant name from a pattern like `Empty`, `(Custom _)`,
373368
/// `Custom`. Returns `None` for `_` or empty / non-identifier patterns.
374369
fn extract_variant_from_pattern(pattern: &str) -> Option<String> {
375-
let p = pattern
376-
.trim_start_matches('(')
377-
.trim_end_matches(')')
378-
.trim();
370+
let p = pattern.trim_start_matches('(').trim_end_matches(')').trim();
379371
let head_end = p.find(|c: char| !is_ident_char(c)).unwrap_or(p.len());
380372
if head_end == 0 {
381373
return None;

src/abi/manifest_schema.rs

Lines changed: 50 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -73,14 +73,56 @@ pub fn to_snake_case(s: &str) -> String {
7373
/// the cartridge convention is to rename the variant in Zig — the
7474
/// verifier accepts the cartridge convention as a valid alternative.
7575
const ZIG_RESERVED: &[&str] = &[
76-
"addrspace", "align", "allowzero", "and", "anyframe", "anytype", "asm",
77-
"async", "await", "break", "callconv", "catch", "comptime", "const",
78-
"continue", "defer", "else", "enum", "errdefer", "error", "export",
79-
"extern", "fn", "for", "if", "inline", "linksection", "noalias",
80-
"noinline", "nosuspend", "null", "opaque", "or", "orelse", "packed",
81-
"pub", "resume", "return", "struct", "suspend", "switch", "test",
82-
"threadlocal", "try", "union", "unreachable", "usingnamespace", "var",
83-
"volatile", "while",
76+
"addrspace",
77+
"align",
78+
"allowzero",
79+
"and",
80+
"anyframe",
81+
"anytype",
82+
"asm",
83+
"async",
84+
"await",
85+
"break",
86+
"callconv",
87+
"catch",
88+
"comptime",
89+
"const",
90+
"continue",
91+
"defer",
92+
"else",
93+
"enum",
94+
"errdefer",
95+
"error",
96+
"export",
97+
"extern",
98+
"fn",
99+
"for",
100+
"if",
101+
"inline",
102+
"linksection",
103+
"noalias",
104+
"noinline",
105+
"nosuspend",
106+
"null",
107+
"opaque",
108+
"or",
109+
"orelse",
110+
"packed",
111+
"pub",
112+
"resume",
113+
"return",
114+
"struct",
115+
"suspend",
116+
"switch",
117+
"test",
118+
"threadlocal",
119+
"try",
120+
"union",
121+
"unreachable",
122+
"usingnamespace",
123+
"var",
124+
"volatile",
125+
"while",
84126
];
85127

86128
pub fn is_zig_reserved(word: &str) -> bool {

src/abi/verify.rs

Lines changed: 64 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -279,18 +279,43 @@ mod tests {
279279
enums: vec![EnumDecl {
280280
name: "S".into(),
281281
variants: vec![
282-
EnumVariant { name: "Empty".into(), value: 0 },
283-
EnumVariant { name: "Ready".into(), value: 1 },
284-
EnumVariant { name: "Done".into(), value: 2 },
282+
EnumVariant {
283+
name: "Empty".into(),
284+
value: 0,
285+
},
286+
EnumVariant {
287+
name: "Ready".into(),
288+
value: 1,
289+
},
290+
EnumVariant {
291+
name: "Done".into(),
292+
value: 2,
293+
},
285294
],
286295
}],
287296
transition_table: Some(TransitionTable {
288297
state_enum: "S".into(),
289298
rows: vec![
290-
TransitionRow { from: "Empty".into(), to: "Ready".into(), allowed: true },
291-
TransitionRow { from: "Ready".into(), to: "Done".into(), allowed: true },
292-
TransitionRow { from: "Done".into(), to: "Empty".into(), allowed: true },
293-
TransitionRow { from: "Empty".into(), to: "Done".into(), allowed: false },
299+
TransitionRow {
300+
from: "Empty".into(),
301+
to: "Ready".into(),
302+
allowed: true,
303+
},
304+
TransitionRow {
305+
from: "Ready".into(),
306+
to: "Done".into(),
307+
allowed: true,
308+
},
309+
TransitionRow {
310+
from: "Done".into(),
311+
to: "Empty".into(),
312+
allowed: true,
313+
},
314+
TransitionRow {
315+
from: "Empty".into(),
316+
to: "Done".into(),
317+
allowed: false,
318+
},
294319
],
295320
}),
296321
}
@@ -331,8 +356,18 @@ mod tests {
331356
}
332357
"#;
333358
let z = parse_zig(src).unwrap();
334-
let report = verify(&make_manifest(), &z, Path::new("m.json"), Path::new("z.zig"));
335-
assert!(report.findings.iter().any(|f| f.kind == "variant-value-mismatch"));
359+
let report = verify(
360+
&make_manifest(),
361+
&z,
362+
Path::new("m.json"),
363+
Path::new("z.zig"),
364+
);
365+
assert!(
366+
report
367+
.findings
368+
.iter()
369+
.any(|f| f.kind == "variant-value-mismatch")
370+
);
336371
}
337372

338373
#[test]
@@ -348,9 +383,17 @@ mod tests {
348383
}
349384
"#;
350385
let z = parse_zig(src).unwrap();
351-
let report = verify(&make_manifest(), &z, Path::new("m.json"), Path::new("z.zig"));
386+
let report = verify(
387+
&make_manifest(),
388+
&z,
389+
Path::new("m.json"),
390+
Path::new("z.zig"),
391+
);
352392
assert!(
353-
report.findings.iter().any(|f| f.kind == "transition-forbidden-but-accepted"),
393+
report
394+
.findings
395+
.iter()
396+
.any(|f| f.kind == "transition-forbidden-but-accepted"),
354397
"{:#?}",
355398
report.findings
356399
);
@@ -369,9 +412,17 @@ mod tests {
369412
}
370413
"#;
371414
let z = parse_zig(src).unwrap();
372-
let report = verify(&make_manifest(), &z, Path::new("m.json"), Path::new("z.zig"));
415+
let report = verify(
416+
&make_manifest(),
417+
&z,
418+
Path::new("m.json"),
419+
Path::new("z.zig"),
420+
);
373421
assert!(
374-
report.findings.iter().any(|f| f.kind == "transition-accepted-but-undeclared"),
422+
report
423+
.findings
424+
.iter()
425+
.any(|f| f.kind == "transition-accepted-but-undeclared"),
375426
"{:#?}",
376427
report.findings
377428
);

src/abi/zig_ffi_parser.rs

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -103,9 +103,9 @@ fn parse_enum_body(body: &str) -> Result<BTreeMap<String, i64>> {
103103
.next()
104104
.ok_or_else(|| anyhow!("variant `{}` missing `= <int>` value", name))?
105105
.trim();
106-
let value: i64 = value_str
107-
.parse()
108-
.with_context(|| format!("variant `{}` value `{}` is not an integer", name, value_str))?;
106+
let value: i64 = value_str.parse().with_context(|| {
107+
format!("variant `{}` value `{}` is not an integer", name, value_str)
108+
})?;
109109
if variants.insert(name.clone(), value).is_some() {
110110
return Err(anyhow!("duplicate variant `{}` in enum body", name));
111111
}
@@ -148,8 +148,7 @@ fn parse_transition_table(src: &str) -> Result<Option<ZigTransitionTable>> {
148148
_ => {}
149149
}
150150
}
151-
let end =
152-
end_idx.ok_or_else(|| anyhow!("`switch (from)` body is unterminated"))?;
151+
let end = end_idx.ok_or_else(|| anyhow!("`switch (from)` body is unterminated"))?;
153152
let body = &body_src[..end];
154153
let arms = parse_switch_arms(body)?;
155154
Ok(Some(ZigTransitionTable {
@@ -234,9 +233,8 @@ fn parse_switch_arms(body: &str) -> Result<BTreeMap<String, Vec<String>>> {
234233
.strip_prefix('.')
235234
.ok_or_else(|| anyhow!("switch arm `{}` does not start with `.`", from))?
236235
.to_string();
237-
let tos = parse_arm_targets(body_part).with_context(|| {
238-
format!("parsing targets of switch arm for `{}`", from)
239-
})?;
236+
let tos = parse_arm_targets(body_part)
237+
.with_context(|| format!("parsing targets of switch arm for `{}`", from))?;
240238
if arms.insert(from.clone(), tos).is_some() {
241239
return Err(anyhow!("duplicate switch arm for `{}`", from));
242240
}

src/codegen/cartridge.rs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -89,10 +89,7 @@ impl CartridgeRepo {
8989
/// Scaffold a boj-server cartridge skeleton for the given manifest.
9090
///
9191
/// Writes `<output_dir>/<iser_name>-mcp/` and all its contents.
92-
pub fn scaffold_cartridge(
93-
manifest: &Manifest,
94-
output_dir: &Path,
95-
) -> CartridgeScaffoldResult {
92+
pub fn scaffold_cartridge(manifest: &Manifest, output_dir: &Path) -> CartridgeScaffoldResult {
9693
let model = manifest.to_language_model();
9794
let iser_name = model.iser_name();
9895
let cartridge_name = format!("{}-mcp", iser_name);

0 commit comments

Comments
 (0)