Replace an implementation

Move an implementation's alias to a new implementation, backed by an accepted proof that the new one replaces the old.

The replace method moves an alias from one implementation to another only when you name an accepted theorem of the exact replacement claim. For Core v2 the claim is Replaces from lean/core/Replaces.lean: the two implementations’ start states are related, and Simulates holds between them under that relation. By replaces_runs, every client that is safe on the contract then gets the same result from both. Contracts, implementations and proofs explains the idea. The steps below follow crates/lema-cli/tests/replace_v2.rs and its counter example, lean/core/ReplaceV2.lean.

Before you start

• A running server on a store where Core v2 is accepted. Publish lean/core/CoreV2.lean with "prefix": "LemaDraft", "seed_salt": "lean/core" and "seeds" set to the seeds object of lean/core/seeds.json, and keep the names map from the response.
• You know how Received.* bindings work (Reuse a proof by identity).
• In the commands, $SOCK is the server’s socket. In the request files, values in angle brackets are placeholders. source is the Lean file’s text as one JSON string: jq -Rs . lean/core/Replaces.lean prints it encoded.

Steps

1. Publish lean/core/Replaces.lean, which defines Replaces and proves replaces_runs. Bind the Core v2 names it uses. Each binding’s value is that name’s entry in Core v2’s names map, copied as it is (some entries carry a role):

   {"source": "<text of lean/core/Replaces.lean>",
    "prefix": "LemaDraft",
    "seed_salt": "lean/core/Replaces",
    "bindings": {
      "Received.Contract": <names["LemaDraft.Contract"]>,
      "Received.Impl": <names["LemaDraft.Impl"]>,
      "Received.Simulates": <names["LemaDraft.Simulates"]>,
      "Received.Safe": <names["LemaDraft.Safe"]>,
      "Received.Prog": <names["LemaDraft.Prog"]>,
      "Received.run": <names["LemaDraft.run"]>,
      "Received.replacement": <names["LemaDraft.replacement"]>}}

   lema --socket $SOCK call publish --params-file replaces.json

   Keep the response’s names: the next step binds LemaDraft.Replaces.

2. Publish lean/core/ReplaceV2.lean the same way, with "seed_salt": "lean/core/ReplaceV2" and these bindings:

   Binding	Entry
   Received.Contract	LemaDraft.Contract
   Received.mkContract	LemaDraft.Contract.mk
   Received.Impl	LemaDraft.Impl
   Received.mkImpl	LemaDraft.Impl.mk
   Received.Simulates	LemaDraft.Simulates
   Received.Replaces	LemaDraft.Replaces, from step 1

   The file defines the contract counter (each tick replies with the count so far) and two implementations: plain holds the count, and offset holds the count plus five. It also defines the relation Shifted between their states, the claim PlainOffset := Received.Replaces 0 0 5 counter plain offset Shifted and its proof plain_offset.

3. Point the alias at the current implementation, if it does not name it already:

   lema --socket $SOCK call alias --params '{"name": "counter.impl", "target": {"id": "<plain>"}, "expect": null}'

4. Replace it. Every field except name is the ID of an accepted declaration, taken from the names maps (LemaDraft.ReplaceV2.plain and so on):

   {"name": "counter.impl",
    "expected": "<plain>",
    "target": "<offset>",
    "contract": "<counter>",
    "claim": "<PlainOffset>",
    "proof": "<plain_offset>",
    "representation": "<Shifted>",
    "relation": "<LemaDraft.Replaces>"}

   lema --socket $SOCK call replace --params-file replace.json

   You may also give expected_generation (the generation find reports) and an idempotency_key, which work as they do for alias. Any other field is refused.

5. Read the result. The response is the witness: name, old, new, contract, claim, proof, representation, namespace, relation, prefix and scope. Here prefix holds the claim’s eight leading arguments: the implicit C R S M N and the start states 0 0 5. The move and its witness are one replace line in the store’s history, and find now shows counter.impl at offset, generation 2.

Refusals

The store checks the claim before anything moves:

Reading the witness

The witness records that an accepted proof of exactly this claim exists. Nothing is re-addressed: a client sees offset only when it looks the alias up again and binds the new ID. If you rely on a witness, check its relation, leading arguments and representation. The start states are yours to choose, so they must match the deployment. Moving back needs a claim of its own, with the representation (Shifted) flipped.