diff --git a/docs/contracts/README.md b/docs/contracts/README.md index ad71436c..6b5c0819 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -28,10 +28,10 @@ Evidence classes (weakest → strongest): `doc-only` < `by-construction` < Measured per contract in [`proofs/contract-provenance.toml`](../../proofs/contract-provenance.toml) (`scripts/check-contract-provenance.py`: the instant the id entered this ledger against the instant -the `since` release was tagged). Of 379 contracts: **requirements-first 74** (two-repo regime, since 2026-08-20), +the `since` release was tagged). Of 380 contracts: **requirements-first 75** (two-repo regime, since 2026-08-20), contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 17. -379 contracts +380 contracts | ID | Contract | Since | Status | Strongest Evidence | # Fixtures | |----|----------|-------|--------|--------------------|-----------:| @@ -414,4 +414,5 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1 | C-377 | net tcp: loopback, handle numbering, EOF, close, is_open and tcp_local_port agree on native, the embedded wasm lane and the stock WASI 0.3 component | 0.68.0 | active | fixture | 0 | | C-378 | net tcp: every failure reads as errno-free classified text from one table, identical on native, the embedded wasm lane and the stock WASI 0.3 component | 0.68.0 | active | fixture | 0 | | C-379 | net tcp: timeouts and tcp_available are guest-enforced on the stock WASI 0.3 component and answer what native and the embedded wasm lane answer | 0.68.0 | active | fixture | 0 | +| C-380 | json.to_map holds one entry per key: a repeated object key keeps its first position and takes its last value, on every leg | 0.68.0 | active | fixture | 1 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 0ac47a22..3262bb7f 100644 --- a/docs/contracts/conformance.md +++ b/docs/contracts/conformance.md @@ -11,7 +11,7 @@ > (spec-coverage + evidence-class >= fixture for every active contract), so this > page cannot legitimately contain an empty Fixtures cell. -134 normative sections; 828 distinct executable fixtures. +134 normative sections; 829 distinct executable fixtures. | Section | Contracts | Fixtures (how CI runs each) | |---------|-----------|------------------------------| @@ -26,7 +26,7 @@ | ALS-B9 | C-316 | `tests/diagnostics/e076-bounded-effect-outside-capability/broken.almd` (checker) | | ALS-B10 | C-317 | `tests/diagnostics/e077-bounded-float-arithmetic/broken.almd` (checker) | | ALS-B11 | C-318 | `tests/diagnostics/e078-bounded-early-exit-in-loop/broken.almd` (checker)
`spec/stdlib/bounded_profile_test.almd` (both-target test) | -| ALS-C1 | C-013 | `spec/wasm_cross/map_insertion_order.almd` (byte-compare)
`spec/wasm_cross/map_filter.almd` (byte-compare)
`spec/wasm_cross/map_fold.almd` (byte-compare)
`spec/wasm_cross/map_index_order.almd` (byte-compare)
`spec/wasm_cross/map_core_trio.almd` (byte-compare)
`spec/wasm_cross/map_fold_heap_accumulator.almd` (byte-compare)
`spec/wasm_cross/map_of_maps_value.almd` (byte-compare)
`spec/wasm_cross/map_set_index_threshold.almd` (byte-compare) | +| ALS-C1 | C-013, C-380 | `spec/wasm_cross/map_insertion_order.almd` (byte-compare)
`spec/wasm_cross/map_filter.almd` (byte-compare)
`spec/wasm_cross/map_fold.almd` (byte-compare)
`spec/wasm_cross/map_index_order.almd` (byte-compare)
`spec/wasm_cross/map_core_trio.almd` (byte-compare)
`spec/wasm_cross/map_fold_heap_accumulator.almd` (byte-compare)
`spec/wasm_cross/map_of_maps_value.almd` (byte-compare)
`spec/wasm_cross/map_set_index_threshold.almd` (byte-compare)
`spec/wasm_cross/json_to_map_duplicate_keys.almd` (byte-compare) | | ALS-C2 | C-014 | `spec/wasm_cross/set_insertion_order.almd` (byte-compare)
`spec/wasm_cross/set_index_order.almd` (byte-compare)
`spec/wasm_cross/map_set_index_threshold.almd` (byte-compare) | | ALS-C3 | C-015, C-124, C-185 | `spec/wasm_cross/compound_eq.almd` (byte-compare)
`spec/wasm_cross/deep_eq_heap.almd` (byte-compare)
`spec/wasm_cross/map_set_eq.almd` (byte-compare)
`spec/wasm_cross/variant_record_literal_equality.almd` (byte-compare)
`spec/wasm_cross/unique_non_flat_element.almd` (byte-compare)
`spec/wasm_cross/list_of_tuples_equality.almd` (byte-compare)
`spec/wasm_cross/map_rich_variant_key.almd` (byte-compare)
`spec/wasm_cross/value_deep_eq.almd` (byte-compare)
`spec/wasm_cross/fan_any_early_winner.almd` (byte-compare) | | ALS-C4 | C-034, C-354 | `spec/wasm_cross/list_insert_clamp.almd` (byte-compare)
`spec/wasm_cross/list_remove_at_oob.almd` (byte-compare)
`spec/wasm_cross/list_swap_oob.almd` (byte-compare)
`spec/wasm_cross/list_slice_oob.almd` (byte-compare)
`spec/wasm_cross/list_sort_short.almd` (byte-compare)
`spec/wasm_cross/list_with_capacity.almd` (byte-compare)
`spec/wasm_cross/negative_offset_and_width_totality.almd` (byte-compare)
`spec/wasm_cross/repeat_size_ceiling.almd` (byte-compare)
`spec/wasm_cross/matrix_slice_rows_domain.almd` (byte-compare)
`spec/wasm_fail/matrix_conv1d_stride_aborts.almd` (both-target test) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index db0f3df9..9e41a3ce 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -4627,3 +4627,13 @@ status = "active" evidence = [ { path = "spec/embedded_cross/net_tcp_timeouts.almd", class = "fixture" }, ] +[[contract]] +id = "C-380" +spec = "ALS-C1" +title = "json.to_map holds one entry per key: a repeated object key keeps its first position and takes its last value, on every leg" +statement = "ALS-C1 (almide/almide#3700): `json.to_map(v)` of an object answers `some(map)` whose entries are the object's fields folded as one upsert each, in field order. A key the object repeats keeps the POSITION of its first occurrence and takes the VALUE of its last, so the map holds that key exactly once, the same rule as re-assigning an existing key (ALS-C1). A Str field value is taken verbatim, and any other value is its `value.stringify` text (null, Bool, numbers, arrays and objects alike). A non-object is `none`. An object can carry a repeated key: `value.object` accepts one and `json.parse` keeps one. Before this contract the wasm leg wrote every field as its own entry: `len` counted the key twice, `get` answered the first value, iteration listed both, and `==` against the deduplicated map was false, while native answered with one entry. The reference evaluator answered `none` for any non-Str value and did not deduplicate either." +since = "0.68.0" +status = "active" +evidence = [ + { path = "spec/wasm_cross/json_to_map_duplicate_keys.almd", class = "fixture" }, +] diff --git a/docs/specs/als/README.md b/docs/specs/als/README.md index e1396800..019c94b6 100644 --- a/docs/specs/als/README.md +++ b/docs/specs/als/README.md @@ -23,7 +23,7 @@ | ID | Section | Contracts | |----|---------|-----------| -| [ALS-C1](./collections.md#als-c1-map-の順序規範) | Map の順序規範 | C-013 | +| [ALS-C1](./collections.md#als-c1-map-の順序規範) | Map の順序規範 | C-013, C-380 | | [ALS-C2](./collections.md#als-c2-set-の順序規範) | Set の順序規範 | C-014 | | [ALS-C3](./collections.md#als-c3-構造的等価) | 構造的等価 | C-015, C-124, C-185 | | [ALS-C4](./collections.md#als-c4-範囲外アクセスの縮退規則) | 範囲外アクセスの縮退規則 | C-034, C-354 | diff --git a/proofs/contract-provenance.toml b/proofs/contract-provenance.toml index 48535eb5..8fc887c5 100644 --- a/proofs/contract-provenance.toml +++ b/proofs/contract-provenance.toml @@ -2849,3 +2849,10 @@ since = "0.68.0" entry = "2026-10-13T01:40:00+09:00" entry_commit = "2d345882" class = "requirements-first" + +[[contract]] +id = "C-380" +since = "0.68.0" +entry = "2026-10-14T08:56:29+09:00" +entry_commit = "0249441" +class = "requirements-first" diff --git a/ref/src/stdlib_ext.rs b/ref/src/stdlib_ext.rs index 2f647b32..6fdf26a0 100644 --- a/ref/src/stdlib_ext.rs +++ b/ref/src/stdlib_ext.rs @@ -577,12 +577,22 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec) -> Result { arity(name, &args, 1)?; Ok(match want_dyn(name, &args[0])? { + // C-380: one entry per key — a repeated key keeps its first + // position and takes its last value (an upsert per field); a + // Str value is taken verbatim, any other is its stringify. Dyn::O(fields) => { let mut out: Vec<(Value, Value)> = Vec::new(); for (k, v) in fields.iter() { - match v { - Dyn::S(s) => out.push((Value::Str(k.clone()), Value::Str(s.clone()))), - _ => return Ok(Ok(Value::None)), + let text = match v { + Dyn::S(s) => Value::Str(s.clone()), + other => Value::str(&dyn_text(other)), + }; + match out + .iter_mut() + .find(|(ok, _)| matches!(ok, Value::Str(a) if *a == *k)) + { + Some(slot) => slot.1 = text, + None => out.push((Value::Str(k.clone()), text)), } } some(Value::Map(Rc::new(out))) diff --git a/spec/wasm_cross/json_to_map_duplicate_keys.almd b/spec/wasm_cross/json_to_map_duplicate_keys.almd new file mode 100644 index 00000000..204d3720 --- /dev/null +++ b/spec/wasm_cross/json_to_map_duplicate_keys.almd @@ -0,0 +1,45 @@ +// @contract: C-380 +// json.to_map builds a Map, and a Map holds one entry per key (almide/almide#3700). +// An object can repeat a key (value.object accepts it, and so does json.parse), +// and the repeated key must not reach the map twice. It keeps the position of its +// first occurrence and takes the value of its last, as an upsert per field would. +// A Str value is taken verbatim; any other value is its value.stringify text. A +// non-object is none. Every later read of the map (len, get, iteration, equality) +// then agrees across targets. +import json + +fn show(label: String, v: Value) -> Unit = { + match json.to_map(v) { + some(m) => { + println("${label} ${m} len=${map.len(m)}") + for (k, x) in m { + println(" ${k} -> ${x} get=${map.get(m, k)}") + } + }, + none => println("${label} none"), + } +} + +fn main() -> Unit = { + show("twice", value.object([("k", value.int(1)), ("k", value.int(2))])) + show( + "first-position", + value.object([("a", value.str("x")), ("b", value.bool(true)), ("a", value.str("y"))]), + ) + show( + "mixed", + value.object([ + ("s", value.str("plain")), + ("n", value.null()), + ("f", value.float(1.5)), + ("arr", value.array([value.int(1)])), + ("s", value.array([])) + ]), + ) + show("parsed", json.parse("{\"k\":1,\"j\":\"two\",\"k\":{\"x\":3}}") ?? value.null()) + show("empty", value.object([])) + show("not-object", value.array([value.int(1)])) + let a = json.to_map(value.object([("k", value.int(1)), ("k", value.int(2))])) ?? map.new() + let b = json.to_map(value.object([("k", value.int(2))])) ?? map.new() + println("equal=${a == b}") +}