@@ -198,3 +198,351 @@ fn test_c_header_parsing_extracts_functions() {
198198 "Should contain reduce from verify list"
199199 ) ;
200200}
201+
202+ // ==========================================================================
203+ // Point-to-point: each interface format generates correct Idris2
204+ // ==========================================================================
205+
206+ #[ test]
207+ fn test_all_interface_formats_generate ( ) {
208+ let formats = [ "openapi" , "c-header" , "protobuf" , "type-sig" ] ;
209+ for fmt in & formats {
210+ let toml_str = format ! ( r#"
211+ [project]
212+ name = "test-{fmt}"
213+
214+ [[interfaces]]
215+ name = "test-iface"
216+ source = "nonexistent.file"
217+ format = "{fmt}"
218+ "# ) ;
219+
220+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( & toml_str) . unwrap ( ) ;
221+ idrisiser:: manifest:: validate ( & m) . unwrap ( ) ;
222+
223+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
224+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) )
225+ . unwrap_or_else ( |e| panic ! ( "Failed for format {fmt}: {e}" ) ) ;
226+
227+ // Every format should produce an Idris2 module
228+ let idr_dir = dir. path ( ) . join ( "idris2" ) ;
229+ assert ! ( idr_dir. exists( ) , "idris2/ missing for format {fmt}" ) ;
230+
231+ // And a Zig bridge
232+ let zig_dir = dir. path ( ) . join ( "zig" ) ;
233+ assert ! ( zig_dir. exists( ) , "zig/ missing for format {fmt}" ) ;
234+ }
235+ }
236+
237+ // ==========================================================================
238+ // End-to-end: full pipeline with all artifacts
239+ // ==========================================================================
240+
241+ #[ test]
242+ fn test_end_to_end_all_artifacts ( ) {
243+ let m = idrisiser:: manifest:: load_manifest ( "examples/user-api/idrisiser.toml" ) . unwrap ( ) ;
244+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
245+ let out = dir. path ( ) . to_str ( ) . unwrap ( ) ;
246+
247+ idrisiser:: codegen:: generate_all ( & m, out) . unwrap ( ) ;
248+
249+ // All expected artifacts
250+ assert ! ( dir. path( ) . join( "idris2" ) . exists( ) , "idris2/ dir" ) ;
251+ assert ! ( dir. path( ) . join( "zig" ) . exists( ) , "zig/ dir" ) ;
252+ assert ! ( dir. path( ) . join( "example_project_verified.ipkg" ) . exists( ) , ".ipkg" ) ;
253+ assert ! ( dir. path( ) . join( "build.sh" ) . exists( ) , "build.sh" ) ;
254+
255+ // Two interfaces should produce two Idris2 modules
256+ let idr_files: Vec < _ > = walkdir:: WalkDir :: new ( dir. path ( ) . join ( "idris2" ) )
257+ . into_iter ( )
258+ . filter_map ( |e| e. ok ( ) )
259+ . filter ( |e| e. path ( ) . extension ( ) . is_some_and ( |ext| ext == "idr" ) )
260+ . collect ( ) ;
261+ assert_eq ! ( idr_files. len( ) , 2 , "Should generate 2 .idr modules" ) ;
262+ }
263+
264+ // ==========================================================================
265+ // Edge cases
266+ // ==========================================================================
267+
268+ #[ test]
269+ fn test_single_interface_project ( ) {
270+ let toml_str = r#"
271+ [project]
272+ name = "minimal"
273+
274+ [[interfaces]]
275+ name = "single"
276+ source = "api.yaml"
277+ format = "openapi"
278+ "# ;
279+
280+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
281+ idrisiser:: manifest:: validate ( & m) . unwrap ( ) ;
282+
283+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
284+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
285+ }
286+
287+ #[ test]
288+ fn test_many_interfaces ( ) {
289+ let toml_str = r#"
290+ [project]
291+ name = "multi"
292+
293+ [[interfaces]]
294+ name = "api-one"
295+ source = "a.yaml"
296+ format = "openapi"
297+
298+ [[interfaces]]
299+ name = "api-two"
300+ source = "b.proto"
301+ format = "protobuf"
302+
303+ [[interfaces]]
304+ name = "api-three"
305+ source = "c.h"
306+ format = "c-header"
307+
308+ [[interfaces]]
309+ name = "api-four"
310+ source = "d.tsig"
311+ format = "type-sig"
312+ "# ;
313+
314+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
315+ idrisiser:: manifest:: validate ( & m) . unwrap ( ) ;
316+ assert_eq ! ( m. interfaces. len( ) , 4 ) ;
317+
318+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
319+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
320+ }
321+
322+ #[ test]
323+ fn test_interface_with_preconditions_and_postconditions ( ) {
324+ let toml_str = r#"
325+ [project]
326+ name = "constrained"
327+
328+ [[interfaces]]
329+ name = "guarded-api"
330+ source = "api.yaml"
331+ format = "openapi"
332+ preconditions = ["auth_valid", "rate_limit_ok"]
333+ postconditions = ["status < 500", "body_valid"]
334+ invariants = ["db_consistent"]
335+ "# ;
336+
337+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
338+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
339+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
340+
341+ // Find the generated module and check it contains the constraints
342+ let idr_files: Vec < _ > = walkdir:: WalkDir :: new ( dir. path ( ) . join ( "idris2" ) )
343+ . into_iter ( )
344+ . filter_map ( |e| e. ok ( ) )
345+ . filter ( |e| e. path ( ) . extension ( ) . is_some_and ( |ext| ext == "idr" ) )
346+ . collect ( ) ;
347+ assert ! ( !idr_files. is_empty( ) ) ;
348+
349+ let content = fs:: read_to_string ( idr_files[ 0 ] . path ( ) ) . unwrap ( ) ;
350+ assert ! ( content. contains( "auth_valid" ) , "Precondition should appear" ) ;
351+ assert ! ( content. contains( "status < 500" ) , "Postcondition should appear" ) ;
352+ // Invariants are stored in the contract but rendered in a future phase
353+ assert ! ( m. interfaces[ 0 ] . invariants. contains( & "db_consistent" . to_string( ) ) ,
354+ "Invariant should be in manifest" ) ;
355+ }
356+
357+ #[ test]
358+ fn test_custom_module_prefix ( ) {
359+ let toml_str = r#"
360+ [project]
361+ name = "my-project"
362+ module-prefix = "Com.Example.Verified"
363+
364+ [[interfaces]]
365+ name = "api"
366+ source = "api.yaml"
367+ format = "openapi"
368+ "# ;
369+
370+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
371+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
372+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
373+
374+ let idr_path = dir. path ( ) . join ( "idris2/Com/Example/Verified/api.idr" ) ;
375+ assert ! ( idr_path. exists( ) , "Module should use custom prefix path: {:?}" , idr_path) ;
376+
377+ let content = fs:: read_to_string ( & idr_path) . unwrap ( ) ;
378+ assert ! ( content. contains( "module Com.Example.Verified.api" ) ) ;
379+ }
380+
381+ #[ test]
382+ fn test_validate_rejects_empty_interface_name ( ) {
383+ let toml_str = r#"
384+ [project]
385+ name = "test"
386+
387+ [[interfaces]]
388+ name = ""
389+ source = "api.yaml"
390+ format = "openapi"
391+ "# ;
392+
393+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
394+ let result = idrisiser:: manifest:: validate ( & m) ;
395+ assert ! ( result. is_err( ) ) ;
396+ }
397+
398+ #[ test]
399+ fn test_validate_rejects_empty_source ( ) {
400+ let toml_str = r#"
401+ [project]
402+ name = "test"
403+
404+ [[interfaces]]
405+ name = "api"
406+ source = ""
407+ format = "openapi"
408+ "# ;
409+
410+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
411+ let result = idrisiser:: manifest:: validate ( & m) ;
412+ assert ! ( result. is_err( ) ) ;
413+ }
414+
415+ // ==========================================================================
416+ // Aspect: generated code quality
417+ // ==========================================================================
418+
419+ #[ test]
420+ fn test_all_generated_idris2_has_spdx_header ( ) {
421+ let m = idrisiser:: manifest:: load_manifest ( "examples/user-api/idrisiser.toml" ) . unwrap ( ) ;
422+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
423+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
424+
425+ for entry in walkdir:: WalkDir :: new ( dir. path ( ) . join ( "idris2" ) )
426+ . into_iter ( )
427+ . filter_map ( |e| e. ok ( ) )
428+ . filter ( |e| e. path ( ) . extension ( ) . is_some_and ( |ext| ext == "idr" ) )
429+ {
430+ let content = fs:: read_to_string ( entry. path ( ) ) . unwrap ( ) ;
431+ assert ! (
432+ content. contains( "SPDX-License-Identifier" ) ,
433+ "Missing SPDX in {:?}" ,
434+ entry. path( )
435+ ) ;
436+ }
437+ }
438+
439+ #[ test]
440+ fn test_all_generated_idris2_is_total ( ) {
441+ let m = idrisiser:: manifest:: load_manifest ( "examples/user-api/idrisiser.toml" ) . unwrap ( ) ;
442+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
443+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
444+
445+ for entry in walkdir:: WalkDir :: new ( dir. path ( ) . join ( "idris2" ) )
446+ . into_iter ( )
447+ . filter_map ( |e| e. ok ( ) )
448+ . filter ( |e| e. path ( ) . extension ( ) . is_some_and ( |ext| ext == "idr" ) )
449+ {
450+ let content = fs:: read_to_string ( entry. path ( ) ) . unwrap ( ) ;
451+ assert ! (
452+ content. contains( "%default total" ) ,
453+ "Missing %%default total in {:?}" ,
454+ entry. path( )
455+ ) ;
456+ }
457+ }
458+
459+ #[ test]
460+ fn test_zig_bridge_has_proper_exports ( ) {
461+ let m = idrisiser:: manifest:: load_manifest ( "examples/user-api/idrisiser.toml" ) . unwrap ( ) ;
462+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
463+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
464+
465+ let zig_ffi = dir. path ( ) . join ( "zig/example_project_ffi.zig" ) ;
466+ let content = fs:: read_to_string ( & zig_ffi) . unwrap ( ) ;
467+
468+ // Every export should use C calling convention
469+ for line in content. lines ( ) {
470+ if line. contains ( "export fn" ) {
471+ assert ! (
472+ line. contains( "callconv(.C)" ) ,
473+ "Export missing callconv(.C): {}" ,
474+ line. trim( )
475+ ) ;
476+ }
477+ }
478+ }
479+
480+ #[ test]
481+ fn test_ipkg_references_all_modules ( ) {
482+ let m = idrisiser:: manifest:: load_manifest ( "examples/user-api/idrisiser.toml" ) . unwrap ( ) ;
483+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
484+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
485+
486+ let ipkg = fs:: read_to_string ( dir. path ( ) . join ( "example_project_verified.ipkg" ) ) . unwrap ( ) ;
487+
488+ // Should reference both interfaces
489+ assert ! ( ipkg. contains( "user_api" ) , "ipkg should reference user_api module" ) ;
490+ assert ! ( ipkg. contains( "core_lib" ) , "ipkg should reference core_lib module" ) ;
491+ }
492+
493+ // ==========================================================================
494+ // Proof config tests
495+ // ==========================================================================
496+
497+ #[ test]
498+ fn test_qtt_tracking_enabled ( ) {
499+ let toml_str = r#"
500+ [project]
501+ name = "qtt-test"
502+
503+ [[interfaces]]
504+ name = "api"
505+ source = "api.yaml"
506+ format = "openapi"
507+
508+ [proofs]
509+ qtt-tracking = true
510+ "# ;
511+
512+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
513+ assert ! ( m. proofs. qtt_tracking) ;
514+
515+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
516+ idrisiser:: codegen:: generate_all ( & m, dir. path ( ) . to_str ( ) . unwrap ( ) ) . unwrap ( ) ;
517+ }
518+
519+ #[ test]
520+ fn test_proof_defaults ( ) {
521+ let toml_str = r#"
522+ [project]
523+ name = "defaults"
524+
525+ [[interfaces]]
526+ name = "api"
527+ source = "x"
528+ format = "openapi"
529+ "# ;
530+
531+ let m: idrisiser:: manifest:: Manifest = toml:: from_str ( toml_str) . unwrap ( ) ;
532+ assert ! ( m. proofs. require_totality) ;
533+ assert ! ( m. proofs. round_trip_proofs) ;
534+ assert ! ( !m. proofs. qtt_tracking) ;
535+ assert_eq ! ( m. proofs. search_depth, 100 ) ;
536+ }
537+
538+ #[ test]
539+ fn test_library_api_convenience_function ( ) {
540+ // Test the lib.rs generate() convenience function
541+ let dir = tempfile:: tempdir ( ) . unwrap ( ) ;
542+ let result = idrisiser:: generate (
543+ "examples/user-api/idrisiser.toml" ,
544+ dir. path ( ) . to_str ( ) . unwrap ( ) ,
545+ ) ;
546+ assert ! ( result. is_ok( ) ) ;
547+ assert ! ( dir. path( ) . join( "idris2" ) . exists( ) ) ;
548+ }
0 commit comments