Blind mathematical read-back

The declarations below are in the namespace GBFPlus.OccupancyDisclosure. In the mathematical notation used here, $I_m=\{0,\ldots,m-1\}$ is the set of natural numbers strictly less than $m$, $B=\mathbb Z/2\mathbb Z$, and $B^{I_m}$ is the set of all functions from $I_m$ to $B$. Addition of such functions, and of pairs of such functions, is coordinatewise addition modulo two; zero denotes the corresponding all-zero function or pair. An optional value is either an absent value, written $\bot$, or a present value, written $\operatorname{some}(x)$; in particular, $\operatorname{some}(0)$ and $\bot$ are distinct. Finite-set sums include each member once, list sums include each occurrence, and an empty sum is zero. Each paragraph renders one explicit declaration, with the two anonymous instance declarations identified by the propositions they decide.

Config. A configuration is a record of four natural numbers $n$ (cells), $k$ (shares), $a$ (prefixBits), and $b$ (suffixBits), together with witnesses of the four inequalities $1\le k$, $k\le n$, $1\le a$, and $1\le b$. Thus every configuration has $1\le k\le n$ and positive $a,b$, and none of $n,k,a,b$ can be zero. These are all the fields and conditions in this record; no further relationship between the four numbers is imposed.

Word. For each configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, a word is an ordered pair $(u,v)$ in $B^{I_a}\times B^{I_b}$. Its first component assigns a residue modulo two to each of the $a$ prefix positions, and its second component assigns a residue modulo two to each of the $b$ suffix positions. Every such pair is a word, including the all-zero pair; there is no condition relating its two components to one another or to the cells or shares.

Identifier. For each configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, an identifier is any function $v:I_b\to B$. All $b$-coordinate binary functions, including zero, are allowed. The type carries no additional property such as uniqueness or a relation to a prefix.

Snapshot. For each configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, a snapshot is any function $A:I_n\to\operatorname{Option}(B^{I_a}\times B^{I_b})$. At each of the $n$ cells it specifies either $\bot$ or a present pair of binary functions of lengths $a$ and $b$. Every assignment of these optional values is allowed, including an assignment with no present cells or with every cell present; a present zero word is distinct from an absent cell.

wordBits. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every word $w=(u,v)\in B^{I_a}\times B^{I_b}$, this function returns the binary function $z:I_{a+b}\to B$ with $z(i)=u(i)$ when $0\le i<a$ and $z(i)=v(i-a)$ when $a\le i<a+b$. Thus the first component occupies the first $a$ positions and the second component occupies the following $b$ positions. The subtraction occurs in the second case, where $i\ge a$, so it gives an index in $I_b$; no sum of the two components is taken.

empty. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, this is the snapshot $A:I_n\to\operatorname{Option}(B^{I_a}\times B^{I_b})$ defined by $A(i)=\bot$ for every cell $i$. Its domain has $n\ge1$ cells, all absent; its values are not present zero words.

Row. For each configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, a row is a record consisting of a finite set $S\subseteq I_n$ (support), a witness that $|S|=k$ (support_card), a function $h:I_a\to B$ (hashPrefix), and a function $y:I_b\to B$ (identifier). The support has exactly $k\ge1$ distinct members and is therefore nonempty. Apart from the cardinality condition, these fields are unrestricted: the two binary functions are not required to be computed from one another or from the support, and separate rows may have equal supports, equal prefixes, or equal identifiers.

Row.target. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every row consisting of $S\subseteq I_n$ with $|S|=k$, $h:I_a\to B$, and $y:I_b\to B$, its target word is exactly $(h,y)\in B^{I_a}\times B^{I_b}$. The value uses the row's two binary functions and does not depend on which cells belong to its support.

Attempt. For each configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, an attempt is a record containing a row $(S,h,y)$ with $S\subseteq I_n$, $|S|=k$, $h:I_a\to B$, and $y:I_b\to B$; an optional cell $p\in\operatorname{Option}(I_n)$ (pivot); and an arbitrary function $f:I_n\to B^{I_a}\times B^{I_b}$ (free). The pivot may be absent or may name any cell, whether or not that cell is in $S$. The function $f$ is specified at every cell, including cells outside $S$, and has no distributional, independence, or other restriction. The record itself has no snapshot argument and imposes no occupancy requirement.

admissible. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every optional-word assignment $A:I_n\to\operatorname{Option}(B^{I_a}\times B^{I_b})$, and every attempt with row $(S,h,y)$, $|S|=k$, optional pivot, and arbitrary word function $f$, this proposition has two cases. If the pivot is absent, it means that $A(i)\ne\bot$ for every $i\in S$. If the pivot is $\operatorname{some}(p)$, it means the conjunction $p\in S$ and $A(p)=\bot$. In the latter case no condition is imposed on the other cells in $S$, which may be present or absent. Neither case constrains $h$, $y$, or $f$, and neither imposes a condition outside $S$. Since $|S|=k\ge1$, the universal condition in the absent-pivot case is not over an empty support; an absent-pivot attempt against the all-absent snapshot does not satisfy it.

Anonymous instance deciding admissible. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every snapshot $A:I_n\to\operatorname{Option}(B^{I_a}\times B^{I_b})$, this supplies, for each attempt with row support $S$ of cardinality $k$, an explicit decision of its admissibility proposition: either evidence that the proposition holds or evidence that it does not. An absent pivot selects the decision of $\forall i\in S,\ A(i)\ne\bot$; a present pivot $p$ selects the decision of $p\in S\land A(p)=\bot$. The row's prefix and identifier and the attempt's arbitrary word function do not enter these tests. This declares decidability for all attempts, including inadmissible ones; it does not assert that all attempts are admissible.

fillWord. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every snapshot $A:I_n\to\operatorname{Option}(W)$ where $W=B^{I_a}\times B^{I_b}$, every function $f:I_n\to W$, and every cell $i\in I_n$, this returns $w$ if $A(i)=\operatorname{some}(w)$ and returns $f(i)$ if $A(i)=\bot$. A present zero word returns zero rather than the fallback. No support, pivot, or admissibility condition is an argument or hypothesis.

insert. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, let $W=B^{I_a}\times B^{I_b}$; take any snapshot $A:I_n\to\operatorname{Option}(W)$, any row $(S,h,y)$ with $|S|=k$, any cell $p\in I_n$, and any function $f:I_n\to W$. Write $F(i)=w$ if $A(i)=\operatorname{some}(w)$ and $F(i)=f(i)$ if $A(i)=\bot$. The returned snapshot $A'$ is defined at each $i\in I_n$ by $A'(i)=A(i)$ for $i\notin S$, by $A'(i)=\operatorname{some}(F(i))$ for $i\in S$ with $i\ne p$, and by $A'(p)=\operatorname{some}\bigl((h,y)+\sum_{j\in S\setminus\{p\}}F(j)\bigr)$ if $p\in S$. The sums and addition are coordinatewise modulo two, and all $F(j)$ use the input snapshot $A$. No assumption requires $p\in S$ or $A(p)=\bot$: if $p\notin S$, every cell of $S$ receives the nonpivot rule and the value at $p$ is unchanged; if $p\in S$ and was already present, its value is overwritten by the displayed sum. Every cell of $S$ becomes present, even when its assigned word is zero. If $S=\{p\}$, the sum is empty and the word assigned at $p$ is $(h,y)$.

step. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every snapshot $A:I_n\to\operatorname{Option}(W)$ with $W=B^{I_a}\times B^{I_b}$, and every attempt consisting of a row $(S,h,y)$ with $|S|=k$, an optional pivot, and a function $f:I_n\to W$, this returns $A$ unchanged if the pivot is absent. If the pivot is $\operatorname{some}(p)$, define $F(i)$ to be the present word at $i$ in $A$, or $f(i)$ if that cell is absent; the returned snapshot leaves cells outside $S$ unchanged, assigns $\operatorname{some}(F(i))$ at each $i\in S\setminus\{p\}$, and, if $p\in S$, assigns $\operatorname{some}\bigl((h,y)+\sum_{j\in S\setminus\{p\}}F(j)\bigr)$ at $p$, with coordinatewise addition modulo two and an empty sum equal to zero. The operation requires no admissibility hypothesis and performs no admissibility test; it is defined for absent pivots when supported cells are absent and for present pivots outside the support or at already-present cells.

run. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every initial snapshot $A:I_n\to\operatorname{Option}(W)$ where $W=B^{I_a}\times B^{I_b}$, and every finite list of attempts, this returns the result of processing the list in order from its first element to its last. An attempt contains a support $S\subseteq I_n$ of size $k$, a prefix $h:I_a\to B$, an identifier $y:I_b\to B$, an optional pivot, and a function $f:I_n\to W$. An absent pivot leaves the current snapshot unchanged. For a present pivot $p$, let $F(i)$ be the current word at $i$ when present and $f(i)$ otherwise; the next snapshot leaves cells outside $S$ unchanged, stores $F(i)$ at every nonpivot cell $i\in S$, and, if $p\in S$, stores $(h,y)+\sum_{j\in S\setminus\{p\}}F(j)$ at $p$, where every stored value is marked present and all additions are coordinatewise modulo two. Processing the empty list returns the initial snapshot itself. Lists may repeat attempts, and no admissibility condition is imposed on the initial snapshot or any list entry.

Honest. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every initial snapshot $A:I_n\to\operatorname{Option}(W)$ where $W=B^{I_a}\times B^{I_b}$, and every finite list of attempts, this is the recursively defined proposition that each attempt meets its pivot condition in the snapshot reached immediately before it. For an attempt with row $(S,h,y)$, $|S|=k$, optional pivot, and word function $f$, that condition is $\forall i\in S,\ A(i)\ne\bot$ if the pivot is absent, and $p\in S\land A(p)=\bot$ if the pivot is $\operatorname{some}(p)$, using the current snapshot in place of $A$. An absent pivot leaves that snapshot unchanged; for a present pivot $p$, let $F(i)$ be its current present word, or $f(i)$ if absent, leave cells outside $S$ unchanged, store $F(i)$ at cells of $S$ other than $p$, and store $(h,y)+\sum_{j\in S\setminus\{p\}}F(j)$ at $p$ when $p\in S$, with coordinatewise addition modulo two and all newly stored values marked present. For a nonempty list, the proposition is the conjunction of the first attempt's condition and the same recursively defined proposition for the remaining list at this updated snapshot. For the empty list it is true for every initial snapshot. There is no requirement that the initial snapshot be all absent, and no restriction on the values of the word functions beyond their types.

honestDecidable. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, this supplies a decision for every snapshot $A:I_n\to\operatorname{Option}(W)$, $W=B^{I_a}\times B^{I_b}$, and every finite list of attempts, as to whether the following successive conditions hold. An attempt has row $(S,h,y)$ with $|S|=k$, optional pivot, and word function $f$; an absent pivot requires every cell of $S$ currently present and makes no update, whereas a present pivot $p$ requires $p\in S$ and its current cell absent. The update associated to a present pivot uses $F(i)$ equal to the current present word or $f(i)$ if absent, preserves cells outside $S$, stores $F(i)$ at each nonpivot supported cell, and, if $p\in S$, stores $(h,y)+\sum_{j\in S\setminus\{p\}}F(j)$ at $p$, with coordinatewise addition modulo two and newly stored words marked present. The decision is affirmative for an empty list. For a nonempty list it combines the decision of the first pivot condition with the recursively obtained decision for the remaining list at the updated snapshot, deciding their conjunction. Its result is either evidence that all successive conditions hold or evidence that they do not; it makes no assertion that an arbitrary input list satisfies them.

Anonymous instance deciding Honest. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every snapshot $A:I_n\to\operatorname{Option}(W)$ with $W=B^{I_a}\times B^{I_b}$, and every finite list of attempts, this installs the recursively computed decision of the following property: at each attempt, with row $(S,h,y)$ of support size $k$, optional pivot, and word function $f$, an absent pivot has all supported cells currently present, while a present pivot $p$ belongs to $S$ and is currently absent. Snapshots evolve in list order by leaving them unchanged for absent pivots and, for present pivots, taking $F(i)$ to be the current present word or the fallback $f(i)$, leaving cells outside $S$ unchanged, storing $F(i)$ at each $i\in S\setminus\{p\}$, and storing $(h,y)+\sum_{j\in S\setminus\{p\}}F(j)$ at $p$ if $p\in S$, where addition is coordinatewise modulo two and stored words are present. The empty list satisfies the property regardless of $A$. The installed decision produces either evidence of this property or its negation for every input, and has no additional hypothesis beyond the specified types.

successful. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every finite list of attempts, each having a row $(S,h,y)$ with $S\subseteq I_n$, $|S|=k$, $h:I_a\to B$, and $y:I_b\to B$, an optional cell pivot, and an arbitrary function $I_n\to B^{I_a}\times B^{I_b}$, this returns the list of rows from precisely those attempts whose pivots are present. It keeps their original order and multiplicities, discards attempts with absent pivots, and discards the actual pivot values and word functions from the result. It has no snapshot argument and checks neither pivot membership in the support nor occupancy nor any successive admissibility condition. The input list may be empty, in which case the returned list is empty.

finalSnapshot. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every finite list of attempts, this produces an optional-word assignment on $I_n$ by starting with $A(i)=\bot$ at every cell and processing the attempts in list order. For each attempt with row $(S,h,y)$, $|S|=k$, optional pivot, and function $f:I_n\to W$ where $W=B^{I_a}\times B^{I_b}$, an absent pivot leaves the current assignment unchanged. For a present pivot $p$, let $F(i)$ be the current present word at $i$ or $f(i)$ if absent; the next assignment preserves cells outside $S$, stores $F(i)$ at cells of $S$ other than $p$, and stores $(h,y)+\sum_{j\in S\setminus\{p\}}F(j)$ at $p$ if $p\in S$, with coordinatewise addition modulo two and all stored words marked present. The returned snapshot is the assignment after the last entry; for the empty list it is the all-absent assignment. No admissibility condition is assumed or tested, so the function also accepts lists containing pivots outside their supports or at already-present cells.

occupied. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every snapshot $A:I_n\to\operatorname{Option}(B^{I_a}\times B^{I_b})$, this is the finite set $\{i\in I_n\mid A(i)=\operatorname{some}(w)\text{ for some }w\in B^{I_a}\times B^{I_b}\}$. Membership depends only on whether a word is present, so a cell containing a zero word belongs to this set. The set is empty for an all-absent snapshot and is $I_n$ for a snapshot with every cell present; it has no row or list argument.

payload. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every snapshot $A:I_n\to\operatorname{Option}(W)$ where $W=B^{I_a}\times B^{I_b}$, and every cell $i\in I_n$, this returns the word $w$ when $A(i)=\operatorname{some}(w)$ and returns the all-zero word of $W$ when $A(i)=\bot$. Consequently an absent cell and a cell containing the zero word have the same returned payload, even though their optional snapshot values differ. There is no hypothesis that $i$ is occupied.

rowXor. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, every snapshot $A:I_n\to\operatorname{Option}(W)$ with $W=B^{I_a}\times B^{I_b}$, and every row $(S,h,y)$ with $S\subseteq I_n$, $|S|=k$, $h:I_a\to B$, and $y:I_b\to B$, this returns $\sum_{i\in S}P(i)\in W$, where $P(i)$ is the word present at $i$ in $A$, or the all-zero word if that cell is absent. The sum is coordinatewise modulo two and counts each supported cell once. The support is nonempty, but every summand may still be zero, including when all supported cells are absent. The row's prefix $h$ and identifier $y$ do not enter the expression, and no assertion equates this sum with $(h,y)$.

recover. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every snapshot $A:I_n\to\operatorname{Option}(W)$ where $W=B^{I_a}\times B^{I_b}$, this returns the suffix component of $\sum_{i\in O}P(i)$, where $O=\{i\in I_n\mid A(i)\text{ is present}\}$ and $P(i)$ is the present word at $i$ or zero if it is absent. Equivalently, the returned function $y:I_b\to B$ is defined by $y(t)=\sum_{i\in O}v_i(t)$, where $A(i)=\operatorname{some}(u_i,v_i)$ for $i\in O$ and each sum is modulo two. Each occupied cell is counted once; cells storing zero are included and contribute zero. If $O$ is empty, the result is the all-zero identifier. There is no input row, list of attempts, or admissibility hypothesis, and the definition asserts no relationship between this result and any prescribed identifier.

supportUnion. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every finite list of rows $(S_1,h_1,y_1),\ldots,(S_m,h_m,y_m)$, where each $S_j\subseteq I_n$ has cardinality $k$, each $h_j:I_a\to B$, and each $y_j:I_b\to B$, this returns a finite set formed by starting with $U_0=\varnothing$ and defining $U_j=U_{j-1}\cup S_j$ for $j=1,\ldots,m$. Thus its value is $\bigcup_{j=1}^{m}S_j$. Empty lists give the empty set, repeated rows or overlapping supports do not create multiplicities, and the prefixes and identifiers are unused. Every individual support is nonempty; the union is nonempty when the list is nonempty.

identifierXor. For every configuration $C$ with natural parameters $n,k,a,b$ satisfying $1\le k\le n$, $1\le a$, and $1\le b$, and every finite list of rows $(S_1,h_1,y_1),\ldots,(S_m,h_m,y_m)$, where each $S_j\subseteq I_n$ has cardinality $k$, each $h_j:I_a\to B$, and each $y_j:I_b\to B$, this returns the function $y:I_b\to B$ defined by $y(t)=\sum_{j=1}^{m}y_j(t)$, with addition modulo two. Every row occurrence in the list contributes once, including repeated rows or repeated identifiers; an identifier repeated twice contributes zero from those two occurrences. The empty list returns the all-zero identifier. The row supports and prefixes do not enter this sum, and no uniqueness or disjointness hypothesis is required.