RHL-16 + RHL-2: vocabulary v2 and corpus v2; ruchy fix --safe; ruchy vocab

CHANGELOG.md

@@ -7,6 +7,28 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added — RHL-16 and RHL-2: vocabulary v2, `ruchy fix --safe`, `ruchy vocab` (RHL-001)
+
+- `vocab/fleet-v2.yaml`, `vocab/tickets-v2.yaml`: every v1 term carried forward,
+  each with its own `-v2` contract. `file ticket` declares the attributes
+  `title` and `label`; `ticket count` (the number of tickets a run files) is a
+  measure with no effect. v1 is unchanged.
+- `docs/rhl/breaks/v2/`: the 12 valid programs rewritten so each checks clean
+  under v2, and the six planted-break classes regenerated from them. Every v2
+  break yields its pre-registered code on the mutated line, new relative to its
+  base; v2 has no known-defect exceptions. `docs/rhl/PREREGISTRATION.sha256`
+  only adds lines. Details: `docs/rhl/rhl-16-v2.md`.
+- The checker reads a `with … end` block under an action that declares
+  attributes as attribute assignments (name and type checked). An unknown
+  attribute with no near match is RHL-V001 with the declared names in
+  `expected`.
+- `ruchy fix --safe <file.rhl>` applies every safe fix, re-checks the whole
+  file, and reverts any fix after which the error count rose. It is idempotent
+  and never applies a fix with two candidates.
+- `ruchy vocab list | show | validate [--format json]`, backed by the checker's
+  own loader. `contracts/rhl-vocabulary-shape-v1.yaml` states the shape every
+  vocabulary satisfies. Details: `docs/rhl/rhl-2.md`.
+
 ### Fixed — RHLGA-1: `ruchy doc` tests no longer rewrite tracked files
 
 - `tests/cli_contract_doc.rs` ran `ruchy doc` with the repository as the

contracts/rhl-fleet-disk-free-of-v2.yaml

@@ -0,0 +1,64 @@
+metadata:
+  version: "2.0.0"
+  author: "RHL-16"
+  description: "RHL-16 v2 contract for vocabulary term 'disk free of' (fleet v2, kind: measure)"
+  crate: "ruchy"
+  references:
+    - "RHL-001 §3.4"
+
+equations:
+  disk_free_of_shape:
+    formula: "kind('disk free of') = measure ∧ gives('disk free of') = Size"
+    domain: "t ∈ vocabulary fleet v2 terms named 'disk free of'"
+    invariants:
+      - "term kind is one of {noun, measure, action, unit, entity} (RHL-001 §3.4)"
+      - "term result type ('gives') is Size"
+      - "term declares effect 'read disk' (RHL-001 §3.1 rule 6)"
+      - "lowers_to stays the unbound marker `[U]` until RHL-4 — RHL-16 does not bind lowering"
+
+proof_obligations:
+  - type: invariant
+    property: "Term 'disk free of' carries a contract template on disk (F6)"
+    formal: "contract('disk free of') exists"
+    applies_to: all
+  - type: invariant
+    property: "Term 'disk free of' kind is drawn from RHL's closed kind list"
+    formal: "kind('disk free of') ∈ {noun, measure, action, unit, entity}"
+    applies_to: all
+
+falsification_tests:
+  - id: FALSIFY-RHL-FLEET-DISK-FREE-OF-V2-001
+    rule: "Vocabulary term contract must exist (RHL-001 F6)"
+    test: "test_rhl16_v2_every_term_has_an_existing_contract"
+    prediction: "verified"
+    if_fails: "Contract violation — RHL-001 F6: term 'disk free of' has no contract template"
+
+  - id: FALSIFY-RHL-FLEET-DISK-FREE-OF-V2-002
+    rule: "Vocabulary term kind is drawn from the closed list"
+    test: "test_rhl16_v2_carries_every_v1_term_forward"
+    prediction: "verified"
+    if_fails: "Contract violation — term 'disk free of' kind not in {noun, measure, action, unit, entity}"
+
+# NOT APPLICABLE, declared because `pv validate` requires the block. A vocabulary
+# term contract states a property of YAML bytes on disk; Kani symbolically executes
+# Rust and cannot reach a file system. Declaring a harness that does not exist is the
+# practice KANIDEBT-1 was filed against, so it is marked rather than pretended.
+kani_harnesses:
+  - id: KANI-RHL-FLEET-DISK-FREE-OF-V2-001
+    obligation: PO-RHL-FLEET-DISK-FREE-OF-V2-001
+    property: "NOT APPLICABLE — a vocabulary term contract is a property of YAML bytes on disk, outside Kani's reach"
+    bound: 1
+    strategy: bounded_int
+    harness: none
+    status: declared_not_implemented
+    discharged_by: "test_rhl16_v2_every_term_has_an_existing_contract"
+
+qa_gate:
+  id: QA-RHL-FLEET-DISK-FREE-OF-V2
+  name: "rhl fleet vocabulary v2 term: disk free of"
+  min_coverage: 1.0
+  max_complexity: 10
+  required_tests:
+    - test_rhl16_v2_every_term_has_an_existing_contract
+    - test_rhl16_v2_carries_every_v1_term_forward
+    - test_rhl16_v2_lowers_to_and_sigma_entity_stay_unbound

contracts/rhl-fleet-disk-usage-of-v2.yaml

@@ -0,0 +1,64 @@
+metadata:
+  version: "2.0.0"
+  author: "RHL-16"
+  description: "RHL-16 v2 contract for vocabulary term 'disk usage of' (fleet v2, kind: measure)"
+  crate: "ruchy"
+  references:
+    - "RHL-001 §3.4"
+
+equations:
+  disk_usage_of_shape:
+    formula: "kind('disk usage of') = measure ∧ gives('disk usage of') = Size"
+    domain: "t ∈ vocabulary fleet v2 terms named 'disk usage of'"
+    invariants:
+      - "term kind is one of {noun, measure, action, unit, entity} (RHL-001 §3.4)"
+      - "term result type ('gives') is Size"
+      - "term declares effect 'read disk' (RHL-001 §3.1 rule 6)"
+      - "lowers_to stays the unbound marker `[U]` until RHL-4 — RHL-16 does not bind lowering"
+
+proof_obligations:
+  - type: invariant
+    property: "Term 'disk usage of' carries a contract template on disk (F6)"
+    formal: "contract('disk usage of') exists"
+    applies_to: all
+  - type: invariant
+    property: "Term 'disk usage of' kind is drawn from RHL's closed kind list"
+    formal: "kind('disk usage of') ∈ {noun, measure, action, unit, entity}"
+    applies_to: all
+
+falsification_tests:
+  - id: FALSIFY-RHL-FLEET-DISK-USAGE-OF-V2-001
+    rule: "Vocabulary term contract must exist (RHL-001 F6)"
+    test: "test_rhl16_v2_every_term_has_an_existing_contract"
+    prediction: "verified"
+    if_fails: "Contract violation — RHL-001 F6: term 'disk usage of' has no contract template"
+
+  - id: FALSIFY-RHL-FLEET-DISK-USAGE-OF-V2-002
+    rule: "Vocabulary term kind is drawn from the closed list"
+    test: "test_rhl16_v2_carries_every_v1_term_forward"
+    prediction: "verified"
+    if_fails: "Contract violation — term 'disk usage of' kind not in {noun, measure, action, unit, entity}"
+
+# NOT APPLICABLE, declared because `pv validate` requires the block. A vocabulary
+# term contract states a property of YAML bytes on disk; Kani symbolically executes
+# Rust and cannot reach a file system. Declaring a harness that does not exist is the
+# practice KANIDEBT-1 was filed against, so it is marked rather than pretended.
+kani_harnesses:
+  - id: KANI-RHL-FLEET-DISK-USAGE-OF-V2-001
+    obligation: PO-RHL-FLEET-DISK-USAGE-OF-V2-001
+    property: "NOT APPLICABLE — a vocabulary term contract is a property of YAML bytes on disk, outside Kani's reach"
+    bound: 1
+    strategy: bounded_int
+    harness: none
+    status: declared_not_implemented
+    discharged_by: "test_rhl16_v2_every_term_has_an_existing_contract"
+
+qa_gate:
+  id: QA-RHL-FLEET-DISK-USAGE-OF-V2
+  name: "rhl fleet vocabulary v2 term: disk usage of"
+  min_coverage: 1.0
+  max_complexity: 10
+  required_tests:
+    - test_rhl16_v2_every_term_has_an_existing_contract
+    - test_rhl16_v2_carries_every_v1_term_forward
+    - test_rhl16_v2_lowers_to_and_sigma_entity_stay_unbound

contracts/rhl-fleet-gb-v2.yaml

@@ -0,0 +1,63 @@
+metadata:
+  version: "2.0.0"
+  author: "RHL-16"
+  description: "RHL-16 v2 contract for vocabulary term 'GB' (fleet v2, kind: unit)"
+  crate: "ruchy"
+  references:
+    - "RHL-001 §3.4"
+
+equations:
+  gb_shape:
+    formula: "kind('GB') = unit ∧ gives('GB') = Size"
+    domain: "t ∈ vocabulary fleet v2 terms named 'GB'"
+    invariants:
+      - "term kind is one of {noun, measure, action, unit, entity} (RHL-001 §3.4)"
+      - "term result type ('gives') is Size"
+      - "lowers_to stays the unbound marker `[U]` until RHL-4 — RHL-16 does not bind lowering"
+
+proof_obligations:
+  - type: invariant
+    property: "Term 'GB' carries a contract template on disk (F6)"
+    formal: "contract('GB') exists"
+    applies_to: all
+  - type: invariant
+    property: "Term 'GB' kind is drawn from RHL's closed kind list"
+    formal: "kind('GB') ∈ {noun, measure, action, unit, entity}"
+    applies_to: all
+
+falsification_tests:
+  - id: FALSIFY-RHL-FLEET-GB-V2-001
+    rule: "Vocabulary term contract must exist (RHL-001 F6)"
+    test: "test_rhl16_v2_every_term_has_an_existing_contract"
+    prediction: "verified"
+    if_fails: "Contract violation — RHL-001 F6: term 'GB' has no contract template"
+
+  - id: FALSIFY-RHL-FLEET-GB-V2-002
+    rule: "Vocabulary term kind is drawn from the closed list"
+    test: "test_rhl16_v2_carries_every_v1_term_forward"
+    prediction: "verified"
+    if_fails: "Contract violation — term 'GB' kind not in {noun, measure, action, unit, entity}"
+
+# NOT APPLICABLE, declared because `pv validate` requires the block. A vocabulary
+# term contract states a property of YAML bytes on disk; Kani symbolically executes
+# Rust and cannot reach a file system. Declaring a harness that does not exist is the
+# practice KANIDEBT-1 was filed against, so it is marked rather than pretended.
+kani_harnesses:
+  - id: KANI-RHL-FLEET-GB-V2-001
+    obligation: PO-RHL-FLEET-GB-V2-001
+    property: "NOT APPLICABLE — a vocabulary term contract is a property of YAML bytes on disk, outside Kani's reach"
+    bound: 1
+    strategy: bounded_int
+    harness: none
+    status: declared_not_implemented
+    discharged_by: "test_rhl16_v2_every_term_has_an_existing_contract"
+
+qa_gate:
+  id: QA-RHL-FLEET-GB-V2
+  name: "rhl fleet vocabulary v2 term: GB"
+  min_coverage: 1.0
+  max_complexity: 10
+  required_tests:
+    - test_rhl16_v2_every_term_has_an_existing_contract
+    - test_rhl16_v2_carries_every_v1_term_forward
+    - test_rhl16_v2_lowers_to_and_sigma_entity_stay_unbound

contracts/rhl-fleet-host-v2.yaml

@@ -0,0 +1,64 @@
+metadata:
+  version: "2.0.0"
+  author: "RHL-16"
+  description: "RHL-16 v2 contract for vocabulary term 'host' (fleet v2, kind: entity)"
+  crate: "ruchy"
+  references:
+    - "RHL-001 §3.4"
+
+equations:
+  host_closed_world:
+    formula: "instances('host') = { x : x ∈ glob('machines/*/forjar.yaml') }"
+    domain: "t ∈ vocabulary fleet v2 terms named 'host'"
+    invariants:
+      - "term kind is entity (RHL-001 §3.4)"
+      - "every instance of 'host' comes from the declared closed-world source 'machines/*/forjar.yaml'"
+      - "an undeclared instance is a compile error naming the nearest candidate (RHL-001 §3.4)"
+      - "lowers_to stays the unbound marker `[U]` until RHL-4 — RHL-16 does not bind lowering"
+
+proof_obligations:
+  - type: invariant
+    property: "Term 'host' carries a contract template on disk (F6)"
+    formal: "contract('host') exists"
+    applies_to: all
+  - type: completeness
+    property: "Every instance of entity term 'host' is enumerable from its closed-world source"
+    formal: "∀x. valid('host', x) ⟺ x ∈ glob('machines/*/forjar.yaml')"
+    applies_to: all
+
+falsification_tests:
+  - id: FALSIFY-RHL-FLEET-HOST-V2-001
+    rule: "Vocabulary term contract must exist (RHL-001 F6)"
+    test: "test_rhl16_v2_every_term_has_an_existing_contract"
+    prediction: "verified"
+    if_fails: "Contract violation — RHL-001 F6: term 'host' has no contract template"
+
+  - id: FALSIFY-RHL-FLEET-HOST-V2-002
+    rule: "Entity term declares its closed-world instances_from source"
+    test: "test_rhl16_v2_carries_every_v1_term_forward"
+    prediction: "verified"
+    if_fails: "Contract violation — entity term 'host' has no instances_from source"
+
+# NOT APPLICABLE, declared because `pv validate` requires the block. A vocabulary
+# term contract states a property of YAML bytes on disk; Kani symbolically executes
+# Rust and cannot reach a file system. Declaring a harness that does not exist is the
+# practice KANIDEBT-1 was filed against, so it is marked rather than pretended.
+kani_harnesses:
+  - id: KANI-RHL-FLEET-HOST-V2-001
+    obligation: PO-RHL-FLEET-HOST-V2-001
+    property: "NOT APPLICABLE — a vocabulary term contract is a property of YAML bytes on disk, outside Kani's reach"
+    bound: 1
+    strategy: bounded_int
+    harness: none
+    status: declared_not_implemented
+    discharged_by: "test_rhl16_v2_every_term_has_an_existing_contract"
+
+qa_gate:
+  id: QA-RHL-FLEET-HOST-V2
+  name: "rhl fleet vocabulary v2 term: host"
+  min_coverage: 1.0
+  max_complexity: 10
+  required_tests:
+    - test_rhl16_v2_every_term_has_an_existing_contract
+    - test_rhl16_v2_carries_every_v1_term_forward
+    - test_rhl16_v2_lowers_to_and_sigma_entity_stay_unbound

contracts/rhl-fleet-hour-v2.yaml

@@ -0,0 +1,63 @@
+metadata:
+  version: "2.0.0"
+  author: "RHL-16"
+  description: "RHL-16 v2 contract for vocabulary term 'hour' (fleet v2, kind: unit)"
+  crate: "ruchy"
+  references:
+    - "RHL-001 §3.4"
+
+equations:
+  hour_shape:
+    formula: "kind('hour') = unit ∧ gives('hour') = Duration"
+    domain: "t ∈ vocabulary fleet v2 terms named 'hour'"
+    invariants:
+      - "term kind is one of {noun, measure, action, unit, entity} (RHL-001 §3.4)"
+      - "term result type ('gives') is Duration"
+      - "lowers_to stays the unbound marker `[U]` until RHL-4 — RHL-16 does not bind lowering"
+
+proof_obligations:
+  - type: invariant
+    property: "Term 'hour' carries a contract template on disk (F6)"
+    formal: "contract('hour') exists"
+    applies_to: all
+  - type: invariant
+    property: "Term 'hour' kind is drawn from RHL's closed kind list"
+    formal: "kind('hour') ∈ {noun, measure, action, unit, entity}"
+    applies_to: all
+
+falsification_tests:
+  - id: FALSIFY-RHL-FLEET-HOUR-V2-001
+    rule: "Vocabulary term contract must exist (RHL-001 F6)"
+    test: "test_rhl16_v2_every_term_has_an_existing_contract"
+    prediction: "verified"
+    if_fails: "Contract violation — RHL-001 F6: term 'hour' has no contract template"
+
+  - id: FALSIFY-RHL-FLEET-HOUR-V2-002
+    rule: "Vocabulary term kind is drawn from the closed list"
+    test: "test_rhl16_v2_carries_every_v1_term_forward"
+    prediction: "verified"
+    if_fails: "Contract violation — term 'hour' kind not in {noun, measure, action, unit, entity}"
+
+# NOT APPLICABLE, declared because `pv validate` requires the block. A vocabulary
+# term contract states a property of YAML bytes on disk; Kani symbolically executes
+# Rust and cannot reach a file system. Declaring a harness that does not exist is the
+# practice KANIDEBT-1 was filed against, so it is marked rather than pretended.
+kani_harnesses:
+  - id: KANI-RHL-FLEET-HOUR-V2-001
+    obligation: PO-RHL-FLEET-HOUR-V2-001
+    property: "NOT APPLICABLE — a vocabulary term contract is a property of YAML bytes on disk, outside Kani's reach"
+    bound: 1
+    strategy: bounded_int
+    harness: none
+    status: declared_not_implemented
+    discharged_by: "test_rhl16_v2_every_term_has_an_existing_contract"
+
+qa_gate:
+  id: QA-RHL-FLEET-HOUR-V2
+  name: "rhl fleet vocabulary v2 term: hour"
+  min_coverage: 1.0
+  max_complexity: 10
+  required_tests:
+    - test_rhl16_v2_every_term_has_an_existing_contract
+    - test_rhl16_v2_carries_every_v1_term_forward
+    - test_rhl16_v2_lowers_to_and_sigma_entity_stay_unbound