[codex] Implement PR11.11b structural interfaces

[agentc1]

Summary

• add Safe structural interfaces as compile-time operation contracts with interface declarations, parameter-position use, and structural satisfaction checking
• specialize local/private interface-constrained subprogram bodies to concrete clones before MIR, while rejecting public interface-constrained bodies in the PR11.11b subset
• export/import interface contract metadata through typed-v5 and safei-v4, and add tests, proofs, and docs for the shipped interface surface

Why

PR11.11b is the next composition milestone after method syntax. This lands named structural interfaces with zero runtime dispatch by keeping them as compile-time contracts only and lowering interface-constrained bodies away before MIR.

Validation

• cd compiler_impl && alr build
• python3 scripts/run_tests.py -> 745 passed, 1 skipped, 0 failed
• python3 scripts/run_samples.py -> 19 passed, 0 failed
• python3 scripts/run_proofs.py -> 181 proved, 0 failed
• PR11.11b checkpoint: 2 proved, 0 failed

[Copilot]

Pull request overview

This PR implements the PR11.11b subset of Safe structural interfaces as compile-time-only operation contracts, including parsing/AST/schema support, satisfaction checking, and specialization of local/private interface-constrained bodies into concrete clones prior to MIR emission.

Changes:

• Add type X is interface declarations with signature-only receiver members and enforce PR11.11b subset restrictions (parameter-position only, no interface objects/returns, reject public interface-constrained bodies).
• Implement structural satisfaction checking and clone-based specialization of interface-constrained subprogram bodies, while ensuring templates are not lowered/emitted to MIR/Ada.
• Bump and validate emitted artifact contracts (typed-v5, safei-v4) and add tests/docs/proof fixtures for the new surface.

Reviewed changes

Copilot reviewed 31 out of 31 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/positive/pr1111b_interface_local.safe	Positive local interface + satisfaction + call syntax coverage.
tests/negative/neg_pr1111b_public_interface_body.safe	Reject public interface-constrained body in PR11.11b subset.
tests/negative/neg_pr1111b_missing_member.safe	Reject interface satisfaction when required member is missing.
tests/negative/neg_pr1111b_interface_return.safe	Reject interface types in return positions.
tests/negative/neg_pr1111b_interface_object.safe	Reject interface-typed objects (non-parameter positions).
tests/negative/neg_pr1111b_interface_member_no_receiver.safe	Reject interface member specs without receiver syntax.
tests/negative/neg_pr1111b_interface_free_call.safe	Reject interface-member calls using free-call syntax (vs method syntax).
tests/interfaces/provider_printable.safe	Export a public interface + concrete provider type for cross-unit tests.
tests/interfaces/client_printable.safe	Cross-unit satisfaction test using imported interface contract.
tests/interfaces/client_printable_ambiguous.safe	Cross-unit ambiguous satisfaction negative case.
tests/build/pr1111b_interface_builtin_build.safe	Build/run coverage for interfaces satisfied by builtin container operations.
spec/08-syntax-summary.md	Add grammar and syntax notes for structural interface declarations and restrictions.
spec/02-restrictions.md	Clarify exclusion applies to Ada interface/tagged types, not Safe structural interfaces.
scripts/validate_output_contracts.py	Extend contract validator for interface_members; bump typed/safei versions.
scripts/validate_ast_output.py	Admit InterfaceTypeDefinition node in AST validation allowlist.
scripts/run_tests.py	Add PR11.11b positive/build fixtures and cross-unit interface test cases.
scripts/run_proofs.py	Add PR11.11b checkpoint proof fixture group.
scripts/_lib/proof_inventory.py	Register PR11.11b checkpoint fixtures in proof inventory.
docs/tutorial.md	Document structural interfaces and PR11.11b subset limitations in the tutorial.
docs/PR11.x-series-proposed.md	Update PR11.11b proposal text to match implemented subset and behavior.
docs/artifact_contract.md	Bump frozen artifact formats to typed-v5 and safei-v4 and document interface_members.
compiler/ast_schema.json	Add InterfaceTypeDefinition AST node schema.
compiler_impl/src/safe_frontend-mir_model.ads	Add MIR-model structs for interface member signatures in type descriptors.
compiler_impl/src/safe_frontend-interfaces.adb	Parse interface_members from imported interface/type descriptors; accept safei-v4.
compiler_impl/src/safe_frontend-check_resolve.adb	Implement interface typing rules, satisfaction, template specialization, and template suppression.
compiler_impl/src/safe_frontend-check_parse.adb	Parse type ... is interface with indented signature-only members and validation.
compiler_impl/src/safe_frontend-check_model.ads	Add interface decl kind/members and flags for synthetic/interface-template subprograms.
compiler_impl/src/safe_frontend-check_lower.adb	Skip lowering interface templates to MIR graphs.
compiler_impl/src/safe_frontend-check_emit.adb	Emit interface AST nodes and interface_members; bump to typed-v5/safei-v4; suppress template/synthetic executables.
compiler_impl/src/safe_frontend-ada_emit.adb	Avoid emitting Ada for interface types and interface-template subprograms.
compiler_impl/README.md	Update documentation to typed-v5 / safei-v4 terminology.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.