diff --git a/docs/api/_items/ommx.OneHotPromotionWitness.rst b/docs/api/_items/ommx.OneHotPromotionWitness.rst new file mode 100644 index 000000000..69d74983c --- /dev/null +++ b/docs/api/_items/ommx.OneHotPromotionWitness.rst @@ -0,0 +1,4 @@ +OneHotPromotionWitness +====================== + +.. pyo3-api-class:: ommx OneHotPromotionWitness diff --git a/docs/api/_items/ommx.PromotionAudit.rst b/docs/api/_items/ommx.PromotionAudit.rst new file mode 100644 index 000000000..306dc6a28 --- /dev/null +++ b/docs/api/_items/ommx.PromotionAudit.rst @@ -0,0 +1,4 @@ +PromotionAudit +============== + +.. pyo3-api-class:: ommx PromotionAudit diff --git a/docs/api/_items/ommx.PromotionPreview.rst b/docs/api/_items/ommx.PromotionPreview.rst new file mode 100644 index 000000000..634c4b897 --- /dev/null +++ b/docs/api/_items/ommx.PromotionPreview.rst @@ -0,0 +1,4 @@ +PromotionPreview +================ + +.. pyo3-api-class:: ommx PromotionPreview diff --git a/docs/api/_items/ommx.PromotionReport.rst b/docs/api/_items/ommx.PromotionReport.rst new file mode 100644 index 000000000..6ed39c7d5 --- /dev/null +++ b/docs/api/_items/ommx.PromotionReport.rst @@ -0,0 +1,4 @@ +PromotionReport +=============== + +.. pyo3-api-class:: ommx PromotionReport diff --git a/docs/api/_items/ommx.PromotionResult.rst b/docs/api/_items/ommx.PromotionResult.rst new file mode 100644 index 000000000..2e50146ad --- /dev/null +++ b/docs/api/_items/ommx.PromotionResult.rst @@ -0,0 +1,4 @@ +PromotionResult +=============== + +.. pyo3-api-class:: ommx PromotionResult diff --git a/docs/api/api_reference.json b/docs/api/api_reference.json index a7055a4c3..96730fa57 100644 --- a/docs/api/api_reference.json +++ b/docs/api/api_reference.json @@ -8471,6 +8471,47 @@ "is_async": false, "deprecated": null }, + { + "name": "check_promotion_witness", + "doc": "Check a detector-supplied one-hot promotion witness without mutation.\n\n``allowed`` is the caller's capability boundary and must contain\n:attr:`AdditionalCapability.OneHot`. The returned preview is\ninformational only; promotion methods re-validate the witness\nagainst the then-current instance.", + "signatures": [ + { + "parameters": [ + { + "name": "witness", + "type_": { + "display": "OneHotPromotionWitness", + "link_target": null, + "children": [] + }, + "default": null + }, + { + "name": "allowed", + "type_": { + "display": "set[AdditionalCapability]", + "link_target": null, + "children": [ + { + "display": "AdditionalCapability", + "link_target": null, + "children": [] + } + ] + }, + "default": null + } + ], + "return_type": { + "display": "PromotionPreview", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + }, { "name": "constraint_context_df", "doc": "Constraint context DataFrame (id-indexed wide format).\n\nOne row per constraint id (active + removed) with columns\n`name`, `subscripts`, `description`. Index column is\n`{kind}_constraint_id`. `kind` selects which constraint family\nto read: `\"regular\"`, `\"indicator\"`, `\"one_hot\"`, or `\"sos1\"`.", @@ -10108,6 +10149,94 @@ "is_async": false, "deprecated": null }, + { + "name": "promote_with_witness", + "doc": "Verify and atomically promote one regular constraint to one-hot form.\n\nThe source regular constraint is retained in ``removed_constraints``\nwith reserved ``promotion.*`` audit metadata, and its full context is\ncopied to the new active one-hot constraint. On error the instance is\nunchanged.", + "signatures": [ + { + "parameters": [ + { + "name": "witness", + "type_": { + "display": "OneHotPromotionWitness", + "link_target": null, + "children": [] + }, + "default": null + }, + { + "name": "allowed", + "type_": { + "display": "set[AdditionalCapability]", + "link_target": null, + "children": [ + { + "display": "AdditionalCapability", + "link_target": null, + "children": [] + } + ] + }, + "default": null + } + ], + "return_type": { + "display": "PromotionResult", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + }, + { + "name": "promote_with_witnesses", + "doc": "Verify and atomically apply multiple one-hot promotion witnesses.\n\nEvery witness is checked against one pre-promotion snapshot.\nExplicit target IDs are reserved before omitted IDs are allocated. Any\ninvalid or conflicting witness leaves the instance unchanged.", + "signatures": [ + { + "parameters": [ + { + "name": "witnesses", + "type_": { + "display": "Sequence[OneHotPromotionWitness]", + "link_target": null, + "children": [ + { + "display": "OneHotPromotionWitness", + "link_target": null, + "children": [] + } + ] + }, + "default": null + }, + { + "name": "allowed", + "type_": { + "display": "set[AdditionalCapability]", + "link_target": null, + "children": [ + { + "display": "AdditionalCapability", + "link_target": null, + "children": [] + } + ] + }, + "default": null + } + ], + "return_type": { + "display": "PromotionReport", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + }, { "name": "random_samples", "doc": "Generate random samples for this instance.\n\nThe generated samples will contain ``num_samples`` sample entries divided into\n``num_different_samples`` groups, where each group shares the same state but has\ndifferent sample IDs.\n\n**Args:**\n- `rng`: Random number generator\n- `num_different_samples`: Number of different states to generate\n- `num_samples`: Total number of samples to generate\n- `max_sample_id`: Maximum sample ID (default: ``num_samples``)\n\n**Returns:**\nSamples object\n\n# Examples\n\nGenerate samples for a simple instance:\n\n```python\n>>> from ommx import Instance, DecisionVariable, Rng\n>>> x = [DecisionVariable.binary(i) for i in range(3)]\n>>> instance = Instance.from_components(\n... decision_variables=x,\n... objective=sum(x),\n... constraints=[(sum(x) <= 2).set_id(0)],\n... sense=Instance.MAXIMIZE,\n... )\n\n>>> rng = Rng()\n>>> samples = instance.random_samples(rng, num_different_samples=2, num_samples=5)\n>>> samples.num_samples()\n5\n```", @@ -10879,6 +11008,32 @@ ], "is_async": false, "deprecated": null + }, + { + "name": "verify_promotion_history", + "doc": "Re-validate a retained one-hot promotion audit trail.\n\nThe removed regular source, reserved metadata, and active or removed\none-hot target are checked again without trusting the original detector.", + "signatures": [ + { + "parameters": [ + { + "name": "source_constraint_id", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "PromotionAudit", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null } ], "attributes": [ @@ -13730,123 +13885,87 @@ }, { "kind": "Class", - "name": "Optimality", - "doc": "Optimality status of a solution", - "bases": [], - "methods": [], - "attributes": [ - { - "name": "NotOptimal", - "doc": "The solver has determined that the solution is not optimal", - "type_": null - }, - { - "name": "Optimal", - "doc": "The solver has determined that the solution is optimal", - "type_": null - }, - { - "name": "Unspecified", - "doc": "The solver cannot determine whether the solution is optimal", - "type_": null - } - ], - "deprecated": null - }, - { - "kind": "Class", - "name": "Parameter", - "doc": "Parameter in an optimization problem.\n\nParameters are values that are fixed during optimization but may vary between different\nruns or scenarios. They share the same ID space with decision variables.\n\nNote that this object overloads `==` for creating a constraint, not for equality comparison.\n\n# Examples\n\n```python\n>>> p = Parameter(1, name=\"penalty\")\n>>> x = DecisionVariable.integer(2)\n>>> x + p # Returns Linear expression\nLinear(...)\n```", + "name": "OneHotPromotionWitness", + "doc": "Detector-supplied witness for promoting a regular constraint to one-hot form.\n\nConstruction validates only the witness's Python shape. Full semantic\nvalidation is performed by :meth:`Instance.check_promotion_witness` or\none of the promotion mutation methods against the current instance.", "bases": [], "methods": [ { - "name": "__add__", + "name": "__eq__", "doc": "", "signatures": [ { "parameters": [ { - "name": "rhs", + "name": "other", "type_": { - "display": "ScalarLike | LinearLike | Parameter", + "display": "object", "link_target": null, - "children": [ - { - "display": "ScalarLike", - "link_target": null, - "children": [] - }, - { - "display": "LinearLike", - "link_target": null, - "children": [] - }, - { - "display": "Parameter", - "link_target": null, - "children": [] - } - ] + "children": [] }, "default": null } ], "return_type": { - "display": "Linear", + "display": "bool", "link_target": null, "children": [] } - }, + } + ], + "is_async": false, + "deprecated": null + }, + { + "name": "__new__", + "doc": "Create a one-hot promotion witness.\n\n**Args:**\n\n- `source_constraint_id`: Active regular constraint claimed to be one-hot.\n- `variables`: Claimed one-hot decision-variable IDs. Duplicates are rejected.\n- `target_one_hot_constraint_id`: Optional requested target ID. Omit to allocate one.", + "signatures": [ { "parameters": [ { - "name": "rhs", + "name": "source_constraint_id", "type_": { - "display": "Quadratic", + "display": "int", "link_target": null, "children": [] }, "default": null - } - ], - "return_type": { - "display": "Quadratic", - "link_target": null, - "children": [] - } - }, - { - "parameters": [ + }, { - "name": "rhs", + "name": "variables", "type_": { - "display": "Polynomial", + "display": "Sequence[int]", "link_target": null, - "children": [] + "children": [ + { + "display": "int", + "link_target": null, + "children": [] + } + ] }, "default": null - } - ], - "return_type": { - "display": "Polynomial", - "link_target": null, - "children": [] - } - }, - { - "parameters": [ + }, { - "name": "rhs", + "name": "target_one_hot_constraint_id", "type_": { - "display": "Function", + "display": "Optional[int]", "link_target": null, - "children": [] + "children": [ + { + "display": "int", + "link_target": null, + "children": [] + } + ] }, - "default": null + "default": { + "kind": "Simple", + "value": "None" + } } ], "return_type": { - "display": "Function", + "display": "OneHotPromotionWitness", "link_target": null, "children": [] } @@ -13856,13 +13975,13 @@ "deprecated": null }, { - "name": "__copy__", + "name": "__repr__", "doc": "", "signatures": [ { "parameters": [], "return_type": { - "display": "Parameter", + "display": "str", "link_target": null, "children": [] } @@ -13870,7 +13989,200 @@ ], "is_async": false, "deprecated": null - }, + } + ], + "attributes": [ + { + "name": "source_constraint_id", + "doc": "Active regular constraint claimed to be one-hot.", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "target_one_hot_constraint_id", + "doc": "Requested target ID, or `None` when OMMX should allocate one.", + "type_": { + "display": "Optional[int]", + "link_target": null, + "children": [ + { + "display": "int", + "link_target": null, + "children": [] + } + ] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "variables", + "doc": "Claimed one-hot variable IDs in sorted order.", + "type_": { + "display": "list[int]", + "link_target": null, + "children": [ + { + "display": "int", + "link_target": null, + "children": [] + } + ] + }, + "is_property": true, + "is_readonly": true + } + ], + "deprecated": null + }, + { + "kind": "Class", + "name": "Optimality", + "doc": "Optimality status of a solution", + "bases": [], + "methods": [], + "attributes": [ + { + "name": "NotOptimal", + "doc": "The solver has determined that the solution is not optimal", + "type_": null + }, + { + "name": "Optimal", + "doc": "The solver has determined that the solution is optimal", + "type_": null + }, + { + "name": "Unspecified", + "doc": "The solver cannot determine whether the solution is optimal", + "type_": null + } + ], + "deprecated": null + }, + { + "kind": "Class", + "name": "Parameter", + "doc": "Parameter in an optimization problem.\n\nParameters are values that are fixed during optimization but may vary between different\nruns or scenarios. They share the same ID space with decision variables.\n\nNote that this object overloads `==` for creating a constraint, not for equality comparison.\n\n# Examples\n\n```python\n>>> p = Parameter(1, name=\"penalty\")\n>>> x = DecisionVariable.integer(2)\n>>> x + p # Returns Linear expression\nLinear(...)\n```", + "bases": [], + "methods": [ + { + "name": "__add__", + "doc": "", + "signatures": [ + { + "parameters": [ + { + "name": "rhs", + "type_": { + "display": "ScalarLike | LinearLike | Parameter", + "link_target": null, + "children": [ + { + "display": "ScalarLike", + "link_target": null, + "children": [] + }, + { + "display": "LinearLike", + "link_target": null, + "children": [] + }, + { + "display": "Parameter", + "link_target": null, + "children": [] + } + ] + }, + "default": null + } + ], + "return_type": { + "display": "Linear", + "link_target": null, + "children": [] + } + }, + { + "parameters": [ + { + "name": "rhs", + "type_": { + "display": "Quadratic", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "Quadratic", + "link_target": null, + "children": [] + } + }, + { + "parameters": [ + { + "name": "rhs", + "type_": { + "display": "Polynomial", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "Polynomial", + "link_target": null, + "children": [] + } + }, + { + "parameters": [ + { + "name": "rhs", + "type_": { + "display": "Function", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "Function", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + }, + { + "name": "__copy__", + "doc": "", + "signatures": [ + { + "parameters": [], + "return_type": { + "display": "Parameter", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + }, { "name": "__deepcopy__", "doc": "", @@ -17752,6 +18064,287 @@ "attributes": [], "deprecated": null }, + { + "kind": "Class", + "name": "PromotionAudit", + "doc": "Re-validated audit record for a previous one-hot promotion.", + "bases": [], + "methods": [ + { + "name": "__eq__", + "doc": "", + "signatures": [ + { + "parameters": [ + { + "name": "other", + "type_": { + "display": "object", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "bool", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + } + ], + "attributes": [ + { + "name": "source_constraint_id", + "doc": "", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "target_is_active", + "doc": "Whether the target one-hot constraint is active rather than removed.", + "type_": { + "display": "bool", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "target_one_hot_constraint_id", + "doc": "", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "variables", + "doc": "Original one-hot members reconstructed from the retained regular source.", + "type_": { + "display": "list[int]", + "link_target": null, + "children": [ + { + "display": "int", + "link_target": null, + "children": [] + } + ] + }, + "is_property": true, + "is_readonly": true + } + ], + "deprecated": null + }, + { + "kind": "Class", + "name": "PromotionPreview", + "doc": "Informational result of checking a promotion witness.\n\nThis object is not an applicable mutation plan. Promotion methods always\nre-validate the original witness against the current instance.", + "bases": [], + "methods": [ + { + "name": "__eq__", + "doc": "", + "signatures": [ + { + "parameters": [ + { + "name": "other", + "type_": { + "display": "object", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "bool", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + } + ], + "attributes": [ + { + "name": "source_constraint_id", + "doc": "", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "target_one_hot_constraint_id", + "doc": "", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "variables", + "doc": "", + "type_": { + "display": "list[int]", + "link_target": null, + "children": [ + { + "display": "int", + "link_target": null, + "children": [] + } + ] + }, + "is_property": true, + "is_readonly": true + } + ], + "deprecated": null + }, + { + "kind": "Class", + "name": "PromotionReport", + "doc": "Result of an all-or-nothing bulk promotion.", + "bases": [], + "methods": [ + { + "name": "__eq__", + "doc": "", + "signatures": [ + { + "parameters": [ + { + "name": "other", + "type_": { + "display": "object", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "bool", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + } + ], + "attributes": [ + { + "name": "source_to_target", + "doc": "Mapping from promoted regular constraint IDs to one-hot target IDs.", + "type_": { + "display": "dict[int, int]", + "link_target": null, + "children": [ + { + "display": "int", + "link_target": null, + "children": [] + }, + { + "display": "int", + "link_target": null, + "children": [] + } + ] + }, + "is_property": true, + "is_readonly": true + } + ], + "deprecated": null + }, + { + "kind": "Class", + "name": "PromotionResult", + "doc": "Result of one successfully applied promotion.", + "bases": [], + "methods": [ + { + "name": "__eq__", + "doc": "", + "signatures": [ + { + "parameters": [ + { + "name": "other", + "type_": { + "display": "object", + "link_target": null, + "children": [] + }, + "default": null + } + ], + "return_type": { + "display": "bool", + "link_target": null, + "children": [] + } + } + ], + "is_async": false, + "deprecated": null + } + ], + "attributes": [ + { + "name": "source_constraint_id", + "doc": "", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + }, + { + "name": "target_one_hot_constraint_id", + "doc": "", + "type_": { + "display": "int", + "link_target": null, + "children": [] + }, + "is_property": true, + "is_readonly": true + } + ], + "deprecated": null + }, { "kind": "Class", "name": "Provenance", @@ -30034,10 +30627,15 @@ "ommx.Linear": "ommx", "ommx.NamedFunction": "ommx", "ommx.OneHotConstraint": "ommx", + "ommx.OneHotPromotionWitness": "ommx", "ommx.Optimality": "ommx", "ommx.Parameter": "ommx", "ommx.ParametricInstance": "ommx", "ommx.Polynomial": "ommx", + "ommx.PromotionAudit": "ommx", + "ommx.PromotionPreview": "ommx", + "ommx.PromotionReport": "ommx", + "ommx.PromotionResult": "ommx", "ommx.Provenance": "ommx", "ommx.ProvenanceKind": "ommx", "ommx.Quadratic": "ommx", diff --git a/docs/api/ommx.rst b/docs/api/ommx.rst index 73b501394..86795d85a 100644 --- a/docs/api/ommx.rst +++ b/docs/api/ommx.rst @@ -23,6 +23,11 @@ ommx _items/ommx.AttachedDecisionVariable _items/ommx.Parameter _items/ommx.AdditionalCapability + _items/ommx.OneHotPromotionWitness + _items/ommx.PromotionPreview + _items/ommx.PromotionResult + _items/ommx.PromotionReport + _items/ommx.PromotionAudit _items/ommx.Constraint _items/ommx.AttachedConstraint _items/ommx.IndicatorConstraint diff --git a/docs/en/release_note/ommx-3.0.md b/docs/en/release_note/ommx-3.0.md index da9a8ceb4..f332cdd51 100644 --- a/docs/en/release_note/ommx-3.0.md +++ b/docs/en/release_note/ommx-3.0.md @@ -8,6 +8,39 @@ Python SDK 3.0.0 contains breaking API changes. A migration guide is available i Changes merged after the most recent release will be appended here as they land, and promoted to a new version section when the next release is cut. +### 🆕 Verified one-hot promotion ([#1050](https://github.com/Jij-Inc/ommx/pull/1050)) + +{class}`~ommx.OneHotPromotionWitness` and the new +{class}`~ommx.Instance` promotion methods let presolvers and other detectors +promote an active regular equality such as `x1 + x2 + x3 = 1` to a first-class +one-hot constraint. OMMX rechecks the witness exactly against the current +instance: every member must be a binary decision variable, the complete +function must be linear, and the coefficients and constant must form an exact +nonzero scalar multiple of `sum(x) - 1`. Approximate and nonlinear matches are +rejected. + +```python +from ommx import AdditionalCapability, OneHotPromotionWitness + +witness = OneHotPromotionWitness( + source_constraint_id=10, + variables=[1, 2, 3], +) +result = instance.promote_with_witness( + witness, + allowed={AdditionalCapability.OneHot}, +) +``` + +Use {meth}`~ommx.Instance.check_promotion_witness` for a non-mutating +preview and {meth}`~ommx.Instance.promote_with_witnesses` for all-or-nothing +bulk promotion. The original regular constraint is retained as removed with +reserved `promotion.*` metadata, while +{meth}`~ommx.Instance.verify_promotion_history` re-validates the retained +source and active or removed target. Restoring the source is rejected while +that target remains in either lifecycle state, including after +{meth}`~ommx.Instance.reduce_capabilities` lowers the one-hot constraint again. + ### ⚠ Dedicated Experiment artifact type ([#1033](https://github.com/Jij-Inc/ommx/pull/1033)) Committed Experiment artifacts now write `application/org.ommx.v1.experiment` diff --git a/docs/ja/release_note/ommx-3.0.md b/docs/ja/release_note/ommx-3.0.md index 205a22b47..340d46717 100644 --- a/docs/ja/release_note/ommx-3.0.md +++ b/docs/ja/release_note/ommx-3.0.md @@ -8,6 +8,39 @@ Python SDK 3.0.0にはAPIの破壊的な変更が含まれます。マイグレ 直近のリリース以降にマージされた変更を、このセクションに順次追記していきます。次のリリース時に新しいバージョンのセクションへ昇格します。 +### 🆕 検証付き one-hot promotion ([#1050](https://github.com/Jij-Inc/ommx/pull/1050)) + +{class}`~ommx.OneHotPromotionWitness` と新しい +{class}`~ommx.Instance` の promotion method により、presolver などの detector +が `x1 + x2 + x3 = 1` のような active regular equality を first-class one-hot +constraint へ昇格できるようになりました。OMMX は witness を現在の instance +に対して厳密に再検証します。すべての変数が binary decision variable であり、 +function 全体が linear で、係数と定数項が `sum(x) - 1` の厳密な非ゼロ scalar +multiple になっている必要があります。近似的な一致や nonlinear な式は拒否します。 + +```python +from ommx import AdditionalCapability, OneHotPromotionWitness + +witness = OneHotPromotionWitness( + source_constraint_id=10, + variables=[1, 2, 3], +) +result = instance.promote_with_witness( + witness, + allowed={AdditionalCapability.OneHot}, +) +``` + +非変更の preview には {meth}`~ommx.Instance.check_promotion_witness`、 +all-or-nothing の一括昇格には +{meth}`~ommx.Instance.promote_with_witnesses` を使います。元の regular +constraint は reserved `promotion.*` metadata とともに removed constraint +として保持され、{meth}`~ommx.Instance.verify_promotion_history` は保持された +source と active または removed の target を再検証します。 +{meth}`~ommx.Instance.reduce_capabilities` で one-hot を再び regular constraint +へ lowering した後も含め、target がいずれかの lifecycle state に残る間は元の +source の restore を拒否します。 + ### ⚠ Experiment 専用 artifact type ([#1033](https://github.com/Jij-Inc/ommx/pull/1033)) commit 済み Experiment Artifact は、OCI Manifest の `artifactType` として diff --git a/python/ommx-tests/tests/test_promotion.py b/python/ommx-tests/tests/test_promotion.py new file mode 100644 index 000000000..2d07bbd4a --- /dev/null +++ b/python/ommx-tests/tests/test_promotion.py @@ -0,0 +1,155 @@ +from __future__ import annotations + +import pytest +from ommx import ( + AdditionalCapability, + DecisionVariable, + Instance, + OneHotConstraint, + OneHotPromotionWitness, + PromotionAudit, + PromotionPreview, + PromotionReport, + PromotionResult, +) + + +def _instance_with_one_source() -> Instance: + x = [DecisionVariable.binary(i) for i in range(3)] + source = (2 * x[0] + 2 * x[1] + 2 * x[2] == 2).set_name("choose") + return Instance.from_components( + decision_variables=x, + objective=sum(x), + constraints={10: source}, + sense=Instance.MINIMIZE, + ) + + +def _witness( + source_constraint_id: int = 10, + variables: list[int] | None = None, + target_one_hot_constraint_id: int | None = None, +) -> OneHotPromotionWitness: + return OneHotPromotionWitness( + source_constraint_id=source_constraint_id, + variables=[0, 1, 2] if variables is None else variables, + target_one_hot_constraint_id=target_one_hot_constraint_id, + ) + + +def test_witness_shape_and_dry_run() -> None: + with pytest.raises(ValueError, match="must be unique"): + _witness(variables=[0, 0, 1]) + + assert repr(_witness(target_one_hot_constraint_id=7)) == ( + "OneHotPromotionWitness(source_constraint_id=10, variables=[0, 1, 2], " + "target_one_hot_constraint_id=7)" + ) + assert repr(_witness()).endswith("target_one_hot_constraint_id=None)") + + empty = _witness(variables=[]) + instance = _instance_with_one_source() + with pytest.raises(RuntimeError, match="must not be empty"): + instance.check_promotion_witness(empty, allowed={AdditionalCapability.OneHot}) + + witness = _witness() + before = instance.to_v2_bytes() + preview = instance.check_promotion_witness( + witness, allowed={AdditionalCapability.OneHot} + ) + assert isinstance(preview, PromotionPreview) + assert preview.source_constraint_id == 10 + assert preview.variables == [0, 1, 2] + assert preview.target_one_hot_constraint_id == 0 + assert instance.to_v2_bytes() == before + + with pytest.raises(RuntimeError, match="allowed capabilities"): + instance.check_promotion_witness(witness, allowed=set()) + + +def test_single_promotion_and_audit_round_trip() -> None: + instance = _instance_with_one_source() + result = instance.promote_with_witness( + _witness(), allowed={AdditionalCapability.OneHot} + ) + + assert isinstance(result, PromotionResult) + assert result.source_constraint_id == 10 + assert result.target_one_hot_constraint_id == 0 + assert instance.required_capabilities == {AdditionalCapability.OneHot} + assert list(instance.constraints) == [] + assert instance.one_hot_constraints[0].variables == [0, 1, 2] + assert instance.one_hot_constraints[0].name == "choose" + + removed = instance.removed_constraints[10] + assert removed.removed_reason == "ommx.Instance.promote_constraint_to_one_hot" + assert removed.removed_reason_parameters == { + "promotion.kind": "one_hot", + "promotion.target_id": "0", + "promotion.witness_version": "1", + } + + audit = instance.verify_promotion_history(10) + assert isinstance(audit, PromotionAudit) + assert audit.source_constraint_id == 10 + assert audit.variables == [0, 1, 2] + assert audit.target_one_hot_constraint_id == 0 + assert audit.target_is_active is True + + round_trip = Instance.from_v2_bytes(instance.to_v2_bytes()) + assert round_trip.verify_promotion_history(10) == audit + + +def test_bulk_reserves_explicit_targets_and_is_atomic() -> None: + x = [DecisionVariable.binary(i) for i in range(4)] + instance = Instance.from_components( + decision_variables=x, + objective=sum(x), + constraints={ + 10: x[0] + x[1] == 1, + 11: -2 * x[2] - 2 * x[3] == -2, + }, + one_hot_constraints={5: OneHotConstraint(variables=[0])}, + sense=Instance.MINIMIZE, + ) + report = instance.promote_with_witnesses( + [ + _witness(10, [0, 1]), + _witness(11, [2, 3], target_one_hot_constraint_id=10), + ], + allowed={AdditionalCapability.OneHot}, + ) + assert isinstance(report, PromotionReport) + assert report.source_to_target == {10: 11, 11: 10} + + invalid = Instance.from_components( + decision_variables=x, + objective=sum(x), + constraints={ + 20: x[0] + x[1] == 1, + 21: x[2] + x[3] <= 1, + }, + sense=Instance.MINIMIZE, + ) + before = invalid.to_v2_bytes() + with pytest.raises(RuntimeError, match="not an equality"): + invalid.promote_with_witnesses( + [_witness(20, [0, 1]), _witness(21, [2, 3])], + allowed={AdditionalCapability.OneHot}, + ) + assert invalid.to_v2_bytes() == before + + +def test_lowering_blocks_restore_of_promoted_source() -> None: + instance = _instance_with_one_source() + instance.promote_with_witness(_witness(), allowed={AdditionalCapability.OneHot}) + assert instance.reduce_capabilities(set()) == {AdditionalCapability.OneHot} + assert instance.required_capabilities == set() + assert 0 in instance.removed_one_hot_constraints + + audit = instance.verify_promotion_history(10) + assert audit.target_is_active is False + before = instance.to_v2_bytes() + with pytest.raises(RuntimeError, match="Cannot restore promoted"): + instance.restore_constraint(10) + assert instance.to_v2_bytes() == before diff --git a/python/ommx/ommx/__init__.py b/python/ommx/ommx/__init__.py index b89903296..383e2384c 100644 --- a/python/ommx/ommx/__init__.py +++ b/python/ommx/ommx/__init__.py @@ -23,10 +23,15 @@ Linear, NamedFunction, OneHotConstraint, + OneHotPromotionWitness, Optimality, Parameter, ParametricInstance, Polynomial, + PromotionAudit, + PromotionPreview, + PromotionReport, + PromotionResult, Provenance, ProvenanceKind, Quadratic, @@ -73,10 +78,15 @@ "Linear", "NamedFunction", "OneHotConstraint", + "OneHotPromotionWitness", "Optimality", "Parameter", "ParametricInstance", "Polynomial", + "PromotionAudit", + "PromotionPreview", + "PromotionReport", + "PromotionResult", "Provenance", "ProvenanceKind", "Quadratic", diff --git a/python/ommx/ommx/_ommx_rust/__init__.pyi b/python/ommx/ommx/_ommx_rust/__init__.pyi index 894ce6b65..ead2fb57f 100644 --- a/python/ommx/ommx/_ommx_rust/__init__.pyi +++ b/python/ommx/ommx/_ommx_rust/__init__.pyi @@ -54,12 +54,17 @@ __all__ = [ "LinearLike", "NamedFunction", "OneHotConstraint", + "OneHotPromotionWitness", "OpenSolve", "Optimality", "Parameter", "Parameters", "ParametricInstance", "Polynomial", + "PromotionAudit", + "PromotionPreview", + "PromotionReport", + "PromotionResult", "Provenance", "ProvenanceKind", "PruneAnonymousReport", @@ -2875,6 +2880,53 @@ class Instance: Raises if any underlying Big-M conversion fails (e.g. a SOS1 variable with a non-finite bound). """ + def check_promotion_witness( + self, + witness: OneHotPromotionWitness, + allowed: builtins.set[AdditionalCapability], + ) -> PromotionPreview: + r""" + Check a detector-supplied one-hot promotion witness without mutation. + + ``allowed`` is the caller's capability boundary and must contain + :attr:`AdditionalCapability.OneHot`. The returned preview is + informational only; promotion methods re-validate the witness + against the then-current instance. + """ + def promote_with_witness( + self, + witness: OneHotPromotionWitness, + allowed: builtins.set[AdditionalCapability], + ) -> PromotionResult: + r""" + Verify and atomically promote one regular constraint to one-hot form. + + The source regular constraint is retained in ``removed_constraints`` + with reserved ``promotion.*`` audit metadata, and its full context is + copied to the new active one-hot constraint. On error the instance is + unchanged. + """ + def promote_with_witnesses( + self, + witnesses: typing.Sequence[OneHotPromotionWitness], + allowed: builtins.set[AdditionalCapability], + ) -> PromotionReport: + r""" + Verify and atomically apply multiple one-hot promotion witnesses. + + Every witness is checked against one pre-promotion snapshot. + Explicit target IDs are reserved before omitted IDs are allocated. Any + invalid or conflicting witness leaves the instance unchanged. + """ + def verify_promotion_history( + self, source_constraint_id: builtins.int + ) -> PromotionAudit: + r""" + Re-validate a retained one-hot promotion audit trail. + + The removed regular source, reserved metadata, and active or removed + one-hot target are checked again without trusting the original detector. + """ def to_v1_bytes(self) -> bytes: ... def to_v2_bytes(self) -> bytes: ... def __str__(self) -> builtins.str: ... @@ -4622,6 +4674,49 @@ class OneHotConstraint: def __copy__(self) -> OneHotConstraint: ... def __deepcopy__(self, _memo: typing.Any) -> OneHotConstraint: ... +@typing.final +class OneHotPromotionWitness: + r""" + Detector-supplied witness for promoting a regular constraint to one-hot form. + + Construction validates only the witness's Python shape. Full semantic + validation is performed by :meth:`Instance.check_promotion_witness` or + one of the promotion mutation methods against the current instance. + """ + @property + def source_constraint_id(self) -> builtins.int: + r""" + Active regular constraint claimed to be one-hot. + """ + @property + def variables(self) -> builtins.list[builtins.int]: + r""" + Claimed one-hot variable IDs in sorted order. + """ + @property + def target_one_hot_constraint_id(self) -> typing.Optional[builtins.int]: + r""" + Requested target ID, or `None` when OMMX should allocate one. + """ + def __eq__(self, other: builtins.object, /) -> builtins.bool: ... + def __new__( + cls, + *, + source_constraint_id: builtins.int, + variables: typing.Sequence[builtins.int], + target_one_hot_constraint_id: typing.Optional[builtins.int] = None, + ) -> OneHotPromotionWitness: + r""" + Create a one-hot promotion witness. + + **Args:** + + - `source_constraint_id`: Active regular constraint claimed to be one-hot. + - `variables`: Claimed one-hot decision-variable IDs. Duplicates are rejected. + - `target_one_hot_constraint_id`: Optional requested target ID. Omit to allocate one. + """ + def __repr__(self) -> builtins.str: ... + @typing.final class OpenSolve: r""" @@ -5314,6 +5409,66 @@ class Polynomial: Create a greater-than-or-equal constraint: self >= other → Constraint """ +@typing.final +class PromotionAudit: + r""" + Re-validated audit record for a previous one-hot promotion. + """ + @property + def source_constraint_id(self) -> builtins.int: ... + @property + def variables(self) -> builtins.list[builtins.int]: + r""" + Original one-hot members reconstructed from the retained regular source. + """ + @property + def target_one_hot_constraint_id(self) -> builtins.int: ... + @property + def target_is_active(self) -> builtins.bool: + r""" + Whether the target one-hot constraint is active rather than removed. + """ + def __eq__(self, other: builtins.object, /) -> builtins.bool: ... + +@typing.final +class PromotionPreview: + r""" + Informational result of checking a promotion witness. + + This object is not an applicable mutation plan. Promotion methods always + re-validate the original witness against the current instance. + """ + @property + def source_constraint_id(self) -> builtins.int: ... + @property + def variables(self) -> builtins.list[builtins.int]: ... + @property + def target_one_hot_constraint_id(self) -> builtins.int: ... + def __eq__(self, other: builtins.object, /) -> builtins.bool: ... + +@typing.final +class PromotionReport: + r""" + Result of an all-or-nothing bulk promotion. + """ + @property + def source_to_target(self) -> builtins.dict[builtins.int, builtins.int]: + r""" + Mapping from promoted regular constraint IDs to one-hot target IDs. + """ + def __eq__(self, other: builtins.object, /) -> builtins.bool: ... + +@typing.final +class PromotionResult: + r""" + Result of one successfully applied promotion. + """ + @property + def source_constraint_id(self) -> builtins.int: ... + @property + def target_one_hot_constraint_id(self) -> builtins.int: ... + def __eq__(self, other: builtins.object, /) -> builtins.bool: ... + @typing.final class Provenance: r""" diff --git a/python/ommx/src/instance.rs b/python/ommx/src/instance.rs index f0d739179..484cf927e 100644 --- a/python/ommx/src/instance.rs +++ b/python/ommx/src/instance.rs @@ -660,6 +660,77 @@ impl Instance { Ok(converted.into_iter().map(|c| c.into()).collect()) } + /// Check a detector-supplied one-hot promotion witness without mutation. + /// + /// ``allowed`` is the caller's capability boundary and must contain + /// :attr:`AdditionalCapability.OneHot`. The returned preview is + /// informational only; promotion methods re-validate the witness + /// against the then-current instance. + pub fn check_promotion_witness( + &self, + witness: crate::OneHotPromotionWitness, + allowed: std::collections::HashSet, + ) -> anyhow::Result { + let allowed: ommx::Capabilities = allowed.into_iter().map(Into::into).collect(); + Ok(self + .inner + .check_promotion_witness(&ommx::PromotionWitness::OneHot(witness.0), &allowed)? + .into()) + } + + /// Verify and atomically promote one regular constraint to one-hot form. + /// + /// The source regular constraint is retained in ``removed_constraints`` + /// with reserved ``promotion.*`` audit metadata, and its full context is + /// copied to the new active one-hot constraint. On error the instance is + /// unchanged. + pub fn promote_with_witness( + &mut self, + witness: crate::OneHotPromotionWitness, + allowed: std::collections::HashSet, + ) -> anyhow::Result { + let allowed: ommx::Capabilities = allowed.into_iter().map(Into::into).collect(); + Ok(self + .inner + .promote_with_witness(ommx::PromotionWitness::OneHot(witness.0), &allowed)? + .into()) + } + + /// Verify and atomically apply multiple one-hot promotion witnesses. + /// + /// Every witness is checked against one pre-promotion snapshot. + /// Explicit target IDs are reserved before omitted IDs are allocated. Any + /// invalid or conflicting witness leaves the instance unchanged. + pub fn promote_with_witnesses( + &mut self, + witnesses: Vec, + allowed: std::collections::HashSet, + ) -> anyhow::Result { + let allowed: ommx::Capabilities = allowed.into_iter().map(Into::into).collect(); + let witnesses = witnesses + .into_iter() + .map(|witness| ommx::PromotionWitness::OneHot(witness.0)) + .collect(); + Ok(self + .inner + .promote_with_witnesses(witnesses, &allowed)? + .into()) + } + + /// Re-validate a retained one-hot promotion audit trail. + /// + /// The removed regular source, reserved metadata, and active or removed + /// one-hot target are checked again without trusting the original detector. + pub fn verify_promotion_history( + &self, + source_constraint_id: u64, + ) -> anyhow::Result { + Ok(self + .inner + .verify_promotion_history(ommx::ConstraintID::from(source_constraint_id))? + .into()) + } + /// Dict of all removed constraints in the instance keyed by their IDs. #[getter] pub fn removed_constraints(&self) -> BTreeMap { diff --git a/python/ommx/src/lib.rs b/python/ommx/src/lib.rs index 6296dba14..02049b1e2 100644 --- a/python/ommx/src/lib.rs +++ b/python/ommx/src/lib.rs @@ -27,6 +27,7 @@ mod parameter; mod parameters; mod parametric_instance; mod polynomial; +mod promotion; mod provenance; mod quadratic; mod random; @@ -65,6 +66,7 @@ pub use parameter::*; pub use parameters::*; pub use parametric_instance::*; pub use polynomial::*; +pub use promotion::*; pub use provenance::*; pub use quadratic::*; pub use random::*; @@ -181,6 +183,11 @@ fn _ommx_rust(_py: Python, m: &Bound) -> PyResult<()> { m.add_class::()?; m.add_class::()?; m.add_class::()?; + m.add_class::()?; + m.add_class::()?; + m.add_class::()?; + m.add_class::()?; + m.add_class::()?; m.add_class::()?; m.add_class::()?; m.add_class::()?; @@ -262,6 +269,12 @@ pyo3_stub_gen::reexport_module_members!("ommx" from "ommx._ommx_rust"; "Parameter", // Constraint capability "AdditionalCapability", + // Verified constraint promotion + "OneHotPromotionWitness", + "PromotionPreview", + "PromotionResult", + "PromotionReport", + "PromotionAudit", // Constraint and named function "Constraint", "AttachedConstraint", diff --git a/python/ommx/src/promotion.rs b/python/ommx/src/promotion.rs new file mode 100644 index 000000000..9df3dbbd9 --- /dev/null +++ b/python/ommx/src/promotion.rs @@ -0,0 +1,234 @@ +use pyo3::{exceptions::PyValueError, prelude::*}; +use pyo3_stub_gen::derive::{gen_stub_pyclass, gen_stub_pymethods}; +use std::collections::{BTreeMap, BTreeSet}; + +/// Detector-supplied witness for promoting a regular constraint to one-hot form. +/// +/// Construction validates only the witness's Python shape. Full semantic +/// validation is performed by :meth:`Instance.check_promotion_witness` or +/// one of the promotion mutation methods against the current instance. +#[gen_stub_pyclass] +#[pyclass(eq, frozen)] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct OneHotPromotionWitness(pub(crate) ommx::OneHotPromotionWitness); + +#[gen_stub_pymethods] +#[pymethods] +impl OneHotPromotionWitness { + /// Create a one-hot promotion witness. + /// + /// **Args:** + /// + /// - `source_constraint_id`: Active regular constraint claimed to be one-hot. + /// - `variables`: Claimed one-hot decision-variable IDs. Duplicates are rejected. + /// - `target_one_hot_constraint_id`: Optional requested target ID. Omit to allocate one. + #[new] + #[pyo3(signature = (*, source_constraint_id, variables, target_one_hot_constraint_id=None))] + pub fn new( + source_constraint_id: u64, + variables: Vec, + target_one_hot_constraint_id: Option, + ) -> PyResult { + let variable_count = variables.len(); + let variables: BTreeSet = + variables.into_iter().map(ommx::VariableID::from).collect(); + if variables.len() != variable_count { + return Err(PyValueError::new_err( + "One-hot promotion witness variables must be unique", + )); + } + Ok(Self(ommx::OneHotPromotionWitness { + source_constraint_id: ommx::ConstraintID::from(source_constraint_id), + variables, + target_one_hot_constraint_id: target_one_hot_constraint_id + .map(ommx::OneHotConstraintID::from), + })) + } + + /// Active regular constraint claimed to be one-hot. + #[getter] + pub fn source_constraint_id(&self) -> u64 { + self.0.source_constraint_id.into_inner() + } + + /// Claimed one-hot variable IDs in sorted order. + #[getter] + pub fn variables(&self) -> Vec { + self.0.variables.iter().map(|id| id.into_inner()).collect() + } + + /// Requested target ID, or `None` when OMMX should allocate one. + #[getter] + pub fn target_one_hot_constraint_id(&self) -> Option { + self.0 + .target_one_hot_constraint_id + .map(ommx::OneHotConstraintID::into_inner) + } + + fn __repr__(&self) -> String { + let target = self + .target_one_hot_constraint_id() + .map_or_else(|| "None".to_string(), |id| id.to_string()); + format!( + "OneHotPromotionWitness(source_constraint_id={}, variables={:?}, target_one_hot_constraint_id={target})", + self.source_constraint_id(), + self.variables(), + ) + } +} + +/// Informational result of checking a promotion witness. +/// +/// This object is not an applicable mutation plan. Promotion methods always +/// re-validate the original witness against the current instance. +#[gen_stub_pyclass] +#[pyclass(eq, frozen)] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct PromotionPreview { + source_constraint_id: u64, + variables: Vec, + target_one_hot_constraint_id: u64, +} + +impl From for PromotionPreview { + fn from(preview: ommx::PromotionPreview) -> Self { + Self { + source_constraint_id: preview.source_constraint_id().into_inner(), + variables: preview + .variables() + .iter() + .map(|id| id.into_inner()) + .collect(), + target_one_hot_constraint_id: preview.target_one_hot_constraint_id().into_inner(), + } + } +} + +#[gen_stub_pymethods] +#[pymethods] +impl PromotionPreview { + #[getter] + pub fn source_constraint_id(&self) -> u64 { + self.source_constraint_id + } + + #[getter] + pub fn variables(&self) -> Vec { + self.variables.clone() + } + + #[getter] + pub fn target_one_hot_constraint_id(&self) -> u64 { + self.target_one_hot_constraint_id + } +} + +/// Result of one successfully applied promotion. +#[gen_stub_pyclass] +#[pyclass(eq, frozen)] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct PromotionResult { + source_constraint_id: u64, + target_one_hot_constraint_id: u64, +} + +impl From for PromotionResult { + fn from(result: ommx::PromotionResult) -> Self { + Self { + source_constraint_id: result.source_constraint_id().into_inner(), + target_one_hot_constraint_id: result.target_one_hot_constraint_id().into_inner(), + } + } +} + +#[gen_stub_pymethods] +#[pymethods] +impl PromotionResult { + #[getter] + pub fn source_constraint_id(&self) -> u64 { + self.source_constraint_id + } + + #[getter] + pub fn target_one_hot_constraint_id(&self) -> u64 { + self.target_one_hot_constraint_id + } +} + +/// Result of an all-or-nothing bulk promotion. +#[gen_stub_pyclass] +#[pyclass(eq, frozen)] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct PromotionReport { + source_to_target: BTreeMap, +} + +impl From for PromotionReport { + fn from(report: ommx::PromotionReport) -> Self { + Self { + source_to_target: report + .source_to_target() + .iter() + .map(|(source, target)| (source.into_inner(), target.into_inner())) + .collect(), + } + } +} + +#[gen_stub_pymethods] +#[pymethods] +impl PromotionReport { + /// Mapping from promoted regular constraint IDs to one-hot target IDs. + #[getter] + pub fn source_to_target(&self) -> BTreeMap { + self.source_to_target.clone() + } +} + +/// Re-validated audit record for a previous one-hot promotion. +#[gen_stub_pyclass] +#[pyclass(eq, frozen)] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct PromotionAudit { + source_constraint_id: u64, + variables: Vec, + target_one_hot_constraint_id: u64, + target_is_active: bool, +} + +impl From for PromotionAudit { + fn from(audit: ommx::PromotionAudit) -> Self { + Self { + source_constraint_id: audit.source_constraint_id().into_inner(), + variables: audit.variables().iter().map(|id| id.into_inner()).collect(), + target_one_hot_constraint_id: audit.target_one_hot_constraint_id().into_inner(), + target_is_active: audit.target_is_active(), + } + } +} + +#[gen_stub_pymethods] +#[pymethods] +impl PromotionAudit { + #[getter] + pub fn source_constraint_id(&self) -> u64 { + self.source_constraint_id + } + + /// Original one-hot members reconstructed from the retained regular source. + #[getter] + pub fn variables(&self) -> Vec { + self.variables.clone() + } + + #[getter] + pub fn target_one_hot_constraint_id(&self) -> u64 { + self.target_one_hot_constraint_id + } + + /// Whether the target one-hot constraint is active rather than removed. + #[getter] + pub fn target_is_active(&self) -> bool { + self.target_is_active + } +} diff --git a/rust/ommx/doc/release_note/3.0.md b/rust/ommx/doc/release_note/3.0.md index 783dbe3f2..63a10eccb 100644 --- a/rust/ommx/doc/release_note/3.0.md +++ b/rust/ommx/doc/release_note/3.0.md @@ -573,6 +573,28 @@ Append user-visible updates within the 3.0 release line here. Each entry should describe only what changed since the previous 3.0.x release; broader redesigns should start a new minor-line page such as `3.1.md`. +### Verified one-hot promotion ([#1050](https://github.com/Jij-Inc/ommx/pull/1050)) + +The Rust SDK now exposes [`PromotionWitness`](crate::PromotionWitness) +and [`OneHotPromotionWitness`](crate::OneHotPromotionWitness) for +detector-supplied witnesses, together with dry-run, single, and atomic bulk +promotion methods on [`Instance`](crate::Instance). OMMX verifies the complete +source function through [`Function::as_linear`](crate::Function::as_linear), +requires an exact nonzero scalar multiple of `sum(x) - 1` over binary decision +variables, and rejects witnesses outside the caller-provided +[`Capabilities`](crate::Capabilities). + +Successful promotion copies the regular constraint context to the new active +one-hot constraint and retains the source as a removed regular constraint with +reserved `promotion.*` audit metadata. The returned +[`PromotionReport`](crate::PromotionReport) records every source-to-target ID +mapping, and +[`Instance::verify_promotion_history`](crate::Instance::verify_promotion_history) +re-validates the retained source against an active or removed target. +[`Instance::restore_constraint`](crate::Instance::restore_constraint) rejects a +promoted source while that target remains, including after capability reduction +has lowered the one-hot constraint back to a distinct regular constraint. + ### Consuming partial evaluation for `Instance` ([#1034](https://github.com/Jij-Inc/ommx/pull/1034)) [`Instance::into_partial_evaluated`](crate::Instance::into_partial_evaluated) diff --git a/rust/ommx/src/instance.rs b/rust/ommx/src/instance.rs index f46ba4d5f..c71842897 100644 --- a/rust/ommx/src/instance.rs +++ b/rust/ommx/src/instance.rs @@ -18,6 +18,7 @@ mod parametric_builder; mod parse; mod pass; mod penalty; +mod promotion; mod qubo; mod reduce_binary_power; mod serialize; @@ -32,6 +33,10 @@ pub use analysis::*; pub use arbitrary::{InstanceParameters, InstanceSpace}; pub use builder::*; pub use parametric_builder::*; +pub use promotion::{ + OneHotPromotionWitness, PromotionAudit, PromotionPreview, PromotionReport, PromotionResult, + PromotionWitness, +}; pub use stats::*; use crate::{ @@ -49,6 +54,56 @@ use crate::{ }; use std::collections::{BTreeMap, HashMap}; +const ONE_HOT_PROMOTION_REASON: &str = "ommx.Instance.promote_constraint_to_one_hot"; +const PROMOTION_KIND_PARAMETER: &str = "promotion.kind"; +const PROMOTION_TARGET_ID_PARAMETER: &str = "promotion.target_id"; +const PROMOTION_WITNESS_VERSION_PARAMETER: &str = "promotion.witness_version"; +const ONE_HOT_PROMOTION_KIND: &str = "one_hot"; +const PROMOTION_WITNESS_VERSION: &str = "1"; + +fn promoted_one_hot_target( + removed_reason: &RemovedReason, +) -> crate::Result> { + if removed_reason.reason != ONE_HOT_PROMOTION_REASON { + return Ok(None); + } + + let kind = removed_reason + .parameters + .get(PROMOTION_KIND_PARAMETER) + .ok_or_else(|| { + crate::error!("Promotion metadata is missing parameter {PROMOTION_KIND_PARAMETER:?}") + })?; + if kind != ONE_HOT_PROMOTION_KIND { + crate::bail!("Unsupported promotion kind {kind:?} in removed-constraint metadata"); + } + + let version = removed_reason + .parameters + .get(PROMOTION_WITNESS_VERSION_PARAMETER) + .ok_or_else(|| { + crate::error!( + "Promotion metadata is missing parameter {PROMOTION_WITNESS_VERSION_PARAMETER:?}" + ) + })?; + if version != PROMOTION_WITNESS_VERSION { + crate::bail!("Unsupported promotion witness version {version:?}"); + } + + let raw_target_id = removed_reason + .parameters + .get(PROMOTION_TARGET_ID_PARAMETER) + .ok_or_else(|| { + crate::error!( + "Promotion metadata is missing parameter {PROMOTION_TARGET_ID_PARAMETER:?}" + ) + })?; + let target_id = raw_target_id.parse::().map_err(|error| { + crate::error!("Invalid one-hot promotion target ID {raw_target_id:?}: {error}") + })?; + Ok(Some(crate::OneHotConstraintID::from(target_id))) +} + /// A constraint type capability flag for non-standard constraint types. /// /// Standard constraints (`f(x) = 0` or `f(x) <= 0`) are always supported by all adapters @@ -126,8 +181,8 @@ pub enum Sense { /// - expression-algebra actions such as substitution, partial evaluation, and /// binary-power reduction; /// - variable-space extensions such as slack-variable introduction; -/// - constraint-family morphisms such as one-hot, indicator, and SOS1 -/// conversion into regular constraints; +/// - constraint-family morphisms such as verified regular-to-one-hot promotion +/// and one-hot, indicator, or SOS1 conversion into regular constraints; /// - lifecycle actions such as relax and restore; /// - unit propagation as a rewrite system over constraints plus assignment /// state; @@ -200,11 +255,11 @@ pub enum Sense { /// [`Self::add_constraint`] / [`Self::add_indicator_constraint`] / /// [`Self::add_one_hot_constraint`] / [`Self::add_sos1_constraint`], and the /// internal `relax_constraint` / `relax_indicator_constraint` / -/// `convert_all_one_hots_to_constraints` / `convert_all_sos1_to_constraints` -/// paths that populate the removed maps. Constraint-family storage is mutated -/// through operation-level collection primitives so active/removed -/// disjointness, removed reasons, and context sidecars remain attached to -/// owned row IDs. +/// `promote_with_witness` / `convert_all_one_hots_to_constraints` / +/// `convert_all_sos1_to_constraints` paths that populate the removed maps. +/// Constraint-family storage is mutated through operation-level collection +/// primitives so active/removed disjointness, removed reasons, and context +/// sidecars remain attached to owned row IDs. /// #[derive( Debug, diff --git a/rust/ommx/src/instance/pass.rs b/rust/ommx/src/instance/pass.rs index 752912bd6..9927682d3 100644 --- a/rust/ommx/src/instance/pass.rs +++ b/rust/ommx/src/instance/pass.rs @@ -21,6 +21,7 @@ impl Instance { } pub fn restore_constraint(&mut self, id: ConstraintID) -> Result<()> { + super::promotion::ensure_promoted_constraint_can_be_restored(self, id)?; let fixed_state = self.fixed_state(); let dependency = self.decision_variable_dependency.clone(); let mut constraint = self diff --git a/rust/ommx/src/instance/promotion.rs b/rust/ommx/src/instance/promotion.rs new file mode 100644 index 000000000..7510af6b6 --- /dev/null +++ b/rust/ommx/src/instance/promotion.rs @@ -0,0 +1,1070 @@ +use super::*; +use crate::{ + constraint::Equality, decision_variable::Kind, Coefficient, LinearMonomial, OneHotConstraintID, +}; +use std::collections::{BTreeMap, BTreeSet}; + +/// A detector-supplied witness for promoting a regular constraint. +/// +/// Witnesses are never trusted as mutation plans. [`Instance`] recomputes +/// the represented mathematical condition against its current state whenever +/// a witness is checked or applied. +#[non_exhaustive] +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum PromotionWitness { + /// Promote an exact linear equality over binary variables to one-hot form. + OneHot(OneHotPromotionWitness), +} + +// Data-carrying enums are not supported by the derive. Delegate to the +// witness payload so its variable-set allocation remains visible. +impl crate::logical_memory::LogicalMemoryProfile for PromotionWitness { + fn visit_logical_memory( + &self, + path: &mut crate::logical_memory::Path, + visitor: &mut V, + ) { + match self { + Self::OneHot(witness) => { + crate::logical_memory::LogicalMemoryProfile::visit_logical_memory( + witness, + path.with("PromotionWitness.OneHot").as_mut(), + visitor, + ); + } + } + } +} + +impl From for PromotionWitness { + fn from(witness: OneHotPromotionWitness) -> Self { + Self::OneHot(witness) + } +} + +/// A witness that an active regular constraint is exactly a one-hot constraint. +/// +/// The fields are intentionally only claims. In particular, callers may +/// construct an empty variable set, refer to non-binary variables, or choose a +/// used target ID. [`Instance::check_promotion_witness`] and the mutation +/// methods validate every invariant against the current instance. +#[derive(Debug, Clone, PartialEq, Eq, crate::logical_memory::LogicalMemoryProfile)] +pub struct OneHotPromotionWitness { + /// Active regular constraint to replace with a one-hot constraint. + pub source_constraint_id: ConstraintID, + /// Claimed one-hot members. The set representation makes membership unique. + pub variables: BTreeSet, + /// Requested one-hot ID, or [`None`] to allocate one during verification. + pub target_one_hot_constraint_id: Option, +} + +/// Informational result of checking one promotion witness. +/// +/// A preview cannot be applied. The instance may change after it is returned, +/// so all mutation entry points verify the original witness again. +#[derive(Debug, Clone, PartialEq, Eq, crate::logical_memory::LogicalMemoryProfile)] +pub struct PromotionPreview { + source_constraint_id: ConstraintID, + variables: BTreeSet, + target_one_hot_constraint_id: OneHotConstraintID, +} + +impl PromotionPreview { + /// The active regular constraint that would be promoted. + pub fn source_constraint_id(&self) -> ConstraintID { + self.source_constraint_id + } + + /// The exactly verified one-hot members. + pub fn variables(&self) -> &BTreeSet { + &self.variables + } + + /// The requested or provisionally allocated target one-hot ID. + pub fn target_one_hot_constraint_id(&self) -> OneHotConstraintID { + self.target_one_hot_constraint_id + } +} + +/// Result of one successfully applied promotion. +#[derive(Debug, Clone, PartialEq, Eq, crate::logical_memory::LogicalMemoryProfile)] +pub struct PromotionResult { + source_constraint_id: ConstraintID, + target_one_hot_constraint_id: OneHotConstraintID, +} + +impl PromotionResult { + /// The regular constraint moved into `removed_constraints`. + pub fn source_constraint_id(&self) -> ConstraintID { + self.source_constraint_id + } + + /// The newly active one-hot constraint. + pub fn target_one_hot_constraint_id(&self) -> OneHotConstraintID { + self.target_one_hot_constraint_id + } +} + +/// Result of an all-or-nothing bulk promotion. +#[derive(Debug, Clone, PartialEq, Eq, Default, crate::logical_memory::LogicalMemoryProfile)] +pub struct PromotionReport { + source_to_target: BTreeMap, +} + +impl PromotionReport { + /// Mapping from every promoted regular constraint to its one-hot target. + pub fn source_to_target(&self) -> &BTreeMap { + &self.source_to_target + } +} + +/// Re-validated audit record for a previous one-hot promotion. +#[derive(Debug, Clone, PartialEq, Eq, crate::logical_memory::LogicalMemoryProfile)] +pub struct PromotionAudit { + source_constraint_id: ConstraintID, + variables: BTreeSet, + target_one_hot_constraint_id: OneHotConstraintID, + target_is_active: bool, +} + +impl PromotionAudit { + /// The removed regular source constraint. + pub fn source_constraint_id(&self) -> ConstraintID { + self.source_constraint_id + } + + /// The original one-hot members reconstructed from the retained source. + pub fn variables(&self) -> &BTreeSet { + &self.variables + } + + /// The target one-hot ID recorded in the source's removal metadata. + pub fn target_one_hot_constraint_id(&self) -> OneHotConstraintID { + self.target_one_hot_constraint_id + } + + /// Whether the target one-hot constraint is active rather than removed. + pub fn target_is_active(&self) -> bool { + self.target_is_active + } +} + +#[derive(Debug, Clone)] +struct PlannedOneHotPromotion { + source_constraint_id: ConstraintID, + variables: BTreeSet, + target_one_hot_constraint_id: OneHotConstraintID, +} + +impl PlannedOneHotPromotion { + fn preview(&self) -> PromotionPreview { + PromotionPreview { + source_constraint_id: self.source_constraint_id, + variables: self.variables.clone(), + target_one_hot_constraint_id: self.target_one_hot_constraint_id, + } + } + + fn result(&self) -> PromotionResult { + PromotionResult { + source_constraint_id: self.source_constraint_id, + target_one_hot_constraint_id: self.target_one_hot_constraint_id, + } + } +} + +impl Instance { + /// Check a detector-supplied witness without mutating this instance. + /// + /// `allowed` is the caller's capability boundary. A one-hot witness is + /// rejected unless it contains [`AdditionalCapability::OneHot`]. Any target + /// ID in the returned preview is informational only; applying the + /// witness later repeats validation and allocation against the then + /// current instance. + pub fn check_promotion_witness( + &self, + witness: &PromotionWitness, + allowed: &Capabilities, + ) -> crate::Result { + let plans = self.plan_promotions(std::slice::from_ref(witness), allowed)?; + Ok(plans + .first() + .expect("a one-element witness slice produces one plan") + .preview()) + } + + /// Verify and atomically apply one promotion witness. + /// + /// Verification is repeated against the current instance. On error, the + /// instance remains unchanged. + pub fn promote_with_witness( + &mut self, + witness: PromotionWitness, + allowed: &Capabilities, + ) -> crate::Result { + let plans = self.plan_promotions(std::slice::from_ref(&witness), allowed)?; + let result = plans + .first() + .expect("a one-element witness slice produces one plan") + .result(); + self.apply_promotion_plans(&plans)?; + Ok(result) + } + + /// Verify and atomically apply multiple promotion witnesses. + /// + /// All witnesses are checked against one pre-promotion snapshot. + /// Duplicate sources and targets are rejected. Explicit target IDs are + /// reserved before omitted IDs are allocated, and any failure leaves this + /// instance unchanged. + pub fn promote_with_witnesses( + &mut self, + witnesses: Vec, + allowed: &Capabilities, + ) -> crate::Result { + let plans = self.plan_promotions(&witnesses, allowed)?; + let source_to_target = plans + .iter() + .map(|plan| (plan.source_constraint_id, plan.target_one_hot_constraint_id)) + .collect(); + self.apply_promotion_plans(&plans)?; + Ok(PromotionReport { source_to_target }) + } + + /// Re-validate the retained audit trail for a previous one-hot promotion. + /// + /// This method trusts neither the original detector nor its witness. It + /// reads the reserved `promotion.*` removal metadata, finds the target + /// one-hot constraint in either lifecycle state, and checks exact + /// equivalence with the retained regular source row again. + pub fn verify_promotion_history( + &self, + source_constraint_id: ConstraintID, + ) -> crate::Result { + let (source, removed_reason) = self + .constraint_collection + .removed() + .get(&source_constraint_id) + .ok_or_else(|| { + crate::error!("Removed regular constraint {source_constraint_id:?} was not found") + })?; + let target_id = promoted_one_hot_target(removed_reason)?.ok_or_else(|| { + crate::error!( + "Removed regular constraint {source_constraint_id:?} is not a one-hot promotion" + ) + })?; + + let (target, target_is_active) = if let Some(target) = + self.one_hot_constraint_collection.active().get(&target_id) + { + (target, true) + } else if let Some((target, _reason)) = + self.one_hot_constraint_collection.removed().get(&target_id) + { + (target, false) + } else { + crate::bail!( + "One-hot promotion target {target_id:?} recorded by source {source_constraint_id:?} was not found" + ); + }; + + let original_variables = + self.verified_one_hot_source_variables(source_constraint_id, source)?; + self.validate_one_hot_variables(&target.variables)?; + if !target.variables.is_subset(&original_variables) { + crate::bail!( + "One-hot promotion target {target_id:?} contains variables outside the retained source support" + ); + } + + // Unit propagation may shrink an active target by removing members + // fixed exactly to zero. Reconstruct the target's lifecycle-normalized + // source without substituting variables that remain in the target; a + // consumed target can legitimately retain members now fixed to one or + // zero in its removed payload. + let removed_variables: BTreeSet<_> = original_variables + .difference(&target.variables) + .copied() + .collect(); + for variable_id in &removed_variables { + if self.fixed_decision_variable_value(*variable_id) != Some(0.0) { + crate::bail!( + "One-hot promotion target {target_id:?} omits source variable {variable_id:?} that is not fixed exactly to zero" + ); + } + } + let mut normalized_source = source.clone(); + if !removed_variables.is_empty() { + let state = crate::v1::State::from( + removed_variables + .iter() + .map(|id| (id.into_inner(), 0.0)) + .collect::>(), + ); + normalized_source.partial_evaluate(&state, crate::ATol::default())?; + } + self.verify_one_hot_equivalence( + source_constraint_id, + &normalized_source, + &target.variables, + )?; + Ok(PromotionAudit { + source_constraint_id, + variables: original_variables, + target_one_hot_constraint_id: target_id, + target_is_active, + }) + } + + fn plan_promotions( + &self, + witnesses: &[PromotionWitness], + allowed: &Capabilities, + ) -> crate::Result> { + let mut source_ids = BTreeSet::new(); + let mut target_ids: BTreeSet = self + .one_hot_constraint_collection + .active() + .keys() + .chain(self.one_hot_constraint_collection.removed().keys()) + .copied() + .collect(); + let existing_target_ids = target_ids.clone(); + + // Reserve every explicit target before allocating any omitted target. + for witness in witnesses { + match witness { + PromotionWitness::OneHot(witness) => { + if !allowed.contains(&AdditionalCapability::OneHot) { + crate::bail!( + "One-hot promotion is outside the caller's allowed capabilities" + ); + } + if !source_ids.insert(witness.source_constraint_id) { + crate::bail!( + "Duplicate promotion source constraint ID {:?}", + witness.source_constraint_id + ); + } + if let Some(target_id) = witness.target_one_hot_constraint_id { + if existing_target_ids.contains(&target_id) { + crate::bail!( + "One-hot promotion target ID {target_id:?} is already used" + ); + } + if !target_ids.insert(target_id) { + crate::bail!("Duplicate one-hot promotion target ID {target_id:?}"); + } + } + } + } + } + + let mut plans = Vec::with_capacity(witnesses.len()); + for witness in witnesses { + match witness { + PromotionWitness::OneHot(witness) => { + let target_id = match witness.target_one_hot_constraint_id { + Some(target_id) => target_id, + None => allocate_one_hot_target_id(&mut target_ids)?, + }; + let source = self + .constraint_collection + .active() + .get(&witness.source_constraint_id) + .ok_or_else(|| { + crate::error!( + "Active regular constraint {:?} was not found", + witness.source_constraint_id + ) + })?; + self.verify_one_hot_equivalence( + witness.source_constraint_id, + source, + &witness.variables, + )?; + plans.push(PlannedOneHotPromotion { + source_constraint_id: witness.source_constraint_id, + variables: witness.variables.clone(), + target_one_hot_constraint_id: target_id, + }); + } + } + } + Ok(plans) + } + + fn verify_one_hot_equivalence( + &self, + source_constraint_id: ConstraintID, + source: &Constraint, + variables: &BTreeSet, + ) -> crate::Result<()> { + self.validate_one_hot_variables(variables)?; + let support = self.verified_one_hot_source_variables(source_constraint_id, source)?; + if support != *variables { + crate::bail!( + "Regular constraint {source_constraint_id:?} has linear support {support:?}, expected {variables:?}" + ); + } + Ok(()) + } + + fn validate_one_hot_variables(&self, variables: &BTreeSet) -> crate::Result<()> { + if variables.is_empty() { + crate::bail!("One-hot promotion variables must not be empty"); + } + for variable_id in variables { + let variable = self.decision_variables.get(variable_id).ok_or_else(|| { + crate::error!( + "One-hot promotion variable {variable_id:?} is not a decision variable" + ) + })?; + if variable.kind() != Kind::Binary { + crate::bail!("One-hot promotion variable {variable_id:?} must be binary"); + } + } + Ok(()) + } + + fn verified_one_hot_source_variables( + &self, + source_constraint_id: ConstraintID, + source: &Constraint, + ) -> crate::Result> { + if source.equality != Equality::EqualToZero { + crate::bail!( + "Regular constraint {source_constraint_id:?} is not an equality-to-zero constraint" + ); + } + + let linear = source.function().as_linear().ok_or_else(|| { + crate::error!("Regular constraint {source_constraint_id:?} is not exactly linear") + })?; + let coefficients: BTreeMap = linear.linear_terms().collect(); + let support: BTreeSet = coefficients.keys().copied().collect(); + self.validate_one_hot_variables(&support)?; + + let common_coefficient = *coefficients + .values() + .next() + .expect("non-empty support has at least one coefficient"); + if coefficients + .values() + .any(|coefficient| *coefficient != common_coefficient) + { + crate::bail!( + "Regular constraint {source_constraint_id:?} does not use one common coefficient for all one-hot variables" + ); + } + + let constant = linear.get(&LinearMonomial::Constant); + if constant != Some(-common_coefficient) { + crate::bail!( + "Regular constraint {source_constraint_id:?} has constant coefficient {constant:?}, expected {:?}", + -common_coefficient + ); + } + Ok(support) + } + + fn apply_promotion_plans(&mut self, plans: &[PlannedOneHotPromotion]) -> crate::Result<()> { + let mut staged = self.clone(); + for plan in plans { + let context = staged + .constraint_collection + .context() + .collect_for(plan.source_constraint_id); + let target = OneHotConstraint::new(plan.variables.clone())?; + staged + .one_hot_constraint_collection + .insert_active_with_context(plan.target_one_hot_constraint_id, target, context)?; + + let mut parameters = fnv::FnvHashMap::default(); + parameters.insert( + PROMOTION_KIND_PARAMETER.to_string(), + ONE_HOT_PROMOTION_KIND.to_string(), + ); + parameters.insert( + PROMOTION_TARGET_ID_PARAMETER.to_string(), + plan.target_one_hot_constraint_id.into_inner().to_string(), + ); + parameters.insert( + PROMOTION_WITNESS_VERSION_PARAMETER.to_string(), + PROMOTION_WITNESS_VERSION.to_string(), + ); + staged.constraint_collection.relax( + plan.source_constraint_id, + RemovedReason { + reason: ONE_HOT_PROMOTION_REASON.to_string(), + parameters, + }, + )?; + } + *self = staged; + Ok(()) + } +} + +/// Reject restoring a promoted regular source while its one-hot target is +/// retained. This is public only inside the private `instance` module so the +/// sibling restore implementation can enforce the cross-family invariant. +pub fn ensure_promoted_constraint_can_be_restored( + instance: &Instance, + source_constraint_id: ConstraintID, +) -> crate::Result<()> { + let Some((_source, removed_reason)) = instance + .constraint_collection + .removed() + .get(&source_constraint_id) + else { + return Ok(()); + }; + let Some(target_id) = promoted_one_hot_target(removed_reason)? else { + return Ok(()); + }; + + if instance + .one_hot_constraint_collection + .active() + .contains_key(&target_id) + || instance + .one_hot_constraint_collection + .removed() + .contains_key(&target_id) + { + crate::bail!( + "Cannot restore promoted regular constraint {source_constraint_id:?} while one-hot target {target_id:?} exists" + ); + } + Ok(()) +} + +fn allocate_one_hot_target_id( + reserved: &mut BTreeSet, +) -> crate::Result { + let next = match reserved.last().copied() { + Some(max_id) => match max_id.into_inner().checked_add(1) { + Some(next) => next, + None => first_unused_one_hot_target_id(reserved)?, + }, + None => 0, + }; + let id = OneHotConstraintID::from(next); + let inserted = reserved.insert(id); + debug_assert!(inserted, "max + 1 must be an unused target ID"); + Ok(id) +} + +fn first_unused_one_hot_target_id(reserved: &BTreeSet) -> crate::Result { + let mut candidate = 0u64; + for id in reserved { + let value = id.into_inner(); + if value < candidate { + continue; + } + if value > candidate { + return Ok(candidate); + } + candidate = candidate.checked_add(1).ok_or_else(|| { + crate::error!("One-hot constraint ID space is exhausted during promotion") + })?; + } + Ok(candidate) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::{ + coeff, quadratic, DecisionVariable, Evaluate, Linear, ModelingLabel, Provenance, Sense, + }; + + fn variables(ids: impl IntoIterator) -> BTreeSet { + ids.into_iter().map(VariableID::from).collect() + } + + fn exact_one_hot_function(ids: &[u64], coefficient: f64) -> Function { + let coefficient = Coefficient::try_from(coefficient).unwrap(); + let terms = ids + .iter() + .copied() + .map(|id| (LinearMonomial::from(id), coefficient)) + .chain(std::iter::once((LinearMonomial::Constant, -coefficient))); + Function::Linear(Linear::try_from_terms(terms).unwrap()) + } + + fn linear_function(terms: &[(u64, f64)], constant: f64) -> Function { + let terms = terms + .iter() + .map(|(id, coefficient)| { + ( + LinearMonomial::from(*id), + Coefficient::try_from(*coefficient).unwrap(), + ) + }) + .chain(std::iter::once(( + LinearMonomial::Constant, + Coefficient::try_from(constant).unwrap(), + ))); + Function::Linear(Linear::try_from_terms(terms).unwrap()) + } + + fn witness( + source_constraint_id: u64, + variable_ids: impl IntoIterator, + target_one_hot_constraint_id: Option, + ) -> PromotionWitness { + OneHotPromotionWitness { + source_constraint_id: ConstraintID::from(source_constraint_id), + variables: variables(variable_ids), + target_one_hot_constraint_id: target_one_hot_constraint_id + .map(OneHotConstraintID::from), + } + .into() + } + + fn instance_with_constraints(constraints: BTreeMap) -> Instance { + let mut decision_variables = BTreeMap::new(); + for id in 1..=4 { + decision_variables.insert(VariableID::from(id), DecisionVariable::binary()); + } + decision_variables.insert(VariableID::from(5), DecisionVariable::integer()); + Instance::builder() + .sense(Sense::Minimize) + .objective(Function::Zero) + .decision_variables(decision_variables) + .constraints(constraints) + .build() + .unwrap() + } + + fn one_source_instance(coefficient: f64) -> Instance { + instance_with_constraints(BTreeMap::from([( + ConstraintID::from(10), + Constraint::equal_to_zero(exact_one_hot_function(&[1, 2, 3], coefficient)), + )])) + } + + fn allowed_one_hot() -> Capabilities { + Capabilities::from([AdditionalCapability::OneHot]) + } + + #[test] + fn checks_and_applies_exact_one_hot_with_audit_context_and_capability() { + let mut instance = one_source_instance(2.0); + instance + .set_constraint_context( + ConstraintID::from(10), + ConstraintContext { + label: ModelingLabel { + name: Some("choose".to_string()), + ..Default::default() + }, + provenance: vec![Provenance::Sos1Constraint(crate::Sos1ConstraintID::from( + 22, + ))], + }, + ) + .unwrap(); + let witness = witness(10, [1, 2, 3], None); + + let before = instance.clone(); + let preview = instance + .check_promotion_witness(&witness, &allowed_one_hot()) + .unwrap(); + assert_eq!(instance, before, "dry-run verification must not mutate"); + assert_eq!(preview.source_constraint_id(), ConstraintID::from(10)); + assert_eq!(preview.variables(), &variables([1, 2, 3])); + assert_eq!( + preview.target_one_hot_constraint_id(), + OneHotConstraintID::from(0) + ); + + let result = instance + .promote_with_witness(witness, &allowed_one_hot()) + .unwrap(); + assert_eq!(result.source_constraint_id(), ConstraintID::from(10)); + assert_eq!( + result.target_one_hot_constraint_id(), + OneHotConstraintID::from(0) + ); + assert!(instance.constraints().is_empty()); + assert_eq!( + instance + .one_hot_constraints() + .get(&OneHotConstraintID::from(0)) + .unwrap() + .variables, + variables([1, 2, 3]) + ); + assert_eq!( + instance + .one_hot_constraint_context() + .name(OneHotConstraintID::from(0)), + Some("choose") + ); + assert_eq!( + instance + .one_hot_constraint_context() + .provenance(OneHotConstraintID::from(0)), + &[Provenance::Sos1Constraint(crate::Sos1ConstraintID::from( + 22 + ))] + ); + assert_eq!(instance.required_capabilities(), allowed_one_hot()); + + let (_source, removed_reason) = instance + .removed_constraints() + .get(&ConstraintID::from(10)) + .unwrap(); + assert_eq!(removed_reason.reason, ONE_HOT_PROMOTION_REASON); + assert_eq!( + removed_reason.parameters.get(PROMOTION_KIND_PARAMETER), + Some(&ONE_HOT_PROMOTION_KIND.to_string()) + ); + assert_eq!( + removed_reason.parameters.get(PROMOTION_TARGET_ID_PARAMETER), + Some(&"0".to_string()) + ); + assert_eq!( + removed_reason + .parameters + .get(PROMOTION_WITNESS_VERSION_PARAMETER), + Some(&PROMOTION_WITNESS_VERSION.to_string()) + ); + + let audit = instance + .verify_promotion_history(ConstraintID::from(10)) + .unwrap(); + assert_eq!(audit.source_constraint_id(), ConstraintID::from(10)); + assert_eq!(audit.variables(), &variables([1, 2, 3])); + assert_eq!( + audit.target_one_hot_constraint_id(), + OneHotConstraintID::from(0) + ); + assert!(audit.target_is_active()); + } + + #[test] + fn accepts_positive_and_negative_exact_scalar_multiples() { + for coefficient in [1.0, 2.0, -1.0, -3.5] { + one_source_instance(coefficient) + .check_promotion_witness(&witness(10, [1, 2, 3], None), &allowed_one_hot()) + .unwrap(); + } + } + + #[test] + fn rejects_disallowed_nonbinary_and_non_exact_witnesses() { + let instance = one_source_instance(1.0); + let err = instance + .check_promotion_witness(&witness(10, [1, 2, 3], None), &Capabilities::new()) + .unwrap_err(); + assert!(err.to_string().contains("allowed capabilities")); + + for invalid in [ + witness(10, [], None), + witness(10, [1, 2, 5], None), + witness(10, [1, 2, 99], None), + witness(10, [1, 2], None), + witness(999, [1, 2, 3], None), + ] { + assert!(instance + .check_promotion_witness(&invalid, &allowed_one_hot()) + .is_err()); + } + + let inequality = instance_with_constraints(BTreeMap::from([( + ConstraintID::from(10), + Constraint::less_than_or_equal_to_zero(exact_one_hot_function(&[1, 2, 3], 1.0)), + )])); + assert!(inequality + .check_promotion_witness(&witness(10, [1, 2, 3], None), &allowed_one_hot(),) + .is_err()); + + let unequal = instance_with_constraints(BTreeMap::from([( + ConstraintID::from(10), + Constraint::equal_to_zero(linear_function(&[(1, 1.0), (2, 2.0)], -1.0)), + )])); + assert!(unequal + .check_promotion_witness(&witness(10, [1, 2], None), &allowed_one_hot(),) + .is_err()); + + let wrong_constant = instance_with_constraints(BTreeMap::from([( + ConstraintID::from(10), + Constraint::equal_to_zero(linear_function(&[(1, 1.0), (2, 1.0)], -2.0)), + )])); + assert!(wrong_constant + .check_promotion_witness(&witness(10, [1, 2], None), &allowed_one_hot(),) + .is_err()); + + let approximate = instance_with_constraints(BTreeMap::from([( + ConstraintID::from(10), + Constraint::equal_to_zero(linear_function(&[(1, 1.0), (2, 1.0 + f64::EPSILON)], -1.0)), + )])); + assert!(approximate + .check_promotion_witness(&witness(10, [1, 2], None), &allowed_one_hot(),) + .is_err()); + } + + #[test] + fn rejects_nonlinear_payload_with_valid_looking_linear_terms() { + let linear_part = ((quadratic!(1) + quadratic!(2)).unwrap() + coeff!(-1.0)).unwrap(); + let nonlinear = Function::Quadratic((linear_part + quadratic!(1, 2)).unwrap()); + let instance = instance_with_constraints(BTreeMap::from([( + ConstraintID::from(10), + Constraint::equal_to_zero(nonlinear), + )])); + + let err = instance + .check_promotion_witness(&witness(10, [1, 2], None), &allowed_one_hot()) + .unwrap_err(); + assert!(err.to_string().contains("not exactly linear")); + } + + #[test] + fn rejects_target_ids_used_in_active_or_removed_one_hot_collections() { + let existing = OneHotConstraint::new(variables([3, 4])).unwrap(); + let mut active_collision = one_source_instance(1.0); + active_collision + .one_hot_constraint_collection + .insert_active_with_context( + OneHotConstraintID::from(7), + existing.clone(), + ConstraintContext::default(), + ) + .unwrap(); + assert!(active_collision + .check_promotion_witness(&witness(10, [1, 2, 3], Some(7)), &allowed_one_hot(),) + .is_err()); + + active_collision + .convert_one_hot_to_constraint(OneHotConstraintID::from(7)) + .unwrap(); + assert!(active_collision + .check_promotion_witness(&witness(10, [1, 2, 3], Some(7)), &allowed_one_hot(),) + .is_err()); + } + + #[test] + fn bulk_reserves_explicit_targets_and_is_atomic() { + let mut instance = instance_with_constraints(BTreeMap::from([ + ( + ConstraintID::from(10), + Constraint::equal_to_zero(exact_one_hot_function(&[1, 2], 1.0)), + ), + ( + ConstraintID::from(11), + Constraint::equal_to_zero(exact_one_hot_function(&[3, 4], -2.0)), + ), + ])); + instance + .one_hot_constraint_collection + .insert_active_with_context( + OneHotConstraintID::from(5), + OneHotConstraint::new(variables([1])).unwrap(), + ConstraintContext::default(), + ) + .unwrap(); + + let report = instance + .promote_with_witnesses( + vec![witness(10, [1, 2], None), witness(11, [3, 4], Some(10))], + &allowed_one_hot(), + ) + .unwrap(); + assert_eq!( + report.source_to_target(), + &BTreeMap::from([ + (ConstraintID::from(10), OneHotConstraintID::from(11)), + (ConstraintID::from(11), OneHotConstraintID::from(10)), + ]) + ); + + let duplicate_source_before = instance.clone(); + assert!(instance + .promote_with_witnesses( + vec![witness(99, [1], Some(20)), witness(99, [1], Some(21)),], + &allowed_one_hot(), + ) + .is_err()); + assert_eq!(instance, duplicate_source_before); + + let mut atomic = instance_with_constraints(BTreeMap::from([ + ( + ConstraintID::from(20), + Constraint::equal_to_zero(exact_one_hot_function(&[1, 2], 1.0)), + ), + ( + ConstraintID::from(21), + Constraint::less_than_or_equal_to_zero(exact_one_hot_function(&[3, 4], 1.0)), + ), + ])); + let before = atomic.clone(); + assert!(atomic + .promote_with_witnesses( + vec![witness(20, [1, 2], None), witness(21, [3, 4], None),], + &allowed_one_hot(), + ) + .is_err()); + assert_eq!(atomic, before); + + let before = atomic.clone(); + assert!(atomic + .promote_with_witnesses( + vec![witness(20, [1, 2], Some(30)), witness(21, [3, 4], Some(30)),], + &allowed_one_hot(), + ) + .is_err()); + assert_eq!(atomic, before); + } + + #[test] + fn bulk_allocates_a_gap_when_an_explicit_target_is_u64_max() { + let mut instance = instance_with_constraints(BTreeMap::from([ + ( + ConstraintID::from(10), + Constraint::equal_to_zero(exact_one_hot_function(&[1, 2], 1.0)), + ), + ( + ConstraintID::from(11), + Constraint::equal_to_zero(exact_one_hot_function(&[3, 4], 1.0)), + ), + ])); + + let report = instance + .promote_with_witnesses( + vec![ + witness(10, [1, 2], None), + witness(11, [3, 4], Some(u64::MAX)), + ], + &allowed_one_hot(), + ) + .unwrap(); + assert_eq!( + report.source_to_target(), + &BTreeMap::from([ + (ConstraintID::from(10), OneHotConstraintID::from(0)), + (ConstraintID::from(11), OneHotConstraintID::from(u64::MAX),), + ]) + ); + } + + #[test] + fn preview_is_not_a_reusable_plan() { + let mut instance = one_source_instance(1.0); + let witness = witness(10, [1, 2, 3], None); + let preview = instance + .check_promotion_witness(&witness, &allowed_one_hot()) + .unwrap(); + assert_eq!( + preview.target_one_hot_constraint_id(), + OneHotConstraintID::from(0) + ); + + instance + .one_hot_constraint_collection + .insert_active_with_context( + OneHotConstraintID::from(0), + OneHotConstraint::new(variables([4])).unwrap(), + ConstraintContext::default(), + ) + .unwrap(); + let result = instance + .promote_with_witness(witness, &allowed_one_hot()) + .unwrap(); + assert_eq!( + result.target_one_hot_constraint_id(), + OneHotConstraintID::from(1) + ); + } + + #[test] + fn lowering_retains_auditable_history_and_blocks_source_restore() { + let mut instance = one_source_instance(-1.0); + instance + .promote_with_witness(witness(10, [1, 2, 3], None), &allowed_one_hot()) + .unwrap(); + instance.reduce_capabilities(&Capabilities::new()).unwrap(); + assert!(instance.one_hot_constraints().is_empty()); + assert!(instance + .removed_one_hot_constraints() + .contains_key(&OneHotConstraintID::from(0))); + + let audit = instance + .verify_promotion_history(ConstraintID::from(10)) + .unwrap(); + assert!(!audit.target_is_active()); + + let before_restore = instance.clone(); + let error = instance + .restore_constraint(ConstraintID::from(10)) + .unwrap_err(); + assert!(error.to_string().contains("Cannot restore promoted")); + assert_eq!(instance, before_restore); + + let bytes = instance.to_v2_bytes(); + let round_trip = Instance::from_v2_bytes(&bytes).unwrap(); + let audit = round_trip + .verify_promotion_history(ConstraintID::from(10)) + .unwrap(); + assert_eq!(audit.variables(), &variables([1, 2, 3])); + assert!(!audit.target_is_active()); + } + + #[test] + fn audit_normalizes_members_removed_by_exact_zero_propagation() { + let mut instance = one_source_instance(1.0); + instance + .promote_with_witness(witness(10, [1, 2, 3], None), &allowed_one_hot()) + .unwrap(); + instance + .partial_evaluate( + &crate::v1::State::from(std::collections::HashMap::from([(1, 0.0)])), + crate::ATol::default(), + ) + .unwrap(); + assert_eq!( + instance + .one_hot_constraints() + .get(&OneHotConstraintID::from(0)) + .unwrap() + .variables, + variables([2, 3]) + ); + + let audit = instance + .verify_promotion_history(ConstraintID::from(10)) + .unwrap(); + assert_eq!(audit.variables(), &variables([1, 2, 3])); + assert!(audit.target_is_active()); + + let round_trip = Instance::from_v2_bytes(&instance.to_v2_bytes()).unwrap(); + let audit = round_trip + .verify_promotion_history(ConstraintID::from(10)) + .unwrap(); + assert_eq!(audit.variables(), &variables([1, 2, 3])); + assert!(audit.target_is_active()); + } + + #[test] + fn audit_rejects_unjustified_target_shrinkage() { + let mut instance = one_source_instance(1.0); + instance + .promote_with_witness(witness(10, [1, 2, 3], None), &allowed_one_hot()) + .unwrap(); + instance + .one_hot_constraint_collection + .replace_active_row( + OneHotConstraintID::from(0), + OneHotConstraint::new(variables([2, 3])).unwrap(), + ) + .unwrap(); + + let error = instance + .verify_promotion_history(ConstraintID::from(10)) + .unwrap_err(); + assert!(error.to_string().contains("not fixed exactly to zero")); + } +}