Skip to content

Commit 892b4e6

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
chore: fix, Rust, lint/fmt, issues
Batch Justfile audit: standardised naming (lowercase→Justfile), fixed parse errors, removed useless build-riscv from non-Rust repos, added missing assail recipe, and fixed code quality issues. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 8126546 commit 892b4e6

File tree

8 files changed

+249
-149
lines changed

8 files changed

+249
-149
lines changed

‎src/codegen/idris2.rs‎

Lines changed: 93 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -67,18 +67,31 @@ fn write_module_header(
6767
_manifest: &Manifest,
6868
) -> Result<()> {
6969
writeln!(src, "-- SPDX-License-Identifier: PMPL-1.0-or-later")?;
70-
writeln!(src, "-- Auto-generated by idrisiser — do not edit manually.")?;
70+
writeln!(
71+
src,
72+
"-- Auto-generated by idrisiser — do not edit manually."
73+
)?;
7174
writeln!(src, "-- Interface: {} ({})", iface.name, iface.format)?;
7275
writeln!(src, "-- Source: {}", iface.source)?;
7376
writeln!(src, "-- Regenerate with: idrisiser generate")?;
7477
writeln!(src)?;
75-
writeln!(src, "||| Formally verified wrapper for interface: {}", iface.name)?;
78+
writeln!(
79+
src,
80+
"||| Formally verified wrapper for interface: {}",
81+
iface.name
82+
)?;
7683
writeln!(src, "|||")?;
7784
writeln!(src, "||| This module provides dependent-type proofs that:")?;
78-
writeln!(src, "||| - All functions are total (cover all inputs, terminate)")?;
85+
writeln!(
86+
src,
87+
"||| - All functions are total (cover all inputs, terminate)"
88+
)?;
7989
writeln!(src, "||| - Preconditions are checked before every call")?;
8090
writeln!(src, "||| - Postconditions hold after every call")?;
81-
writeln!(src, "||| - Invariants are preserved across all operations")?;
91+
writeln!(
92+
src,
93+
"||| - Invariants are preserved across all operations"
94+
)?;
8295
writeln!(src)?;
8396
writeln!(src, "module {module_name}")?;
8497
writeln!(src)?;
@@ -106,9 +119,15 @@ fn write_imports(src: &mut String, manifest: &Manifest) -> Result<()> {
106119
/// Generate types for each function contract.
107120
/// Each function gets a record for its pre/postconditions.
108121
fn write_contract_types(src: &mut String, contracts: &[FunctionContract]) -> Result<()> {
109-
writeln!(src, "-- ================================================================")?;
122+
writeln!(
123+
src,
124+
"-- ================================================================"
125+
)?;
110126
writeln!(src, "-- Contract Types")?;
111-
writeln!(src, "-- ================================================================")?;
127+
writeln!(
128+
src,
129+
"-- ================================================================"
130+
)?;
112131
writeln!(src)?;
113132

114133
for contract in contracts {
@@ -117,19 +136,13 @@ fn write_contract_types(src: &mut String, contracts: &[FunctionContract]) -> Res
117136
// Result type for this function
118137
writeln!(src, "||| Result of calling `{fname}`")?;
119138
writeln!(src, "public export")?;
120-
writeln!(
121-
src,
122-
"data {fname}Result : Type where"
123-
)?;
139+
writeln!(src, "data {fname}Result : Type where")?;
124140
writeln!(
125141
src,
126142
" {fname}Ok : {ret} -> {fname}Result",
127143
ret = idris_type(&contract.return_type)
128144
)?;
129-
writeln!(
130-
src,
131-
" {fname}Err : String -> {fname}Result"
132-
)?;
145+
writeln!(src, " {fname}Err : String -> {fname}Result")?;
133146
writeln!(src)?;
134147

135148
// Parameter record (if there are parameters)
@@ -139,12 +152,7 @@ fn write_contract_types(src: &mut String, contracts: &[FunctionContract]) -> Res
139152
writeln!(src, "record {fname}Params where")?;
140153
writeln!(src, " constructor Mk{fname}Params")?;
141154
for param in &contract.params {
142-
writeln!(
143-
src,
144-
" {} : {}",
145-
param.name,
146-
idris_type(&param.type_name)
147-
)?;
155+
writeln!(src, " {} : {}", param.name, idris_type(&param.type_name))?;
148156
}
149157
writeln!(src)?;
150158
}
@@ -199,9 +207,15 @@ fn write_proof_obligations(
199207
contracts: &[FunctionContract],
200208
manifest: &Manifest,
201209
) -> Result<()> {
202-
writeln!(src, "-- ================================================================")?;
210+
writeln!(
211+
src,
212+
"-- ================================================================"
213+
)?;
203214
writeln!(src, "-- Proof Obligations")?;
204-
writeln!(src, "-- ================================================================")?;
215+
writeln!(
216+
src,
217+
"-- ================================================================"
218+
)?;
205219
writeln!(src)?;
206220

207221
for contract in contracts {
@@ -212,10 +226,7 @@ fn write_proof_obligations(
212226
writeln!(src, "||| Proof that `{fname}` is total (covers all inputs)")?;
213227
writeln!(src, "public export")?;
214228
writeln!(src, "data {fname}Total : Type where")?;
215-
writeln!(
216-
src,
217-
" Is{fname}Total : {fname}Total"
218-
)?;
229+
writeln!(src, " Is{fname}Total : {fname}Total")?;
219230
writeln!(src)?;
220231
}
221232

@@ -239,10 +250,7 @@ fn write_proof_obligations(
239250

240251
// Postcondition proof
241252
if !contract.postconditions.is_empty() {
242-
writeln!(
243-
src,
244-
"||| Proof that postconditions hold for a given result"
245-
)?;
253+
writeln!(src, "||| Proof that postconditions hold for a given result")?;
246254
writeln!(src, "public export")?;
247255
writeln!(
248256
src,
@@ -263,14 +271,8 @@ fn write_proof_obligations(
263271
"||| Proof that serialise/deserialise round-trips for `{fname}` results"
264272
)?;
265273
writeln!(src, "public export")?;
266-
writeln!(
267-
src,
268-
"data {fname}RoundTrip : Type where"
269-
)?;
270-
writeln!(
271-
src,
272-
" {fname}RoundTripOk : {fname}RoundTrip"
273-
)?;
274+
writeln!(src, "data {fname}RoundTrip : Type where")?;
275+
writeln!(src, " {fname}RoundTripOk : {fname}RoundTrip")?;
274276
writeln!(src)?;
275277
}
276278
}
@@ -284,9 +286,15 @@ fn write_ffi_declarations(
284286
contracts: &[FunctionContract],
285287
safe_name: &str,
286288
) -> Result<()> {
287-
writeln!(src, "-- ================================================================")?;
289+
writeln!(
290+
src,
291+
"-- ================================================================"
292+
)?;
288293
writeln!(src, "-- FFI Declarations (implemented in Zig bridge)")?;
289-
writeln!(src, "-- ================================================================")?;
294+
writeln!(
295+
src,
296+
"-- ================================================================"
297+
)?;
290298
writeln!(src)?;
291299

292300
for contract in contracts {
@@ -299,7 +307,7 @@ fn write_ffi_declarations(
299307
.map(|p| idris_prim_type(&p.type_name))
300308
.collect();
301309
let prim_sig = if prim_params.is_empty() {
302-
format!("PrimIO Bits32")
310+
"PrimIO Bits32".to_string()
303311
} else {
304312
format!("{} -> PrimIO Bits32", prim_params.join(" -> "))
305313
};
@@ -318,16 +326,28 @@ fn write_ffi_declarations(
318326

319327
/// Generate safe wrappers that enforce pre/postconditions.
320328
fn write_safe_wrappers(src: &mut String, contracts: &[FunctionContract]) -> Result<()> {
321-
writeln!(src, "-- ================================================================")?;
322-
writeln!(src, "-- Safe Wrappers (enforce contracts at the type level)")?;
323-
writeln!(src, "-- ================================================================")?;
329+
writeln!(
330+
src,
331+
"-- ================================================================"
332+
)?;
333+
writeln!(
334+
src,
335+
"-- Safe Wrappers (enforce contracts at the type level)"
336+
)?;
337+
writeln!(
338+
src,
339+
"-- ================================================================"
340+
)?;
324341
writeln!(src)?;
325342

326343
for contract in contracts {
327344
let fname = &contract.name;
328345
let ret_type = idris_type(&contract.return_type);
329346

330-
writeln!(src, "||| Safe wrapper for `{fname}` with contract enforcement.")?;
347+
writeln!(
348+
src,
349+
"||| Safe wrapper for `{fname}` with contract enforcement."
350+
)?;
331351

332352
if contract.params.is_empty() {
333353
// No-parameter function
@@ -374,13 +394,18 @@ fn write_safe_wrappers(src: &mut String, contracts: &[FunctionContract]) -> Resu
374394
"{fname} : ({}) -> IO (Either String {ret_type})",
375395
param_types.join(", ")
376396
)?;
377-
writeln!(src, "{fname} ({}) = do", contract.params.iter().map(|p| p.name.as_str()).collect::<Vec<_>>().join(", "))?;
397+
writeln!(
398+
src,
399+
"{fname} ({}) = do",
400+
contract
401+
.params
402+
.iter()
403+
.map(|p| p.name.as_str())
404+
.collect::<Vec<_>>()
405+
.join(", ")
406+
)?;
378407

379-
let prim_args: Vec<String> = contract
380-
.params
381-
.iter()
382-
.map(|p| p.name.clone())
383-
.collect();
408+
let prim_args: Vec<String> = contract.params.iter().map(|p| p.name.clone()).collect();
384409
writeln!(
385410
src,
386411
" rc <- primIO (prim__{fname} {})",
@@ -399,20 +424,33 @@ fn write_safe_wrappers(src: &mut String, contracts: &[FunctionContract]) -> Resu
399424

400425
/// Generate verification functions that compose all proofs.
401426
fn write_verification(src: &mut String, contracts: &[FunctionContract]) -> Result<()> {
402-
writeln!(src, "-- ================================================================")?;
427+
writeln!(
428+
src,
429+
"-- ================================================================"
430+
)?;
403431
writeln!(src, "-- Verification")?;
404-
writeln!(src, "-- ================================================================")?;
432+
writeln!(
433+
src,
434+
"-- ================================================================"
435+
)?;
405436
writeln!(src)?;
406437

407438
// All-proofs-discharged witness
408-
writeln!(src, "||| Witness that all proof obligations for this interface are met.")?;
439+
writeln!(
440+
src,
441+
"||| Witness that all proof obligations for this interface are met."
442+
)?;
409443
writeln!(src, "public export")?;
410444
writeln!(src, "data AllProofsComplete : Type where")?;
411445
writeln!(src, " MkAllProofsComplete :")?;
412446

413447
for (i, contract) in contracts.iter().enumerate() {
414448
let fname = &contract.name;
415-
let sep = if i < contracts.len() - 1 { " ->" } else { " ->" };
449+
let sep = if i < contracts.len() - 1 {
450+
" ->"
451+
} else {
452+
" ->"
453+
};
416454
writeln!(src, " {fname}Total{sep}")?;
417455
}
418456

‎src/codegen/mod.rs‎

Lines changed: 15 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -26,10 +26,8 @@ use crate::manifest::Manifest;
2626
/// Creates: idris2/<Module>.idr, zig/<name>_ffi.zig, <name>.ipkg, build.sh
2727
pub fn generate_all(manifest: &Manifest, output_dir: &str) -> Result<()> {
2828
let out = Path::new(output_dir);
29-
fs::create_dir_all(out.join("idris2"))
30-
.context("Failed to create idris2 output directory")?;
31-
fs::create_dir_all(out.join("zig"))
32-
.context("Failed to create zig output directory")?;
29+
fs::create_dir_all(out.join("idris2")).context("Failed to create idris2 output directory")?;
30+
fs::create_dir_all(out.join("zig")).context("Failed to create zig output directory")?;
3331

3432
// Step 1: Parse each interface definition and extract contracts
3533
let mut all_contracts = Vec::new();
@@ -72,7 +70,9 @@ fn generate_ipkg(manifest: &Manifest, output_dir: &Path) -> Result<()> {
7270
.unwrap_or(&safe_name);
7371

7472
let mut src = String::with_capacity(512);
75-
src.push_str(&format!("-- Auto-generated by idrisiser for project: {name}\n"));
73+
src.push_str(&format!(
74+
"-- Auto-generated by idrisiser for project: {name}\n"
75+
));
7676
src.push_str(&format!("package {safe_name}_verified\n\n"));
7777
src.push_str("sourcedir = \"idris2\"\n\n");
7878

@@ -117,16 +117,14 @@ fn generate_build_script(manifest: &Manifest, output_dir: &Path) -> Result<()> {
117117
let name = &manifest.project.name;
118118
let safe_name = name.replace('-', "_");
119119

120-
let codegen = manifest
121-
.idris2
122-
.codegen
123-
.as_deref()
124-
.unwrap_or("chez");
120+
let codegen = manifest.idris2.codegen.as_deref().unwrap_or("chez");
125121

126122
let mut src = String::with_capacity(1024);
127123
src.push_str("#!/usr/bin/env bash\n");
128124
src.push_str("# SPDX-License-Identifier: PMPL-1.0-or-later\n");
129-
src.push_str(&format!("# Auto-generated by idrisiser — build script for: {name}\n\n"));
125+
src.push_str(&format!(
126+
"# Auto-generated by idrisiser — build script for: {name}\n\n"
127+
));
130128
src.push_str("set -euo pipefail\n\n");
131129

132130
src.push_str(&format!("echo \"=== idrisiser Build: {name} ===\"\n\n"));
@@ -145,14 +143,12 @@ fn generate_build_script(manifest: &Manifest, output_dir: &Path) -> Result<()> {
145143

146144
// Step 3: Link
147145
src.push_str("echo \"[3/3] Linking...\"\n");
148-
src.push_str(&format!(
149-
"# Link the Idris2 runtime + Zig FFI into a shared library\n"
150-
));
146+
src.push_str("# Link the Idris2 runtime + Zig FFI into a shared library\n");
151147
src.push_str(&format!(
152148
"# zig build-lib -O ReleaseFast {safe_name}_ffi.o -o lib{safe_name}_verified\n\n"
153149
));
154150

155-
src.push_str(&format!("echo \"=== Build complete ===\"\n"));
151+
src.push_str("echo \"=== Build complete ===\"\n");
156152
src.push_str("echo \"Idris2 proofs compiled and verified.\"\n");
157153

158154
let out_path = output_dir.join("build.sh");
@@ -175,7 +171,9 @@ fn generate_build_script(manifest: &Manifest, output_dir: &Path) -> Result<()> {
175171
pub fn build(manifest: &Manifest, release: bool) -> Result<()> {
176172
println!("Building idrisiser project: {}", manifest.project.name);
177173

178-
let idris2_check = std::process::Command::new("idris2").arg("--version").output();
174+
let idris2_check = std::process::Command::new("idris2")
175+
.arg("--version")
176+
.output();
179177
if idris2_check.is_err() {
180178
anyhow::bail!(
181179
"Idris2 compiler not found on PATH.\n\
@@ -208,10 +206,7 @@ pub fn run(manifest: &Manifest, args: &[String]) -> Result<()> {
208206
let binary = format!("generated/idrisiser/build/{safe_name}_verified");
209207

210208
if !Path::new(&binary).exists() {
211-
anyhow::bail!(
212-
"Binary not found: {}. Run 'idrisiser build' first.",
213-
binary
214-
);
209+
anyhow::bail!("Binary not found: {}. Run 'idrisiser build' first.", binary);
215210
}
216211

217212
println!("Running verified wrapper: {}", manifest.project.name);

0 commit comments

Comments
 (0)