diff --git a/CLAUDE.md b/CLAUDE.md index e5478538..3c4c0473 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -89,7 +89,7 @@ cd coq && make proofs ### Proof Status -See `coq/STATUS.md` for the complete coverage matrix. Current: 585 Qed / 3 Admitted +See `coq/STATUS.md` for the complete coverage matrix. Current: 591 Qed / 3 Admitted (+2 `admit.` tactics) across `coq/Synth/`. The 50 selector-DSL rule theorems (`VcrSelRules.v`) are stated directly about the GENERATED model (VCR-ISA-001 #667: `rule_X := Gen.rule_X`, single source `VcrSelRulesGenerated.v` emitted diff --git a/artifacts/status.json b/artifacts/status.json index 9c5c3820..180ef7e5 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -10,12 +10,12 @@ "rocq_admit_tactics": 2, "rocq_admitted": 3, "rocq_axioms": 93, - "rocq_qed": 585, + "rocq_qed": 591, "sail_bridge_qed": 92, "sel_dsl_pilot_qed": 7, "sel_dsl_rule_qed": 50, "sel_dsl_rules": 50, "version": "0.49.0", "verus_spec_fns": 8, - "wasmcert_bridge_qed": 98 + "wasmcert_bridge_qed": 104 } diff --git a/artifacts/sw-verification.yaml b/artifacts/sw-verification.yaml index 27b0e2f9..1aa0cf09 100644 --- a/artifacts/sw-verification.yaml +++ b/artifacts/sw-verification.yaml @@ -478,12 +478,12 @@ artifacts: 32/64; CompCert 3.16 Integers.v for the underlying ops incl. rol/ror 217-222). WasmCertBridge.v proves a real-Qed op-level refinement lemma per op AND an executor-level lemma routing through the real exec_wasm_instr for - every WIRED op. HONEST SCOPE (named, not fabricated): (1) it is still a - hand TRANSCRIPTION of the pinned sources, not the real external dep — that - stays blocked on the unfree CompCert 3.16 the current nixpkgs pin - propagates; (2) the 6 i64 arithmetic/bitwise ops have op-level refinement - ONLY, because exec_wasm_instr returns None for their constructors (unwired - in the model). The WASM-side analogue of SailArmBridge.v (VCR-ISA-001). + EVERY i32 op and ALL 22 i64 ops (the six arithmetic/bitwise ops were wired + into exec_wasm_instr in the v0.50 batch — see SWVER-021). HONEST SCOPE + (named, not fabricated): it is still a hand TRANSCRIPTION of the pinned + sources, not the real external dep — that stays blocked on the unfree + CompCert 3.16 the current nixpkgs pin propagates. The WASM-side analogue of + SailArmBridge.v (VCR-ISA-001). status: implemented tags: [vcr-wasm, wasmcert, rocq, refinement, transcription, epic-242] links: @@ -494,8 +494,42 @@ artifacts: steps: run: "bazel test //coq:verify_proofs" coverage: > - coq/Synth/WASM/WasmCertBridge.v (98 Qed: i32 + i64 op-level and + coq/Synth/WASM/WasmCertBridge.v (104 Qed: i32 + i64 op-level and executor-level refinement lemmas + encoding/bit-level/rotate-boundary helpers) against coq/Synth/WASM/WasmCertReference.v; re-derived Qed - total 585 CI-gated by scripts/claim_check.py (claims.yaml + total 591 CI-gated by scripts/claim_check.py (claims.yaml wasmcert_bridge_qed flows to artifacts/status.json) + + - id: SWVER-021 + type: sw-verification + title: i64 add/sub/mul/and/or/xor wired into exec_wasm_instr — executor-level refinement (#242) + description: > + Verifies VCR-WASM-001: closes the former "op-level-only" residual for the + six i64 arithmetic/bitwise ops. exec_wasm_instr previously returned None + for the I64Add/I64Sub/I64Mul/I64And/I64Or/I64Xor constructors, so those + ops carried an op-level refinement lemma (I64.op = wasmcert_i64_op) but no + executor-level lemma through the real executor. This batch WIRES the six + ops into the model's match (pop2_i64 / VI64, mirroring their proven i32 + twins) and lands the six executor-level refinement theorems + (i64_{add,sub,mul,and,or,xor}_exec_refines_wasmcert), so all 22 i64 + integer ops now carry BOTH op-level and executor-level refinement. + exec_wasm_instr is the semantics model, NOT the code generator: the change + is byte-invisible (frozen_codegen_bytes 10/10 unchanged). HONEST SCOPE + (named): the reference remains a hand transcription of the pinned + coq9.0-wasm-2.2.0 sources; remaining WASM op coverage (div/rem trap rules, + clz/ctz/popcnt, wrap/extend/reinterpret conversions, memory, control flow) + is the named follow-up. + status: implemented + tags: [vcr-wasm, wasmcert, rocq, refinement, executor, epic-242] + links: + - type: verifies + target: VCR-WASM-001 + fields: + method: formal-proof + steps: + run: "bazel test //coq:verify_proofs && cargo test -p synth-cli --test frozen_codegen_bytes" + coverage: > + coq/Synth/WASM/WasmSemantics.v (six i64 arithmetic/bitwise arms wired + via pop2_i64 / VI64) + coq/Synth/WASM/WasmCertBridge.v (six + i64_*_exec_refines_wasmcert theorems, +6 Qed → 591 total); frozen + 10/10 confirms the semantics-model change does not alter compiled bytes diff --git a/claims.yaml b/claims.yaml index 008c91e4..33b3ebb0 100644 --- a/claims.yaml +++ b/claims.yaml @@ -189,12 +189,12 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-PROOF-COUNT-CLAUDE-MD doc: CLAUDE.md - text: "585 Qed / 3 Admitted" + text: "591 Qed / 3 Admitted" evidence: - kind: count-eq pattern: 'Qed\.' glob: ['coq/Synth/**/*.v'] - expect: 585 + expect: 591 - kind: count-eq pattern: 'Admitted\.' glob: ['coq/Synth/**/*.v'] @@ -202,16 +202,16 @@ claims: - id: SYNTH-PROOF-COUNT-STATUS-MD doc: coq/STATUS.md - text: "585 Qed / 3 Admitted" + text: "591 Qed / 3 Admitted" evidence: - kind: count-eq # headline + Total line must both agree - pattern: '585 Qed / 3 Admitted' + pattern: '591 Qed / 3 Admitted' glob: ['coq/STATUS.md'] expect: 2 - kind: count-eq pattern: 'Qed\.' glob: ['coq/Synth/**/*.v'] - expect: 585 + expect: 591 - kind: count-eq pattern: 'Admitted\.' glob: ['coq/Synth/**/*.v'] diff --git a/coq/STATUS.md b/coq/STATUS.md index 82b50695..42b74429 100644 --- a/coq/STATUS.md +++ b/coq/STATUS.md @@ -1,16 +1,17 @@ # Rocq Proof Suite — Honest Status -**Last Updated: 2026-07-17 (VCR-WASM-001 phase 3: recount 585 Qed / 3 Admitted, -+2 admit., crude `grep "Qed\."` over `coq/Synth/**/*.v` — same method as prior -recounts; +49 vs the prior 536 are the WasmCert-Coq i64 refinement batch in -`WasmCertBridge.v` (22 i64 ops transcribed from the same pinned -coq9.0-wasm-2.2.0 sources with line-level provenance: op-level refinement for -all 22 add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt/gt/le/ge, -plus executor-level for the 16 WIRED ops — the shifts, the two rotates, the 12 -comparisons; the 6 i64 arithmetic/bitwise ops are op-level-only, a NAMED -residual because `exec_wasm_instr` returns `None` for those constructors; still -a hand transcription, not the real external dep). The prior +47 vs 489 was the -i32 batch (19 ops); +**Last Updated: 2026-07-17 (VCR-WASM-001 phase 3 wiring: recount 591 Qed / 3 Admitted, ++2 admit., crude `grep "Qed\."` over `coq/Synth/**/*.v` — same method +as prior recounts; +6 vs the prior 585 are the six i64 arithmetic/bitwise +executor-level refinement theorems in `WasmCertBridge.v` +(add/sub/mul/and/or/xor). Those six ops are now WIRED in `exec_wasm_instr` +(pop2_i64 / VI64, mirroring their i32 twins), so their executor-level +refinement lands — the former "op-level-only" residual is CLOSED and ALL 22 i64 +integer ops now carry BOTH op-level and executor-level refinement. Still a hand +transcription, not the real external dep. The prior +49 vs 536 was the +WasmCert-Coq i64 op-level batch (22 ops transcribed from the same pinned +coq9.0-wasm-2.2.0 sources with line-level provenance); the +47 vs 489 before +that was the i32 batch (19 ops); prior recount context (#166): the -40 vs the prior 512 are the retired VCR-ISA-001 #667 cross-check lemmas of `VcrSelRulesGenCheck.v`: `VcrSelRules.v` now DEFINES every `rule_X` as the @@ -183,7 +184,7 @@ and predates the VcrSelRules (42), VcrSelPilot (7) and SailArmBridge (92) Qed; see the per-file breakdown below for current per-file counts. The T3 row and the headline total are re-derived by the claim gate. -**Total: 585 Qed / 3 Admitted (+2 admit.) across all files** (recount 2026-07-17, CI-gated via `claims.yaml`) +**Total: 591 Qed / 3 Admitted (+2 admit.) across all files** (recount 2026-07-17, CI-gated via `claims.yaml`) v0.10.0 PR 1: +2 T1 Qed (i64_add_correct, i64_sub_correct) and +9 infrastructure Qed (combine_i32_unsigned, carry_split_add, @@ -465,7 +466,7 @@ Recount 2026-07-10 (`grep -oE 'Qed\.'` / `'Admitted\.'` per file): | StateMonad.v | 3 | 0 | Infra | | WasmValues.v | 2 | 0 | Infra | | WasmCertReference.v | 0 | 0 | definitions only (VCR-WASM-001: WasmCert-Coq i32 AND i64 rules transcribed from the pinned coq9.0-wasm-2.2.0 sources with line-level provenance). PHASE 3 (v0.48, #242): the extra-coq-package bazel/nix HOOK is LANDED (blocker (1) closed) but the REAL dep stays PENDING and this file stays a hand transcription — nixpkgs pin 88d3861a ships wasmcert 2.2.0, which propagates the UNFREE compcert 3.16 (inria-compcert, meta.license.free=false); wasmcert >= 2.2.1 (drops CompCert) not yet in the pin, so the "trusted transcription" caveat is NOT yet retired | -| WasmCertBridge.v | 98 | 0 | Infra/T1-analogue (VCR-WASM-001 phase 2: 19 i32 ops; phase 3 (#242): 22 i64 ops — add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt/gt/le/ge, each with an op-level refinement Qed against the WasmCert reference, plus an executor-level Qed through the real `exec_wasm_instr` for the 16 WIRED ops (shifts + 2 rotates + 11 comparisons (incl. eqz)); the 6 i64 arithmetic/bitwise ops are op-level-only, a NAMED residual because `exec_wasm_instr` returns `None` for those constructors — plus the i64 encoding/bit-level/rotate-boundary helper Qed) | +| WasmCertBridge.v | 104 | 0 | Infra/T1-analogue (VCR-WASM-001 phase 2: 19 i32 ops; phase 3 (#242): 22 i64 ops — add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt/gt/le/ge, each with an op-level refinement Qed against the WasmCert reference, PLUS an executor-level Qed through the real `exec_wasm_instr` for ALL 22 ops. The v0.50 wiring batch (#242) WIRED the six arithmetic/bitwise ops (add/sub/mul/and/or/xor) into `exec_wasm_instr` (pop2_i64 / VI64), closing the former op-level-only residual — plus the i64 encoding/bit-level/rotate-boundary helper Qed) | | VcrSelPilot.v | 7 | 0 | T1 (register-polymorphic; VCR-SEL-001 go/abandon measurement) | | VcrSelRules.v | 42 | 0 | T1 (register-polymorphic; the WIRED VCR-SEL-001 increment-1+2+3+4 rule table — 40 rule theorems 1:1 with `coq/vcr_sel_rules.manifest`, coverage-gated by `//coq:vcr_sel_rules_coverage`, + 2 mod-32 helper lemmas #683. VCR-ISA-001 #667 increment 2: every `rule_X` is DEFINED as the GENERATED `Gen.rule_X` of `VcrSelRulesGenerated.v` — emitted from the shipped `sel_dsl::RULES` — so the theorems are stated directly about the shipped sequences; a table change regenerates `Gen` and breaks the matching Qed. The former `VcrSelRulesGenCheck.v` 40-lemma `reflexivity` gate is retired as vacuous/subsumed) | | **Total** | **585** | **3** | (+2 `admit.`; headline re-derived by the claim gate) | diff --git a/coq/Synth/WASM/WasmCertBridge.v b/coq/Synth/WASM/WasmCertBridge.v index c802ae5c..d4a9a7b6 100644 --- a/coq/Synth/WASM/WasmCertBridge.v +++ b/coq/Synth/WASM/WasmCertBridge.v @@ -9,10 +9,11 @@ [exec_wasm_instr]. - PHASE 3 (i64 batch, #242): add, sub, mul, and, or, xor, shl, shr_u, shr_s, rotl, rotr, eqz, eq, ne, lt_u, lt_s, gt_u, gt_s, le_u, le_s, - ge_u, ge_s — op-level refinement for all 22, plus executor-level for the - 16 ops WIRED in [exec_wasm_instr] (the shifts, the two rotates, and the - 11 comparisons (incl. eqz); see the named residual below for the 6 arithmetic/ - bitwise ops the model does not yet route). + ge_u, ge_s — op-level refinement for all 22, plus executor-level for ALL + 22 ops. As of the v0.50 wiring batch (#242) the six arithmetic/bitwise + ops (add/sub/mul/and/or/xor) are WIRED in [exec_wasm_instr] (pop2_i64 / + VI64, mirroring their i32 twins), so their executor-level refinement now + lands too — the former "op-level-only" residual is CLOSED. It is the WASM-side analogue of SailArmBridge.v's per-instruction bridge lemmas (VCR-ISA-001 / #667). @@ -28,12 +29,13 @@ wasmcert >= 2.2.1. NAMED RESIDUALS (not forced, not admitted): - - i64 add/sub/mul/and/or/xor have OP-LEVEL refinement only: synth's - [exec_wasm_instr] returns [None] for the [I64Add]/…/[I64Xor] constructors - (they are not wired in the model's match, unlike their i32 twins). Wiring - them is a semantics-model change, out of scope for a transcription batch. - - Remaining op coverage (div/rem trap rules, clz/ctz/popcnt, memory, - control flow) is the named follow-up for both widths. + - (CLOSED, v0.50 #242) i64 add/sub/mul/and/or/xor are now WIRED in + [exec_wasm_instr] and carry executor-level refinement — they previously + had OP-LEVEL refinement only because the model's match returned [None] for + those constructors. That gap is gone. + - Remaining op coverage (div/rem trap rules, clz/ctz/popcnt, the + wrap/extend/reinterpret conversions, memory, control flow) is the named + follow-up for both widths. NON-VACUITY (why a WRONG synth semantics fails this file): - No op-level lemma is [reflexivity]-only where a real gap exists: @@ -652,14 +654,13 @@ Qed. helpers below are the wordsize-64 duplicates of the i32 helpers (the same raw-vs-normalized [Z.testbit] / shift-count-collapse content, at 2^64). - HONEST SCOPE (named residuals). Two classes are DELIBERATELY not given - executor-level refinement: - - i64 add/sub/mul/and/or/xor: synth's [exec_wasm_instr] returns [None] for - these constructors ([I64Add]/[I64Sub]/…/[I64Xor] are not wired in the - model's match, unlike their i32 counterparts). We prove the OP-LEVEL - refinement ([I64.op = wasmcert_i64_op], genuine raw-vs-normalized content), - and NAME the missing executor routing as a residual — wiring them into the - model is a semantics change, out of scope for a transcription batch. + HONEST SCOPE. As of the v0.50 wiring batch (#242) ALL 22 i64 integer ops + carry BOTH op-level and executor-level refinement: + - i64 add/sub/mul/and/or/xor: now WIRED in synth's [exec_wasm_instr] + ([I64Add]/[I64Sub]/…/[I64Xor], pop2_i64 / VI64, mirroring their i32 + counterparts). Both the OP-LEVEL refinement ([I64.op = wasmcert_i64_op], + genuine raw-vs-normalized content) AND the executor-level routing are + proven — the former "op-level-only" residual is CLOSED. - i64 rotl/rotr: transcribed at the reference level (WasmCertReference.v) and proven op-level here; see the note at the rotate lemmas for the [n = 0] boundary discharge. *) @@ -1028,6 +1029,87 @@ Proof. reflexivity. Qed. +(** ** i64 executor-level refinement: arithmetic + bitwise. + [exec_wasm_instr] pushes exactly the WasmCert reference result. These six + ops (add/sub/mul/and/or/xor) are now WIRED in the model's match (pop2_i64 / + VI64), so their executor-level refinement lands with the same shape as the + i32 twins and the i64 shifts — closing the former "op-level-only" residual. + If an op were miswired (wrong operation, wrong operand order, wrong stack + shape) the theorem would be unprovable: the pushed value is pinned to the + INDEPENDENT reference. *) + +Theorem i64_add_exec_refines_wasmcert : forall v1 v2 s stack', + s.(stack) = VI64 v2 :: VI64 v1 :: stack' -> + exec_wasm_instr I64Add s = + Some (mkWasmState + (VI64 (wasmcert_i64_add v1 v2) :: stack') + s.(locals) s.(globals) s.(memory)). +Proof. + intros v1 v2 s stack' Hstack. + unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack. + rewrite <- i64_add_refines_wasmcert_op. reflexivity. +Qed. + +Theorem i64_sub_exec_refines_wasmcert : forall v1 v2 s stack', + s.(stack) = VI64 v2 :: VI64 v1 :: stack' -> + exec_wasm_instr I64Sub s = + Some (mkWasmState + (VI64 (wasmcert_i64_sub v1 v2) :: stack') + s.(locals) s.(globals) s.(memory)). +Proof. + intros v1 v2 s stack' Hstack. + unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack. + rewrite <- i64_sub_refines_wasmcert_op. reflexivity. +Qed. + +Theorem i64_mul_exec_refines_wasmcert : forall v1 v2 s stack', + s.(stack) = VI64 v2 :: VI64 v1 :: stack' -> + exec_wasm_instr I64Mul s = + Some (mkWasmState + (VI64 (wasmcert_i64_mul v1 v2) :: stack') + s.(locals) s.(globals) s.(memory)). +Proof. + intros v1 v2 s stack' Hstack. + unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack. + rewrite <- i64_mul_refines_wasmcert_op. reflexivity. +Qed. + +Theorem i64_and_exec_refines_wasmcert : forall v1 v2 s stack', + s.(stack) = VI64 v2 :: VI64 v1 :: stack' -> + exec_wasm_instr I64And s = + Some (mkWasmState + (VI64 (wasmcert_i64_and v1 v2) :: stack') + s.(locals) s.(globals) s.(memory)). +Proof. + intros v1 v2 s stack' Hstack. + unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack. + rewrite <- i64_and_refines_wasmcert_op. reflexivity. +Qed. + +Theorem i64_or_exec_refines_wasmcert : forall v1 v2 s stack', + s.(stack) = VI64 v2 :: VI64 v1 :: stack' -> + exec_wasm_instr I64Or s = + Some (mkWasmState + (VI64 (wasmcert_i64_or v1 v2) :: stack') + s.(locals) s.(globals) s.(memory)). +Proof. + intros v1 v2 s stack' Hstack. + unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack. + rewrite <- i64_or_refines_wasmcert_op. reflexivity. +Qed. + +Theorem i64_xor_exec_refines_wasmcert : forall v1 v2 s stack', + s.(stack) = VI64 v2 :: VI64 v1 :: stack' -> + exec_wasm_instr I64Xor s = + Some (mkWasmState + (VI64 (wasmcert_i64_xor v1 v2) :: stack') + s.(locals) s.(globals) s.(memory)). +Proof. + intros v1 v2 s stack' Hstack. + unfold exec_wasm_instr, pop2_i64, pop2. rewrite Hstack. + rewrite <- i64_xor_refines_wasmcert_op. reflexivity. +Qed. + (** ** i64 executor-level refinement: shifts. [exec_wasm_instr] pushes exactly the WasmCert reference result. Mirrors the i32 exec lemmas but through the i64 stack path (pop2_i64 / VI64). *) diff --git a/coq/Synth/WASM/WasmSemantics.v b/coq/Synth/WASM/WasmSemantics.v index 101f6a03..d8ee897b 100644 --- a/coq/Synth/WASM/WasmSemantics.v +++ b/coq/Synth/WASM/WasmSemantics.v @@ -324,6 +324,56 @@ Definition exec_wasm_instr (i : wasm_instr) (s : wasm_state) : option wasm_state | None => None end + (* i64 arithmetic operations (mirror the i32 arms via pop2_i64 / VI64) *) + | I64Add => + match pop2_i64 s with + | Some (v1, v2, s') => + let result := I64.add v1 v2 in + Some (push_value (VI64 result) s') + | None => None + end + + | I64Sub => + match pop2_i64 s with + | Some (v1, v2, s') => + let result := I64.sub v1 v2 in + Some (push_value (VI64 result) s') + | None => None + end + + | I64Mul => + match pop2_i64 s with + | Some (v1, v2, s') => + let result := I64.mul v1 v2 in + Some (push_value (VI64 result) s') + | None => None + end + + (* i64 bitwise operations *) + | I64And => + match pop2_i64 s with + | Some (v1, v2, s') => + let result := I64.and v1 v2 in + Some (push_value (VI64 result) s') + | None => None + end + + | I64Or => + match pop2_i64 s with + | Some (v1, v2, s') => + let result := I64.or v1 v2 in + Some (push_value (VI64 result) s') + | None => None + end + + | I64Xor => + match pop2_i64 s with + | Some (v1, v2, s') => + let result := I64.xor v1 v2 in + Some (push_value (VI64 result) s') + | None => None + end + (* i64 comparison operations *) | I64Eqz => match pop_i64 s with diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index c149678b..b0d66b5f 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -64,10 +64,10 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. | Track | Derived count(s) | What it covers | |-------|------------------|----------------| -| Rocq proof suite | 585 Qed / 3 Admitted (+2 `admit.` tactics) | T1 result-correspondence for all i32 and i64 selection; T2 existence-only for float/SIMD; trusted base: 93 Axiom/Parameter declarations | +| Rocq proof suite | 591 Qed / 3 Admitted (+2 `admit.` tactics) | T1 result-correspondence for all i32 and i64 selection; T2 existence-only for float/SIMD; trusted base: 93 Axiom/Parameter declarations | | Verified selector DSL (VCR-SEL-001) | 50 rules / 50 Qed (1:1, + 7 pilot Qed) | The Rocq-proved rules ARE the shipped lowering path for their covered ops; model generated from the shipped rule table (#667), so selector drift breaks the matching proof | | Sail/ASL ISA bridge (VCR-ISA-001) | 92 Qed | `coq/Synth/ARM/SailArmBridge.v` | -| WasmCert-Coq source anchor (VCR-WASM-001) | 98 Qed | `coq/Synth/WASM/WasmCertBridge.v` — i32 integer fragment refined against pinned WasmCert-Coq rules | +| WasmCert-Coq source anchor (VCR-WASM-001) | 104 Qed | `coq/Synth/WASM/WasmCertBridge.v` — i32 integer fragment refined against pinned WasmCert-Coq rules | | Kani (bounded model checking) | 18 harnesses | ARM encoder properties | | Verus (SMT contracts) | 8 spec functions | `synth-synthesis/src/contracts.rs` |