Target-Relative Commitment Protection

Abstract

One commitment can protect balance while exposing three other history targets.

Theorem 1.1 (Commitment protection must name its history target).

$H i s t ory := B oo l \times B oo l \times B oo l \times B oo l \times B oo l, e d i t ((m, b, o, i, a)) := if (m, (m, not (b), o, i, a), (m, b, not (o), not (i), not (a))), co mmi t m e n t ((m, b, o, i, a)) := not (b), ba l an ce ((m, b, o, i, a)) := b, e v e n tO r d er ((m, b, o, i, a)) := o, i d e n t i t y S o u rce ((m, b, o, i, a)) := i, co n t r a c t A u t h or i z a t i o n ((m, b, o, i, a)) := a, o t h er E d i t := (f a l se, f a l se, f a l se, f a l se, f a l se), (\forall g amma \in H i s t ory, co mmi t m e n t (g amma) = co mmi t m e n t (e d i t (g amma)) \Rightarrow ba l an ce (g amma) = ba l an ce (e d i t (g amma))) \land co mmi t m e n t (o t h er E d i t) = co mmi t m e n t (e d i t (o t h er E d i t)) \land e v e n tO r d er (o t h er E d i t) \neq = e v e n tO r d er (e d i t (o t h er E d i t)) \land i d e n t i t y S o u rce (o t h er E d i t) \neq = i d e n t i t y S o u rce (e d i t (o t h er E d i t)) \land co n t r a c t A u t h or i z a t i o n (o t h er E d i t) \neq = co n t r a c t A u t h or i z a t i o n (e d i t (o t h er E d i t)) \land \neg (\forall T : H i s t ory \to B oo l, \forall g amma \in H i s t ory, co mmi t m e n t (g amma) = co mmi t m e n t (e d i t (g amma)) \Rightarrow T (g amma) = T (e d i t (g amma))) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Audits/TargetRelativeCommitment.commitment_protection_is_target_relative (✓ std3). ∎

Source. Repository-derived.

Commentary.

A history carries a mode bit followed by balance, event-order, identity-source, and contract-authorization coordinates.

The unauthorized edit changes balance in the first mode and changes the other three targets in the second. The commitment stores the Boolean complement of balance, so its injectivity detects every balance change.

At the second witness, the commitment and balance remain equal across the edit while order, identity source, and authorization all change on that same history. The negative clauses therefore cannot be separated into unrelated witnesses.

The final public clause applies the same collision to the order target and rules out protection that is independent of the named target.

References

Truth anchor: D5/S3/ConceptDynamics/Audits/TargetRelativeCommitment.commitment_protection_is_target_relative

Keyboard shortcuts

trureturing Blueprint

Target-Relative Commitment Protection

Abstract

References