lemmaroutine

Catalytic equality test for endpoint keys

Compares endpoint keys

k(v)=k(w)

with restoring catalytic workspace

equality test used by endpoint comparisons

Lemma·lem:fp-catalytic·§9.6 Catalytic key equality

Statement (paper)

Let

V\in\{0,1\}^B

be a shared vector with arbitrary initial contents. Suppose an excursion to either of two deterministically specified endpoints returns the cursor, and its path and result are independent of the incoming contents of

V

. Such excursions may use nested procedures which restore

V

. There is a procedure which xors the bit

\mathbf1_{k(v)=k(w)}

into a local result bit, restores

V

, and needs only constant local data across four endpoint excursions.

In plain English

Given a shared catalyst vector

V\in\{0,1\}^B

with arbitrary contents and two deterministic endpoints

v

and

w

whose excursions return the cursor with path and result independent of

V

, there is a procedure that xors the bit

\mathbf1_{k(v)=k(w)}

into a local result bit, restores

V

, and uses only constant local data across four endpoint excursions.

Why it's here

This lets the construction compare the keys of two endpoints without storing either key, by using the arbitrary-content vector

V

as borrowed workspace and restoring it afterward. It is the basic restoring, catalyst-independent equality test that the endpoint comparisons in the later control-equality lemma build on.

Classified routine:

This is an adaptation of the standard catalytic-computing trick of reversibly xoring values into a borrowed tape and uncomputing to restore it (Buhrman, Cleve, Koucký, Loff, Speelman 2014). Here it is used to test equality of two keys with four excursions.

Uses

Nothing else in the paper

Used by

lemEndpoint comparisons are restoring with O(d) control

Sources

PaperOpen

Section: §9.6 Catalytic key equality
Page: —
Label: lem:fp-catalytic
Line: sections/fingerprints.tex:766

Leannot aligned

Phase 2 aligns this node to a Lean declaration.