Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions docs/contracts/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
|----|----------|-------|--------|--------------------|-----------:|
Expand Down Expand Up @@ -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 |

4 changes: 2 additions & 2 deletions docs/contracts/conformance.md
Original file line number Diff line number Diff line change
Expand Up @@ -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) |
|---------|-----------|------------------------------|
Expand All @@ -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)<br>`spec/stdlib/bounded_profile_test.almd` (both-target test) |
| ALS-C1 | C-013 | `spec/wasm_cross/map_insertion_order.almd` (byte-compare)<br>`spec/wasm_cross/map_filter.almd` (byte-compare)<br>`spec/wasm_cross/map_fold.almd` (byte-compare)<br>`spec/wasm_cross/map_index_order.almd` (byte-compare)<br>`spec/wasm_cross/map_core_trio.almd` (byte-compare)<br>`spec/wasm_cross/map_fold_heap_accumulator.almd` (byte-compare)<br>`spec/wasm_cross/map_of_maps_value.almd` (byte-compare)<br>`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)<br>`spec/wasm_cross/map_filter.almd` (byte-compare)<br>`spec/wasm_cross/map_fold.almd` (byte-compare)<br>`spec/wasm_cross/map_index_order.almd` (byte-compare)<br>`spec/wasm_cross/map_core_trio.almd` (byte-compare)<br>`spec/wasm_cross/map_fold_heap_accumulator.almd` (byte-compare)<br>`spec/wasm_cross/map_of_maps_value.almd` (byte-compare)<br>`spec/wasm_cross/map_set_index_threshold.almd` (byte-compare)<br>`spec/wasm_cross/json_to_map_duplicate_keys.almd` (byte-compare) |
| ALS-C2 | C-014 | `spec/wasm_cross/set_insertion_order.almd` (byte-compare)<br>`spec/wasm_cross/set_index_order.almd` (byte-compare)<br>`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)<br>`spec/wasm_cross/deep_eq_heap.almd` (byte-compare)<br>`spec/wasm_cross/map_set_eq.almd` (byte-compare)<br>`spec/wasm_cross/variant_record_literal_equality.almd` (byte-compare)<br>`spec/wasm_cross/unique_non_flat_element.almd` (byte-compare)<br>`spec/wasm_cross/list_of_tuples_equality.almd` (byte-compare)<br>`spec/wasm_cross/map_rich_variant_key.almd` (byte-compare)<br>`spec/wasm_cross/value_deep_eq.almd` (byte-compare)<br>`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)<br>`spec/wasm_cross/list_remove_at_oob.almd` (byte-compare)<br>`spec/wasm_cross/list_swap_oob.almd` (byte-compare)<br>`spec/wasm_cross/list_slice_oob.almd` (byte-compare)<br>`spec/wasm_cross/list_sort_short.almd` (byte-compare)<br>`spec/wasm_cross/list_with_capacity.almd` (byte-compare)<br>`spec/wasm_cross/negative_offset_and_width_totality.almd` (byte-compare)<br>`spec/wasm_cross/repeat_size_ceiling.almd` (byte-compare)<br>`spec/wasm_cross/matrix_slice_rows_domain.almd` (byte-compare)<br>`spec/wasm_fail/matrix_conv1d_stride_aborts.almd` (both-target test) |
Expand Down
10 changes: 10 additions & 0 deletions docs/contracts/contracts.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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" },
]
2 changes: 1 addition & 1 deletion docs/specs/als/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down
7 changes: 7 additions & 0 deletions proofs/contract-provenance.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
16 changes: 13 additions & 3 deletions ref/src/stdlib_ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -577,12 +577,22 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec<Value>) -> Result<Result<Valu
"json.to_map" => {
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)))
Expand Down
45 changes: 45 additions & 0 deletions spec/wasm_cross/json_to_map_duplicate_keys.almd
Original file line number Diff line number Diff line change
@@ -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}")
}
Loading