Weidner semidirect add/multiply: reordering and history permutation

Module verified

verified

Unbounded integer reference model for the add/multiply example in Composing and Decomposing Op-Based CRDTs with Semidirect Products. Proves transformed-add reordering, commuting multiply actions, action composition, and invariance of transformation under any permutation of multiplication messages. Does not model causal delivery, author metadata, duplicate suppression, reset, general semidirect-product correctness, or JavaScript floating-point arithmetic.

Namespace: Hunch.SemidirectArithmetic

SHA-256: 150ecbd7daaa885e0a25599b4b57955654f32f8cd6a2a4d39585ed0e09db66e9

Definitions and named lemmas

namespace Hunch.SemidirectArithmetic
def addEffect : (Int → Int → Int) :=
  fun a x => x + a

def multiplyEffect : (Int → Int → Int) :=
  fun m x => m * x

def transformAdd : (Int → Int → Int) :=
  fun m a => m * a

def transformHistory : (List Int → Int → Int) :=
  fun ms a => ms.foldr (fun m acc => m * acc) a

theorem reordering : (∀ m a x : Int, multiplyEffect m (addEffect a x) = addEffect (transformAdd m a) (multiplyEffect m x)) :=
  by
    intro m a x
    exact Int.mul_add m x a

theorem actions_commute : (∀ m n a : Int, transformAdd m (transformAdd n a) = transformAdd n (transformAdd m a)) :=
  by
    intro m n a
    exact Int.mul_left_comm m n a

theorem action_composition : (∀ m n a : Int, transformAdd (m*n) a = transformAdd m (transformAdd n a)) :=
  by
    intro m n a
    exact Int.mul_assoc m n a

theorem history_permutation : (∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, transformHistory xs a = transformHistory ys a) :=
  by
    intro xs ys h
    induction h with
    | nil => intro a; rfl
    | cons m h ih =>
      intro a
      exact congrArg (fun z => m * z) (ih a)
    | swap m n rest =>
      intro a
      exact Int.mul_left_comm n m (transformHistory rest a)
    | trans h1 h2 ih1 ih2 =>
      intro a
      exact (ih1 a).trans (ih2 a)

end Hunch.SemidirectArithmetic

Reproducible verification bundle · Signed receipt · Verification guide

Report module

Checker output

'_private.0.Hunch.SemidirectArithmetic.addEffect' does not depend on any axioms
'_private.0.Hunch.SemidirectArithmetic.multiplyEffect' does not depend on any axioms
'_private.0.Hunch.SemidirectArithmetic.transformAdd' does not depend on any axioms
'_private.0.Hunch.SemidirectArithmetic.transformHistory' does not depend on any axioms
'_private.0.Hunch.SemidirectArithmetic.reordering' depends on axioms: [propext]
'_private.0.Hunch.SemidirectArithmetic.actions_commute' depends on axioms: [propext]
'_private.0.Hunch.SemidirectArithmetic.action_composition' depends on axioms: [propext]
'_private.0.Hunch.SemidirectArithmetic.history_permutation' depends on axioms: [propext]
'_private.0.OA_target' does not depend on any axioms
OA_target : OA_statement

To use this module, pin {"id":3,"hash":"150ecbd7daaa885e0a25599b4b57955654f32f8cd6a2a4d39585ed0e09db66e9"} in your target’s modules array. Only independently verified modules can be used.