Hegel properties over the code a card passes through: any text walks
into lines that rejoin as it, a fold anywhere reads as the line
unfolded, replace/substitute/extract move only the lines they name, a
diff takes the card before to the card after, the note's join and
split are one round trip, every birthday spelling reads back, the
match's distance is a metric, and sync tokens read back only where
they were minted. A state machine drives puts, edits and deletes
against a store and checks that a client at any token catches up
through #changes and that a card's diffs rebuild it.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VAiyEheRBdzbBjZUDWZUPk

diff --git a/test/pro_tacts/admin/test_format.rb b/test/pro_tacts/admin/test_format.rb
index db7dd2e..5a2abf6 100644
--- a/test/pro_tacts/admin/test_format.rb
+++ b/test/pro_tacts/admin/test_format.rb
@@ -1,10 +1,14 @@
 require_relative "../../test_helper"
 
+require "hegel"
+
 require "pro_tacts/admin/format"
 require "pro_tacts/contact"
 require "pro_tacts/vcard"
 
 class FormatTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   CARD = "BEGIN:VCARD\r\nVERSION:3.0\r\nFN:Ada Lovelace\r\nN:Lovelace;Ada;;;\r\n" \
     "UID:ada\r\nEND:VCARD\r\n"
 
@@ -180,4 +184,17 @@ class FormatTest < Minitest::Test
     assert_equal "3d ago", ProTacts::Admin::Format.time_ago((now - 3 * 86_400).iso8601(3))
     assert_equal "2mo ago", ProTacts::Admin::Format.time_ago((now - 60 * 86_400).iso8601(3))
   end
+
+  ## Property tests
+
+  # A search key is already folded, so folding it again changes
+  # nothing: a query and a value both reach the comparison as keys,
+  # however many times either was folded on the way.
+  def test_a_search_key_is_its_own_key
+    Hegel.test(test_cases: 1_000) do |tc|
+      key = ProTacts::Admin::Format.search_key(tc.draw(text(max_size: 20)))
+
+      assert_equal key, ProTacts::Admin::Format.search_key(key)
+    end
+  end
 end
diff --git a/test/pro_tacts/import/test_match.rb b/test/pro_tacts/import/test_match.rb
index 0d485a6..2d0dd04 100644
--- a/test/pro_tacts/import/test_match.rb
+++ b/test/pro_tacts/import/test_match.rb
@@ -1,11 +1,15 @@
 require_relative "../../test_helper"
 
+require "hegel"
+
 require "pro_tacts/contact"
 require "pro_tacts/import/match"
 
 # The contacts an arriving card might be
 # (docs/plans/2026-09-23-merging-on-import.md).
 class ImportMatchTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   Match = ProTacts::Import::Match
 
   def contact(id, name, *lines)
@@ -106,4 +110,55 @@ class ImportMatchTest < Minitest::Test
 
     assert_empty Match.candidates(arriving, [contact("jane", "Jane Booles")])
   end
+
+  ## Property tests
+
+  # Strings over a two-letter alphabet share most of their characters,
+  # so the distances between them are small and varied; strings from
+  # all of Unicode are mostly as far apart as they are long.
+  def word = one_of(from_regex("[ab]{0,8}", fullmatch: true), text(max_size: 8))
+
+  # Levenshtein's distance is a metric, and the match ranks by it as
+  # one: the same in both directions ...
+  def test_the_distance_is_symmetric
+    Hegel.test(test_cases: 1_000) do |tc|
+      a, b = tc.draw(word), tc.draw(word)
+
+      assert_equal Match.distance(a, b), Match.distance(b, a)
+    end
+  end
+
+  # ... never shorter than a detour through a third string ...
+  def test_the_distance_obeys_the_triangle_inequality
+    Hegel.test(test_cases: 1_000) do |tc|
+      a, b, c = tc.draw(word), tc.draw(word), tc.draw(word)
+
+      assert_operator Match.distance(a, c), :<=, Match.distance(a, b) + Match.distance(b, c)
+    end
+  end
+
+  # ... and bounded by the strings themselves: at least the difference
+  # in their lengths, at most the longer one's length, and zero only
+  # between equals — which is what keeps a likeness between 0 and 1.
+  def test_the_distance_is_bounded_by_the_lengths
+    Hegel.test(test_cases: 1_000) do |tc|
+      a, b = tc.draw(word), tc.draw(word)
+      distance = Match.distance(a, b)
+
+      assert_includes (a.length - b.length).abs..[a.length, b.length].max, distance
+      assert_equal a == b, distance.zero?
+    end
+  end
+
+  # A number's punctuation and its country code are no part of it:
+  # whatever surrounds a number's digits, it compares as those digits'
+  # last ten.
+  def test_a_phone_compares_as_its_last_ten_digits_whatever_surrounds_them
+    Hegel.test(test_cases: 1_000) do |tc|
+      digits = tc.draw(from_regex("[0-9]{0,14}", fullmatch: true))
+      spelled = digits.chars.map { tc.draw(from_regex("[^0-9]{0,2}", fullmatch: true)) + it }.join
+
+      assert_equal digits.chars.last(Match::PHONE_DIGITS).join, Match.phone(spelled + tc.draw(from_regex("[^0-9]{0,3}", fullmatch: true)))
+    end
+  end
 end
diff --git a/test/pro_tacts/test_birthday.rb b/test/pro_tacts/test_birthday.rb
index 551e1f8..b6c513c 100644
--- a/test/pro_tacts/test_birthday.rb
+++ b/test/pro_tacts/test_birthday.rb
@@ -1,9 +1,13 @@
 require_relative "../test_helper"
 
+require "hegel"
+
 require "pro_tacts/birthday"
 require "pro_tacts/vcard"
 
 class BirthdayTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   # The six shapes RFC 6350 section 4.3.1 admits, one assertion per
   # shape so a failure names the one that broke.
   def test_every_admitted_shape_constructs
@@ -192,4 +196,95 @@ class BirthdayTest < Minitest::Test
       assert_nil ProTacts::Birthday.from_property(unmodeled), unmodeled.value
     end
   end
+
+  ## Property tests
+
+  # Any birthday the constructor admits, all six shapes.
+  def any_birthday
+    year = integers(min_value: 0, max_value: 9999)
+    month = integers(min_value: 1, max_value: 12)
+    day = integers(min_value: 1, max_value: 31)
+    one_of(
+      tuples(year, month, day), tuples(year, month, just(nil)), tuples(year, just(nil), just(nil)),
+      tuples(just(nil), month, day), tuples(just(nil), month, just(nil)), tuples(just(nil), just(nil), day),
+    ).map { |y, m, d| ProTacts::Birthday.new(year: y, month: m, day: d) }
+  end
+
+  # The spellings a shape is read in (the patterns on Birthday): a
+  # full date bare or with any time RFC 2426 section 3.1.5 allows,
+  # and a month-day in both its basic and extended form.
+  def spelling(birthday)
+    y = birthday.year&.then { format("%04d", it) }
+    m, d = [birthday.month, birthday.day].map { it&.then { format("%02d", it) } }
+    case [y, m, d]
+    in [String, String, String]
+      from_regex("(T[0-9]{2}:?[0-9]{2}(:?[0-9]{2}(\\.[0-9]+)?)?(Z|[+-][0-9]{2}:?[0-9]{2})?)?", fullmatch: true)
+        .map { "#{y}-#{m}-#{d}#{it}" }
+    in [nil, String, String] then sampled_from(["--#{m}#{d}", "--#{m}-#{d}"])
+    in [String, String, nil] then just("#{y}-#{m}")
+    in [String, nil, nil] then just(y)
+    in [nil, String, nil] then just("--#{m}")
+    in [nil, nil, String] then just("---#{d}")
+    end
+  end
+
+  # Every admitted birthday, in every spelling its shape has, reads
+  # back as itself — VALUE=date or not, which names the default and
+  # so says nothing. A full date in 1604 is the one that reads as
+  # something else, a month and day (Birthday::NO_YEAR, and
+  # docs/plans/2026-09-11-every-birthday-in-the-model.md, "1604 means
+  # no year"); a partial date in 1604 keeps its year.
+  def test_every_spelling_of_every_shape_reads_back
+    Hegel.test(test_cases: 1_000) do |tc|
+      birthday = tc.draw(any_birthday)
+      value = tc.draw(spelling(birthday))
+      parameters = tc.draw(sampled_from([[], [["VALUE", "date"]], [["value", "DATE"]]]))
+
+      expected = birthday.year == 1604 && birthday.day ? birthday.with(year: nil) : birthday
+      assert_equal expected, ProTacts::Birthday.from_property(property(value, parameters:))
+    end
+  end
+
+  # A spelling with one component out of its range is in no spelling
+  # this reads, so it stays in the card as it came rather than reaching
+  # a constructor that would refuse it.
+  def test_a_component_out_of_range_reads_as_nothing
+    Hegel.test(test_cases: 1_000) do |tc|
+      month = tc.draw(one_of(just(0), integers(min_value: 13, max_value: 99)).map { it.to_s.rjust(2, "0") })
+      day = tc.draw(one_of(just(0), integers(min_value: 32, max_value: 99)).map { it.to_s.rjust(2, "0") })
+      value = tc.draw(sampled_from(["1985-#{month}-12", "1985-04-#{day}", "--#{month}12", "--04#{day}",
+                                    "1985-#{month}", "--#{month}", "---#{day}"]))
+
+      assert_nil ProTacts::Birthday.from_property(property(value))
+    end
+  end
+
+  # What a served birthday sends, read back the way a client's PUT of
+  # it is read, is the birthday it was — the round trip that serving
+  # only the two shapes Apple keeps exists for, a 1604 full date
+  # aside as above.
+  def test_a_served_birthday_reads_back_from_its_line
+    Hegel.test(test_cases: 1_000) do |tc|
+      birthday = tc.draw(any_birthday)
+      tc.assume(birthday.served?)
+
+      read = ProTacts::VCard::Parser.lines("#{birthday.to_line}\r\n").fetch(0).property
+      expected = birthday.year == 1604 ? birthday.with(year: nil) : birthday
+      assert_equal expected, ProTacts::Birthday.from_property(read)
+    end
+  end
+
+  # The day a birthday next lands on is the first day from today on
+  # that is its day — the month's last when the month has no such day
+  # — so none is skipped and none comes early.
+  def test_next_on_is_the_first_day_from_today_that_is_the_birthday
+    Hegel.test(test_cases: 1_000) do |tc|
+      birthday = tc.draw(any_birthday)
+      tc.assume(birthday.month && birthday.day)
+      today = tc.draw(dates(min_value: Date.new(1900, 1, 1), max_value: Date.new(2200, 12, 31)))
+
+      lands = ->(date) { date.month == birthday.month && date.day == [birthday.day, Date.new(date.year, date.month, -1).day].min }
+      assert_equal (today..).find(&lands), birthday.next_on(today)
+    end
+  end
 end
diff --git a/test/pro_tacts/test_card_diff.rb b/test/pro_tacts/test_card_diff.rb
index 18983ec..a0cf39a 100644
--- a/test/pro_tacts/test_card_diff.rb
+++ b/test/pro_tacts/test_card_diff.rb
@@ -1,9 +1,13 @@
 require_relative "../test_helper"
 
+require "hegel"
+
 require "pro_tacts/card_diff"
 require "pro_tacts/vcard"
 
 class CardDiffTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   AIDEN = "BEGIN:VCARD\r\nVERSION:3.0\r\nFN:Aiden\r\nUID:aiden\r\nEND:VCARD\r\n"
 
   def card(bytes) = ProTacts::VCard.new(bytes)
@@ -69,4 +73,100 @@ class CardDiffTest < Minitest::Test
 
     assert_equal diff, ProTacts::CardDiff.from_json(diff.to_json)
   end
+
+  ## Property tests
+
+  # A few lines drawn often, so two cards share some and a card
+  # carries some twice, beside lines drawn fresh.
+  COMMON = ["FN:Ada", "NOTE:one two", "TEL:+1-555-0100", "item1.EMAIL:ada@example.com"].freeze #: Array[String]
+
+  def content = one_of(sampled_from(COMMON), from_regex('[A-Z]{1,4}:[^\r\n]{0,10}', fullmatch: true))
+
+  def contents = arrays(content, max_size: 8)
+
+  # The lines as a client might spell them on the wire: each with its
+  # own terminator and maybe a fold, in an order of the draw's.
+  def card_of(tc, lines)
+    order = tc.draw(arrays(integers, min_size: lines.length, max_size: lines.length))
+    spelled = lines.zip(order).sort_by(&:last).map { |line, _|
+      terminator = tc.draw(sampled_from(["\r\n", "\n"]))
+      fold = tc.draw(integers(min_value: 0, max_value: line.length - 1))
+      "#{fold.zero? ? line : line.dup.insert(fold, "#{terminator} ")}#{terminator}"
+    }
+    card(spelled.join)
+  end
+
+  # What a diff is over: the card's logical lines, unfolded and with
+  # no terminator — the unit the class comment names.
+  def content_of(vcard) = vcard.lines.map(&:content).reject(&:empty?)
+
+  # The diff is the write: the card before, with what it removed taken
+  # off and what it added put on, carries the lines of the card after.
+  def test_a_diff_takes_the_card_before_to_the_card_after
+    Hegel.test(test_cases: 1_000) do |tc|
+      before = card_of(tc, tc.draw(contents))
+      after = card_of(tc, tc.draw(contents))
+      diff = between(before, after)
+
+      remaining = content_of(before).tally
+      diff.removed.each { remaining[it] -= 1 }
+      diff.added.each { remaining[it] = remaining.fetch(it, 0) + 1 }
+      assert_equal content_of(after).tally, remaining.reject { |_, count| count.zero? }
+    end
+  end
+
+  # Lines both cards carry cancel, so no line is both added and
+  # removed: a write records what moved and nothing that stood still.
+  def test_no_line_is_both_added_and_removed
+    Hegel.test(test_cases: 1_000) do |tc|
+      diff = between(card_of(tc, tc.draw(contents)), card_of(tc, tc.draw(contents)))
+
+      assert_empty diff.added & diff.removed
+    end
+  end
+
+  # The diff back is the diff forward turned around.
+  def test_the_diff_back_is_the_diff_forward_reversed
+    Hegel.test(test_cases: 1_000) do |tc|
+      before = card_of(tc, tc.draw(contents))
+      after = card_of(tc, tc.draw(contents))
+
+      forward = between(before, after)
+      assert_equal [forward.removed, forward.added], between(after, before).deconstruct
+    end
+  end
+
+  # A card's own lines spelled again — reordered, refolded, its line
+  # breaks swapped — is no change: the shuffle macOS makes of every
+  # card it touches (docs/apple-contacts.md) and the folds the wire
+  # moves (RFC 2426 section 2.6).
+  def test_the_same_lines_spelled_again_are_no_change
+    Hegel.test(test_cases: 1_000) do |tc|
+      lines = tc.draw(contents)
+
+      assert_predicate between(card_of(tc, lines), card_of(tc, lines)), :empty?
+    end
+  end
+
+  # The group log's path and the card's are the same difference by
+  # the same code (CardDiff.between_lines), so over the same lines
+  # they agree.
+  def test_a_groups_lines_diff_as_a_cards_would
+    Hegel.test(test_cases: 1_000) do |tc|
+      before = card_of(tc, tc.draw(contents))
+      after = card_of(tc, tc.draw(contents))
+
+      assert_equal between(before, after), ProTacts::CardDiff.between_lines(content_of(before), content_of(after))
+    end
+  end
+
+  # The stored spelling holds any line byte for byte, whatever it
+  # carries.
+  def test_any_diff_survives_the_column_it_is_stored_in
+    Hegel.test(test_cases: 1_000) do |tc|
+      diff = ProTacts::CardDiff.new(added: tc.draw(arrays(text(max_size: 20))), removed: tc.draw(arrays(text(max_size: 20))))
+
+      assert_equal diff, ProTacts::CardDiff.from_json(diff.to_json)
+    end
+  end
 end
diff --git a/test/pro_tacts/test_change_id.rb b/test/pro_tacts/test_change_id.rb
index b78feda..ace5841 100644
--- a/test/pro_tacts/test_change_id.rb
+++ b/test/pro_tacts/test_change_id.rb
@@ -1,8 +1,12 @@
 require_relative "../test_helper"
 
+require "hegel"
+
 require "pro_tacts/change_id"
 
 class ChangeIdTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   def test_an_id_is_as_many_letters_from_k_to_z_as_asked_for
     [1, 4, 7, 32].each do |length|
       assert_match(/\A[k-z]{#{length}}\z/, ProTacts::ChangeId.mint(length))
@@ -28,4 +32,16 @@ class ChangeIdTest < Minitest::Test
   def test_letters_outside_the_alphabet_are_not_minted
     refute ProTacts::ChangeId.minted?("abcdefghijjj")
   end
+
+  ## Property tests
+
+  # #minted? recognizes what #mint draws for a contact, and nothing
+  # drawn at another length: the width is the whole of the shape.
+  def test_minted_recognizes_a_contacts_length_and_no_other
+    Hegel.test(test_cases: 1_000) do |tc|
+      length = tc.draw(integers(min_value: 1, max_value: 32))
+
+      assert_equal length == ProTacts::ChangeId::CONTACT_LENGTH, ProTacts::ChangeId.minted?(ProTacts::ChangeId.mint(length))
+    end
+  end
 end
diff --git a/test/pro_tacts/test_note_sections.rb b/test/pro_tacts/test_note_sections.rb
index 355414e..972835c 100644
--- a/test/pro_tacts/test_note_sections.rb
+++ b/test/pro_tacts/test_note_sections.rb
@@ -1,5 +1,7 @@
 require_relative "../test_helper"
 
+require "hegel"
+
 require "pro_tacts/note_sections"
 
 # The text algebra of the one NOTE a served card carries, on its own
@@ -9,6 +11,8 @@ require "pro_tacts/note_sections"
 # each alone where they do not — the split tolerating the whitespace a
 # person's editing moves, the join writing one shape only.
 class NoteSectionsTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   NEIGHBOURS = ProTacts::NoteSections.header("Neighbours") #: String
 
   def section(label, text) = ProTacts::NoteSections::Section.new(label:, text:)
@@ -116,4 +120,64 @@ class NoteSectionsTest < Minitest::Test
 
     assert_equal [section("Dog walkers", "Sunday"), section("Neighbours", "bins")], read.sections
   end
+
+  ## Property tests
+
+  def labels = arrays(from_regex('[^\n]{1,12}', fullmatch: true), max_size: 4).map(&:uniq)
+
+  # A text as the join is handed one: lines of anything, no blank line
+  # at either end — the space between parts is the composer's — and no
+  # line that reads as a header of a label in play, since one line
+  # cannot be both a person's words and a section's start.
+  def body(labels)
+    headers = labels.map { ProTacts::NoteSections.header(it) }
+    arrays(from_regex('[^\n]{0,12}', fullmatch: true), max_size: 4)
+      .map { |lines| trim(lines).join("\n") }
+      .filter { |text| text.split("\n").none? { headers.include?(it.rstrip) } }
+  end
+
+  def trim(lines)
+    lines.drop_while { it.strip.empty? }.reverse.drop_while { it.strip.empty? }.reverse
+  end
+
+  # The two halves are one round trip (the module comment): what the
+  # join writes, the split reads back as the member text and sections
+  # it was made of, whatever labels nothing lends are also in play.
+  def test_the_split_reads_back_what_the_join_wrote
+    Hegel.test(test_cases: 1_000) do |tc|
+      lending = tc.draw(labels)
+      idle = tc.draw(labels) - lending
+      member = tc.draw(body(lending + idle))
+      sections = lending.map { section(it, tc.draw(body(lending + idle))) }
+
+      read = split(ProTacts::NoteSections.join(member, sections), lending + idle)
+      assert_equal ProTacts::NoteSections::Split.new(member:, sections:), read
+    end
+  end
+
+  # Lines a person might leave in a note they edited: the headers
+  # themselves, spelled right and nearly, blanks, and words.
+  def edited_line(labels)
+    one_of(
+      sampled_from(labels).map { ProTacts::NoteSections.header(it) },
+      sampled_from(labels).map { "#{ProTacts::NoteSections.header(it)} " },
+      sampled_from(labels).map { " #{ProTacts::NoteSections.header(it)}" },
+      sampled_from(["", " ", "\t", "\r"]),
+      from_regex('[^\n]{0,12}', fullmatch: true),
+    )
+  end
+
+  # Whatever a person left in the note, reading it once settles it:
+  # the value the split's reading joins back into reads the same way
+  # again, so a save followed by a serve followed by a save is not a
+  # drift.
+  def test_a_split_is_settled_by_one_reading
+    Hegel.test(test_cases: 1_000) do |tc|
+      in_play = tc.draw(labels.filter(&:any?))
+      value = tc.draw(arrays(edited_line(in_play), max_size: 10)).join("\n")
+      read = split(value, in_play)
+
+      assert_equal read, split(ProTacts::NoteSections.join(read.member, read.sections), in_play)
+    end
+  end
 end
diff --git a/test/pro_tacts/test_store.rb b/test/pro_tacts/test_store.rb
index 8ecf9eb..38da5ec 100644
--- a/test/pro_tacts/test_store.rb
+++ b/test/pro_tacts/test_store.rb
@@ -2,9 +2,11 @@ require_relative "../test_helper"
 require_relative "../photo_card"
 
 require "digest"
+require "fileutils"
 require "pathname"
 require "tmpdir"
 
+require "hegel"
 require "sequel"
 
 require "pro_tacts/store"
@@ -2503,6 +2505,105 @@ class StoreTest < Minitest::Test
     end
   end
 
+  ## The change log, driven
+
+  # Clients' writes and the admin's in any order, against the two
+  # promises the change log makes (Store's class comment, and #put):
+  # a client holding any token it was ever handed catches up to the
+  # book by applying what #changes hands it, and a card's history,
+  # its diffs replayed oldest first, rebuilds the card it ends in.
+  class ChangeLogMachine < Hegel::StateMachine
+    # A few ids, so writes land on cards that exist as often as not.
+    IDS = %w[ada bob cy].freeze #: Array[String]
+
+    def initialize(store, tc)
+      @store = store
+      # A token with the book its client held when it took it: the
+      # first is a client that has never synced.
+      @tokens = Hegel::Stateful::Pool.new(tc)
+      @tokens.add([0, {}])
+    end
+
+    # A card a write might carry: any name, and a TEL or two that may
+    # repeat, which a diff counts rather than sets. Any name but one
+    # holding a NUL, which no write survives today: Sequel writes the
+    # card into its INSERT as a literal, SQLite's tokenizer stops at the
+    # NUL, and the write raises with the card's bytes in its message.
+    # That is the store's open question, not this machine's.
+    def card(tc, id)
+      name = ProTacts::VCard.escape(tc.draw(text(max_size: 10, min_codepoint: 1)))
+      phones = tc.draw(arrays(sampled_from(["TEL:+1 555 0100\r\n", "TEL:+1 555 0199\r\n"]), max_size: 3))
+      ProTacts::VCard.new("BEGIN:VCARD\r\nVERSION:3.0\r\nFN:#{name}\r\n#{phones.join}UID:#{id}\r\nEND:VCARD\r\n")
+    end
+
+    # What a client downloading the whole book now would hold: each
+    # card's etag, by id.
+    def book = @store.contacts.to_h { [it.id, it.etag] }
+
+    rule(:put) do |tc|
+      id = tc.draw(sampled_from(IDS))
+      @store.put(id, card(tc, id), client: tc.draw(booleans))
+    end
+
+    rule(:edit) do |tc|
+      id = tc.draw(sampled_from(IDS))
+      tc.assume(@store.contact(id))
+      @store.save_edit(id, card(tc, id), birthday: nil)
+    end
+
+    rule(:delete) do |tc|
+      @store.delete(tc.draw(sampled_from(IDS)))
+    end
+
+    rule(:sync) do
+      @tokens.add([@store.latest_sequence, book])
+    end
+
+    # A client's sync-collection report (RFC 6578 section 3.2): the
+    # entries after its token, applied in order to what it held.
+    rule(:catch_up) do |tc|
+      sequence, held = tc.draw(@tokens.values_reusable)
+      caught_up = @store.changes(after: sequence).each_with_object(held.dup) { |change, cards|
+        if change.action == ProTacts::Store::Action::DELETE
+          cards.delete(change.card_id)
+        else
+          cards[change.card_id] = change.etag
+        end
+      }
+      raise "a client at #{sequence} caught up to #{caught_up}, not #{book}" unless caught_up == book
+    end
+
+    rule(:read_history) do |tc|
+      id = tc.draw(sampled_from(IDS))
+      rebuilt = Hash.new(0)
+      @store.changes_of(id).reverse_each do |change|
+        change.diff.removed.each { rebuilt[it] -= 1 }
+        change.diff.added.each { rebuilt[it] += 1 }
+      end
+      lines = @store.contact(id)&.vcard&.lines&.map(&:content)&.reject(&:empty?) || []
+      raise "#{id}'s history rebuilds #{rebuilt}, not #{lines}" unless rebuilt.reject { |_, count| count.zero? } == lines.tally
+    end
+
+    invariant(:the_ctag_is_the_last_entry) do
+      raise "the ctag is #{@store.ctag}" unless @store.ctag == (@store.changes.last&.sequence || 0).to_s
+    end
+  end
+
+  # Each run starts from a copy of one migrated database rather than
+  # migrating its own, which is most of what opening a store costs.
+  def test_the_change_log_keeps_its_promises_whatever_the_writes
+    Dir.mktmpdir do |dir|
+      template = Pathname.new(dir) / "template.db"
+      ProTacts::Store.connect(template) {}
+      runs = 0
+      Hegel.test(test_cases: 100, stateful_step_count: 20) do |tc|
+        path = Pathname.new(dir) / "#{runs += 1}.db"
+        FileUtils.cp(template, path)
+        ProTacts::Store.connect(path) { |store| Hegel::Stateful.run(ChangeLogMachine.new(store, tc), tc) }
+      end
+    end
+  end
+
   private
 
   # A store whose change-log write fails, after Store#put has already put
diff --git a/test/pro_tacts/test_sync_token.rb b/test/pro_tacts/test_sync_token.rb
index 02eed48..0e11d18 100644
--- a/test/pro_tacts/test_sync_token.rb
+++ b/test/pro_tacts/test_sync_token.rb
@@ -1,8 +1,12 @@
 require_relative "../test_helper"
 
+require "hegel"
+
 require "pro_tacts/sync_token"
 
 class SyncTokenTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   BOOK = ProTacts::SyncToken.book("alpha@example.com")
   DATABASE = "0f1e2d3c4b5a6978" #: String
 
@@ -46,4 +50,33 @@ class SyncTokenTest < Minitest::Test
     assert_match(/\A[0-9a-f]{16}\z/, BOOK)
     refute_equal BOOK, ProTacts::SyncToken.book("zed@example.com")
   end
+
+  ## Property tests
+
+  def database_id = from_regex("[0-9a-f]{16}", fullmatch: true)
+
+  # Any sequence a book's ctag reaches, minted for any login's book on
+  # any database, reads back as that sequence there.
+  def test_any_minted_token_reads_back_as_its_sequence
+    Hegel.test(test_cases: 1_000) do |tc|
+      sequence = tc.draw(integers(min_value: 0))
+      book = ProTacts::SyncToken.book(tc.draw(text))
+      database = tc.draw(database_id)
+
+      assert_equal sequence, ProTacts::SyncToken.read(ProTacts::SyncToken.mint(sequence.to_s, book, database), book, database)
+    end
+  end
+
+  # And reads as nothing anywhere else: on another book or another
+  # database, a token is one this server never minted for it.
+  def test_a_token_reads_as_nothing_off_the_book_and_database_that_minted_it
+    Hegel.test(test_cases: 1_000) do |tc|
+      sequence = tc.draw(integers(min_value: 0)).to_s
+      minted_for = [ProTacts::SyncToken.book(tc.draw(text)), tc.draw(database_id)]
+      read_on = [ProTacts::SyncToken.book(tc.draw(text)), tc.draw(database_id)]
+      tc.assume(minted_for != read_on)
+
+      assert_nil ProTacts::SyncToken.read(ProTacts::SyncToken.mint(sequence, *minted_for), *read_on)
+    end
+  end
 end
diff --git a/test/pro_tacts/vcard/test_lines.rb b/test/pro_tacts/vcard/test_lines.rb
index c735519..46c084e 100644
--- a/test/pro_tacts/vcard/test_lines.rb
+++ b/test/pro_tacts/vcard/test_lines.rb
@@ -2,10 +2,14 @@ require_relative "../../test_helper"
 
 require "digest"
 
+require "hegel"
+
 require "pro_tacts/vcard"
 require "pro_tacts/vcard/parser"
 
 class VCardLinesTest < Minitest::Test
+  include Hegel::Syntax::Methods
+
   VCARD = ProTacts::VCard
   CARD = "BEGIN:VCARD\r\nVERSION:3.0\r\nFN:Ada\r\nUID:ada\r\nEND:VCARD\r\n"
 
@@ -313,4 +317,103 @@ class VCardLinesTest < Minitest::Test
   def test_insert_with_nothing_leaves_the_card_alone
     assert_equal CARD, VCARD.new(CARD).insert([]).to_s
   end
+
+  ## Property tests
+
+  # The names the cards below are made of. X-TEL is the near miss a
+  # name match has to tell apart from TEL, and item1.TEL the group
+  # prefix it has to see through.
+  NAMES = %w[FN NOTE TEL item1.TEL X-TEL EMAIL].freeze #: Array[String]
+
+  # The names an edit asks after: BDAY is one no card below carries,
+  # #insert's case.
+  ASKED = %w[FN NOTE TEL EMAIL BDAY].freeze #: Array[String]
+
+  # A card as a client might send it: an envelope around content lines
+  # in either line-break convention, some folded, some that will not
+  # read, and an END that may close the bytes with no terminator.
+  def any_card
+    composite { |dtc|
+      body = dtc.draw(arrays(content_line, max_size: 8))
+      last = dtc.draw(sampled_from(["\r\n", "\n", ""]))
+      ProTacts::VCard.new("BEGIN:VCARD\r\nVERSION:3.0\r\n#{body.join}END:VCARD#{last}")
+    }
+  end
+
+  def content_line
+    composite { |dtc|
+      terminator = dtc.draw(sampled_from(["\r\n", "\n"]))
+      value = dtc.draw(from_regex('[^\r\n]{0,12}', fullmatch: true))
+      fold = dtc.draw(integers(min_value: 0, max_value: value.length))
+      folded = fold.zero? ? value : value.dup.insert(fold, "#{terminator} ")
+      dtc.draw(booleans(p: 0.1)) ? "garbage#{terminator}" : "#{dtc.draw(sampled_from(NAMES))}:#{folded}#{terminator}"
+    }
+  end
+
+  # Lines an edit hands in, bare or terminated, each naming `name`.
+  def edit_lines(name)
+    line = tuples(from_regex('[^\r\n]{0,12}', fullmatch: true), sampled_from(["", "\r\n", "\n"]))
+    arrays(line, max_size: 3).map { |lines| lines.map { |value, terminator| "#{name}:#{value}#{terminator}" } }
+  end
+
+  def first_named(card, name) = card.lines.index { it.names?(name) }
+
+  def reading(lines) = lines.map { [it.property, it.verbatim, it.error.class] }
+
+  # #extract hands the remainder back already read (VCard.of), on the
+  # promise that its bytes read as those same lines: no split leaves a
+  # continuation stranded or a terminator missing.
+  def test_an_extracted_remainder_reads_as_the_lines_it_was_made_of
+    Hegel.test(test_cases: 1_000) do |tc|
+      card = tc.draw(any_card)
+      _, rest = card.extract(tc.draw(sampled_from(ASKED)))
+
+      assert_equal reading(rest.lines), reading(ProTacts::VCard.new(rest.to_s).lines)
+    end
+  end
+
+  # #replace touches the named lines and no others: with them taken
+  # out again, the card is the one the original leaves when they are
+  # taken out of it, byte for byte, and what was taken is the lines
+  # handed in — present or absent before, folded or not.
+  def test_replace_changes_the_named_lines_and_no_others
+    Hegel.test(test_cases: 1_000) do |tc|
+      card = tc.draw(any_card)
+      name = tc.draw(sampled_from(ASKED))
+      lines = tc.draw(edit_lines(name))
+      taken, rest = card.replace(name, lines).extract(name)
+
+      assert_equal [lines.map(&:chomp), card.extract(name).last.to_s], [taken.map(&:content), rest.to_s]
+    end
+  end
+
+  # In place: the replacement starts where the first line it replaces
+  # stood, not at the card's end.
+  def test_replace_lands_where_the_first_named_line_stood
+    Hegel.test(test_cases: 1_000) do |tc|
+      card = tc.draw(any_card)
+      name = tc.draw(sampled_from(NAMES.grep_v(/[-.]/)))
+      tc.assume(card.lines.any? { it.names?(name) })
+      lines = tc.draw(edit_lines(name).filter(&:any?))
+
+      assert_equal first_named(card, name), first_named(card.replace(name, lines), name)
+    end
+  end
+
+  # #substitute swaps the first line whose bytes the digest names and
+  # no other: every line around it keeps its bytes and its place, and
+  # the card's bytes read as exactly that.
+  def test_substitute_swaps_the_addressed_line_and_keeps_the_rest
+    Hegel.test(test_cases: 1_000) do |tc|
+      card = tc.draw(any_card)
+      before = card.lines.map(&:verbatim)
+      addressed = card.lines.fetch(tc.draw(integers(min_value: 0, max_value: before.length - 1)))
+      lines = tc.draw(edit_lines(tc.draw(sampled_from(NAMES))))
+
+      at = before.index(addressed.verbatim)
+      terminator = addressed.verbatim[/\r?\n\z/] || "\r\n"
+      expected = [*before.take(at), *lines.map { it.end_with?("\n") ? it : it + terminator }, *before.drop(at + 1)]
+      assert_equal expected, card.substitute(addressed.digest, lines).lines.map(&:verbatim)
+    end
+  end
 end
diff --git a/test/pro_tacts/vcard/test_parser.rb b/test/pro_tacts/vcard/test_parser.rb
index 8ad9a40..a34f7e3 100644
--- a/test/pro_tacts/vcard/test_parser.rb
+++ b/test/pro_tacts/vcard/test_parser.rb
@@ -383,6 +383,46 @@ class VCardParserTest < Minitest::Test
     end
   end
 
+  # Fragments a card is made of, the line breaks and the grammar's
+  # punctuation among them, joined in any order: the inputs a draw
+  # from all of Unicode almost never assembles into something
+  # card-shaped enough to reach a fold or a bare CR.
+  FRAGMENTS = ["BEGIN:VCARD", "END:VCARD", "item1.", "TEL", "x", ":", ";", "=", ",", "\"", ".",
+               "\r\n", "\n", "\r", " ", "\t", "é"].freeze #: Array[String]
+
+  # No read raises on a card's behalf: whatever the bytes, the walk
+  # comes back as lines, and between them they hold every byte, in
+  # order — the guarantee behind serving a card from its bytes however
+  # it reads.
+  def test_any_text_walks_into_lines_that_rejoin_as_it
+    card_like = arrays(sampled_from(FRAGMENTS), max_size: 40).map(&:join)
+    Hegel.test(test_cases: 1_000) do |tc|
+      card = tc.draw(one_of(text(max_size: 200), card_like))
+
+      assert_equal card, lines(card).map(&:verbatim).join
+    end
+  end
+
+  # RFC 2426 section 2.6 puts no constraint on where a fold lands, mid-
+  # token and mid-escape included, so a content line folded between
+  # any of its characters reads as the line unfolded.
+  def test_a_fold_anywhere_reads_as_the_line_unfolded
+    token = from_regex("[A-Za-z0-9-]{1,8}", fullmatch: true)
+    line = composite { |dtc|
+      parameters = dtc.draw(arrays(tuples(token, from_regex('[^\x00-\x1f\x7f";:,]{0,8}', fullmatch: true)), max_size: 3))
+      value = dtc.draw(from_regex('[^\r\n]{0,40}', fullmatch: true))
+      "#{dtc.draw(token)}#{parameters.map { |name, setting| ";#{name}=#{setting}" }.join}:#{value}"
+    }
+    Hegel.test(test_cases: 1_000) do |tc|
+      unfolded = tc.draw(line)
+      cuts = tc.draw(sets(integers(min_value: 1, max_value: unfolded.length - 1))) if unfolded.length > 1
+      fold = tc.draw(sampled_from(["\r\n ", "\r\n\t", "\n "]))
+      folded = unfolded.chars.each_with_index.map { |char, index| cuts&.include?(index) ? "#{fold}#{char}" : char }.join
+
+      assert_equal properties("#{unfolded}\r\n"), properties("#{folded}\r\n")
+    end
+  end
+
   # One value, two readings, and only the caller knows which its property
   # wants: N is structured, so the escaped "\;" is a character inside a
   # component — read as text it comes back spelled like the separator