[codex] Implement PR11.10c built-in map

[agentc1]

Summary

Implements PR11.10c as the minimal built-in map of (K, V) wedge.

This adds:

• map of (K, V) as a source type constructor
• contextual builtins:
  • contains(m, key)
  • get(m, key)
  • set(m, key, value)
  • remove(m, key)
• lowering to the existing growable-array-of-tuple machinery with no typed/MIR/safei version bump
• positive, negative, build, interface, AST, and proof coverage for the new map surface

Why

This is the next container slice after PR11.10b. It establishes the first admitted map surface without introducing a second container runtime or method syntax.

The implementation keeps maps as an unsorted growable sequence of (K, V) entries with linear lookup and explicitly unspecified iteration order.

Impact

User-facing changes:

• map of (K, V) is now accepted
• set mutates a writable map in statement position
• get and remove return optional V
• for entry of m iterates (K, V) tuples

Compiler/runtime impact:

• no artifact format bump
• no new dedicated map runtime package
• map operations reuse existing growable-array and tuple lowering paths

Validation

Validated in the implementation checkout before publishing this clean branch:

• cd compiler_impl && alr build
• python3 scripts/run_tests.py -> 717 passed, 1 skipped, 0 failed
• python3 scripts/run_samples.py -> 19 passed, 0 failed
• python3 scripts/run_proofs.py -> 176 proved, 0 failed

The branch published here was recreated from refreshed upstream/main and the PR11.10c patch applied cleanly onto that base.

[Copilot]

Pull request overview

Implements the PR11.10c “built-in map” surface by adding map of (K, V) as a first-class source type constructor and lowering map operations to the existing growable-array-of-(K, V) tuple machinery, with accompanying docs and test/proof coverage.

Changes:

• Add parsing, AST emission/schema, and type resolution for map of (K, V).
• Implement contextual map builtins (contains, get, set, remove) via resolver validation + desugaring/lowering.
• Add positive/negative/interface/build tests and wire them into the test + proof harnesses; update docs/spec.

Reviewed changes

Copilot reviewed 25 out of 25 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
tests/positive/pr1110c_map_basics.safe	Positive coverage for default-empty maps, iteration over (K,V) tuples, and basic map ops.
tests/negative/neg_pr1110c_set_non_map.safe	Reject set when first arg isn’t a map.
tests/negative/neg_pr1110c_set_constant.safe	Reject set when the map target is not writable.
tests/negative/neg_pr1110c_remove_stmt.safe	Reject remove used as a statement (must be expression).
tests/negative/neg_pr1110c_remove_constant.safe	Reject remove when the map target is not writable.
tests/negative/neg_pr1110c_map_value_mismatch.safe	Reject set with a value type mismatch.
tests/negative/neg_pr1110c_map_key_mismatch.safe	Reject get with a key type mismatch.
tests/negative/neg_pr1110c_map_bad_key.safe	Reject disallowed map key types.
tests/interfaces/provider_map.safe	Interface test provider exporting map-valued APIs.
tests/interfaces/client_map.safe	Interface test client consuming provider’s map API.
tests/build/pr1110c_map_build.safe	Build/run coverage for update + remove semantics and .length.
tests/build/pr1110c_map_string_build.safe	Build/run coverage for string-key/string-value maps.
tests/build/pr1110c_map_list_build.safe	Build/run coverage for maps with container (list) values.
spec/08-syntax-summary.md	Syntax summary updates for map_type_spec and builtin call admission rules.
scripts/run_tests.py	Registers new positive/interface/build test cases for maps.
scripts/run_proofs.py	Adds PR11.10c proof checkpoint fixture group execution and summary.
scripts/_lib/proof_inventory.py	Adds PR11.10c checkpoint fixture manifest and includes it in coverage roots.
docs/tutorial.md	Tutorial section documenting the new map surface and examples.
docs/PR11.x-series-proposed.md	PR11.10c spec updates (decisions/scope/notes) for map wedge.
compiler/ast_schema.json	Extends AST schema with MapTypeSpec and allows it in relevant type positions.
compiler_impl/src/safe_frontend-check_parse.adb	Adds parser support + internal naming for map of (K, V) type specs.
compiler_impl/src/safe_frontend-check_model.ads	Adds Type_Spec_Map and key/value fields to the frontend type-spec model.
compiler_impl/src/safe_frontend-check_emit.adb	Emits MapTypeSpec nodes in AST JSON output.
compiler_impl/src/safe_frontend-check_resolve.adb	Resolves map types to growable arrays of 2-tuples; validates map builtins; desugars/lowerings for map ops.
compiler_impl/src/safe_frontend-ada_emit.adb	Updates synthetic-type collection / type lookup paths needed for new map/tuple helper emission.

---

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