dhtable_mateo.ath

load "htable.ath"
load "dlls.ath"
load "dpair.ath"
# ll := Location List; hf := hash function; rv := replicate value; htl := hash table location
structure (DHTable S) := (dht_empty  ll:(Lst Location) hf:(fn S N) rv:N htl:Location) |
                         (dht_insert (DHTable S) S)

datatype (DHTRep S) := (dhtr hf:(fn S N) rv:N htl:Location buckets:(DLst (Lst S)))
# rv must always be > 0


module DHTable {

	define [initDPrList insertDPrList available_key in no_consecutive_failures] :=
	       [DL_L_S.initDPrList DL_L_S.insertDPrList
		    DL_L_S.available_key DL_L_S.in
		    DL_L_S.no_consecutive_failures]

	assert dht_st_axioms := (structure-axioms "DHTable")

	# Each of this asserts gives axioms for each of the selectors of both data types
	assert dht_se_axioms := (selector-axioms "DHTable")
	assert dhtr_se_axioms := (selector-axioms "DHTable")

	define [s s0] := [?s:(Set.Set 'S) ?s0:(Set.Set 'S)]
	define [dht_no_conf dht_no_junk] := dht_st_axioms
	define [v v0 v2]     := [?v:'S ?v0:'S ?v2:'S]
	define [rv rv1 n m]  := [?rv:N ?rv1:N ?n:N ?m:N]
	define [dht dht0 dht1]    := [?dht:(DHTable 'S) ?dht0:(DHTable 'S)  ?dht1:(DHTable 'S) ]
	define [ll ll1]      := [?ll:(Lst Location) ?ll1:(Lst Location)]
	define [htl htl1 l0 l1] := [?htl:Location ?htl1:Location ?l0:Location ?l1:Location]
	define [hf hf1 f g]     := [?hf:(fn 'S N) ?hf1:(fn 'S N) ?f:(fn 'S N) ?g:(fn 'S N)]
	define [dlls dlls3 dlls0 dlls1] := [?dlls:(DLst (Lst 'S)) ?dlls:(DLst (Lst 'S)) ?dlls0:(DLst (Lst 'S)) ?dlls1:(DLst (Lst 'S))]

	assert* dhtr_no_conf :=
	(
		((dhtr f n l0 dlls0) =  (dhtr g m l1 dlls1))
		<==>
		((f = g) & (n = m) & (l0 = l1) & (dlls0 = dlls1))
	)

	### rep
	### Purpose:
	###     Extract the internal distributed representation of a distributed hash table.
	###     This function expands the abstract DHTable structure into its operational form,
	###     consisting of the hash function, replication factor, home table location, and
	###     the distributed list of buckets.
	###
	### Parameters:
	###     dht::(DHTable S) : A distributed hash table.
	###
	### Returns:
	###     A value of type (DHTRep S), constructed as:
	###         dhtr hf rv htl dlls
	###     where:
	###       - hf   : hash function stored in the table
	###       - rv   : replication value (>0)
	###       - htl  : base location of the table
	###       - dlls : distributed list of buckets, initialized with
	###               initDPrList for empty tables, or updated using
	###               insertDPrList when inserting a value v into the
	###               bucket at position (hf at v).
	###
	# TODO: may be here we can ensure that rv>0...
	declare rep : (S) [(DHTable S)] -> (DHTRep S)	       
	assert rep_axioms :=
		(fun [
			(rep (dht_empty ll hf rv htl)) = (dhtr hf rv htl (initDPrList hf htl ll))
			(rep (dht_insert dht v)) = [(dhtr hf rv htl (insertDPrList (hf at v) rv v dlls))
						when ((rep dht) = (dhtr hf rv htl dlls))]
		])

	define rep_e :=
		(forall dht . exists hf rv htl dlls .
			((rep dht) = (dhtr hf rv htl dlls))
		)

	by-induction rep_e {
		(dht as (dht_empty ll1 hf1 rv1 htl1)) =>
			let {
				empty_dpr_list   := (initDPrList hf1 htl1 ll1);
				rep_dt := (!chain [
					(rep dht)
					= (dhtr hf1 rv1 htl1 empty_dpr_list) [rep_axioms] ])}
			(!egen* (exists hf rv htl dlls . ((rep dht) = (dhtr hf rv htl dlls))) 
					[hf1 rv1 htl1 empty_dpr_list])
		| (dht as (dht_insert dht1 v)) =>
			let { 
				ih := (exists hf1 rv1 htl1 dlls3 . ((rep dht1) = (dhtr hf1 rv1 htl1 dlls3)))
			}
			pick-witnesses hf2 rv2 htl2 dlls2 for ih rep_dt_def
			let {
				insert_dpr_list := (insertDPrList (hf2 at v) rv2 v dlls2);
				rep_dt := (!chain<- [
					((rep (dht_insert dht1 v)) = (dhtr hf2 rv2 htl2 insert_dpr_list))
					<== rep_dt_def   [rep_axioms]
				])
			}
			(!egen* (exists hf rv htl dlls . ((rep dht) = (dhtr hf rv htl dlls))) 
					[hf2 rv2 htl2 insert_dpr_list])
	}
	# TODO: You need a correctness theorem for the value and its replica, i.e., each
	# insertion in the dht must have the value and the value replicated rv number of times
	# in the valid buckets

	### available (constructor-recursive on DHTable)
	### Purpose:
	###     A distributed hash table is "available" when every value it actually
	###     stores can be queried successfully — i.e. the bucket window for each
	###     inserted value is alive. Stated constructor-recursively over the
	###     DHTable shape:
	###
	###       * an empty DHT has noestored values, so it is trivially available;
	###       * (dht_insert dht v) is available iff dht is and the bucket window
	###         where v was just placed is alive.
	###
	###     This replaces the previous formulation
	###         (available_aux (dhtr hf rv htl dlls)) <==>
	###             (forall v . available_key (hf at v) rv dlls dlls)
	###     which quantified over the entire carrier 'S. For an infinite 'S
	###     (e.g. N) that was effectively "every bucket is rv-safe" and
	###     strictly stronger than what query_functional_correctness needs.
	###     The new form makes both branches of the QFC induction
	###     carry useful information: the empty branch is trivially available,
	###     the insert branch hands us `available_key` on the freshly inserted
	###     bucket directly. The intermediate predicate `available_aux` (which
	###     lifted the bad characterization to DHTRep) is dropped — every use
	###     site folded through it back to `available` anyway.
	###
	### Returns:
	###     Boolean.
	declare available : (S) [(DHTable S)] -> Boolean
	assert available_axioms := (fun [
		(available (dht_empty ll hf rv htl)) <==> true
		(available (dht_insert dht v)) <==> [
			((available dht) & (available_key (hf at v) rv dlls dlls))
				when ((rep dht) = (dhtr hf rv htl dlls))
		]
	])

	### query / query_aux
	### Purpose:
	###     Perform a lookup operation on a distributed hash table. The function
	###		`query_aux` executes the lookup over the internal representation (DHTRep),
	###		while `query` is the  public version that first expands the DHTable using
	###     `rep` and then delegates to `query_aux`.
	###
	### Returns:
	###     Option Boolean:
	###         SOME b     when the key v is located in one of the
	###                    available buckets or replicas. The boolean
	###                    b indicates whether v is present.
	###         NONE       when the lookup cannot be completed because
	###                    the relevant bucket and its replicas are not
	###                    available.
	###
	declare query_aux : (S) [(DHTRep S) S] -> (Option Boolean)
	assert query_aux_axioms :=
		(fun [(query_aux (dhtr hf rv htl dlls) v) = [
			(SOME (in (hf at v) rv dlls dlls v) )
						when (available_key (hf at v) rv dlls dlls)
			NONE 
						when (~ available_key (hf at v) rv dlls dlls)
			]]
		)
	declare query : (S) [(DHTable S) S] -> (Option Boolean)
	assert* query_axiom := ((query dht v) = (query_aux (rep dht) v))

	
	# After the `available` change above, `available (dht_empty ll hf rv htl) <==> true`, so
	# the old `available` antecedent no longer constrains bucket aliveness on
	# its own. The theorem is restated with the relevant `available_key`
	# hypothesis spelled out directly. Under the old `available_aux_axiom` the
	# two forms were equivalent (the old axiom would have let you derive this
	# hypothesis from `available`); under the new constructor-recursive
	# `available`, the direct form is the provable one.
	define query_fc_empty :=
	(forall ll hf rv htl v .
		((available_key (hf at v) rv (initDPrList hf htl ll) (initDPrList hf htl ll)) ==>
		  ((query (dht_empty ll hf rv htl) v) = (SOME false))))

	# The old `force` step bridging
	#   (in … (…) v) <==> false      (what in_init_false gives us)
	# to
	#   (in … (…) v) =  false        (what `query = (SOME false)` needs under SOME)
	# is now done by chaining iff → (~ p) → (p = false) via `false-bool` from bool.ath.
	pick-any ll hf rv htl v
		assume availableKey :=
			(available_key (hf at v) rv (initDPrList hf htl ll) (initDPrList hf htl ll))
		let {
			# in_init_false instantiated at our query's bucket and rep witnesses:
			#   (in (hf at v) rv (initDPrList hf htl ll) (initDPrList hf htl ll) v) <==> false
			p_iff_false := (!uspec* in_init_false
									[(hf at v) rv ll hf v htl]);
			# Iff with `false` is propositionally equivalent to negation.
			not_p := (!chain-> [
						p_iff_false
						==> (~ (in (hf at v) rv (initDPrList hf htl ll) (initDPrList hf htl ll) v))
							[prop-taut]
					]);
			# bool.ath's false-bool turns (~ p) into the term equality (p = false),
			# closing the gap that previously forced `force`.
			p_eq_false := (!false-bool not_p);
			query_some :=
				(!chain [
					(query (dht_empty ll hf rv htl) v)
					= (query_aux (rep (dht_empty ll hf rv htl)) v) [query_axiom]
					= (query_aux (dhtr hf rv htl (initDPrList hf htl ll)) v) [rep_axioms]
					= (SOME (in (hf at v) rv (initDPrList hf htl ll) (initDPrList hf htl ll) v)) [query_aux_axioms]
				])
			}
			(!chain [
				(query (dht_empty ll hf rv htl) v)
				= (SOME (in (hf at v) rv (initDPrList hf htl ll) (initDPrList hf htl ll) v)) [query_some]
				= (SOME false)                                                                [p_eq_false]
			])
	
	define [b0 b1] := [?b0:Boolean ?b1:Boolean]

	# define query_fc_insert :=
	# 	(forall dht v0 v1 . (available (dht_insert dht v0)) ==>
	# 		exists b0 b1 . (
	# 			((query (dht_insert dht v0) v1) = (SOME b0)) &
	# 			((query dht v1) = (SOME b1)) &
	# 			(b0 <==> ((v0 = v1) | b1))
	# 		))
	### query_functional_correctness (TODO — asserted, not yet proved)
	###
	### After the `available` change above, `available dht` no longer guarantees
	### bucket-aliveness for arbitrary v. The theorem now takes the relevant
	### `available_key` fact as an explicit per-v hypothesis (the same change
	### we already made to query_fc_empty), and pulls the rep witnesses
	### (hf rv htl dlls) into the outer forall so they're in scope for both
	### the hypothesis and the empty-disjunct's existential.
	###
	### Proof obligation (deferred):
	###   * Empty branch (dht = dht_empty ll hf rv htl): follows from
	###     query_fc_empty using the available_key hypothesis directly.
	###   * Insert branch (dht = dht_insert dt v0):
	###       - case v = v0: needs in_after_insert_self at an arbitrary
	###         bucket. Only the bucket=0 case is proven, in dlls.ath:630;
	###         see the status block at dlls.ath:668-701 for the missing
	###         size / `<` infrastructure.
	###       - case v ≠ v0: needs in_after_insert_other — currently
	###         asserted as a TODO in dlls.ath:720.
	###       - either case: available_key_insert_invariant is proven
	###         (dlls.ath:776), modulo its asserted intermediate
	###         available_key_dlls_locs_inv.
	### Direct induction on dht is the cleaner path; Carlos's canonical /
	### ht-equiv bridge does not lift to rv+1-fold replication (no bijection
	### between DHTable and HTable when each value lives in many buckets).
	# TODO: discharge by induction on dht once in_after_insert_self is proven
	# for an arbitrary bucket and in_after_insert_other is upgraded from an
	# asserted conjecture to a proven theorem.
	define query_functional_correctness :=
		(forall dht v hf rv htl dlls .
			(rep dht = (dhtr hf rv htl dlls) &
			 (available dht) &
			 (available_key (hf at v) rv dlls dlls))
			==>
			(
				(exists ll . (dht = (dht_empty ll hf rv htl) &
				              (query dht v) = (SOME false)))
				| (exists dht0 v0 b b0 . (
						dht = (dht_insert dht0 v0) &
						(query dht v)  = (SOME b) &
						(query dht0 v) = (SOME b0) &
						(b <==> ((v = v0) | b0))))
			))
	assert query_functional_correctness


	declare values_aux : (S) [(DHTRep S)]  -> (Option (Set.Set S))
	assert* values_aux_axioms := 
			((values_aux (dhtr hf rv htl dlls)) = (DL_L_S.values dlls Set.null true))
	declare values : 	 (S) [(DHTable S)] -> (Option (Set.Set S))
	assert* values_axiom := ((values dht) = (values_aux (rep dht)))

	# Empty-DHT case (PROVEN): an empty DHT is `available`, and `values` on it
	# returns SOME Set.null (never NONE), because the public boundary always
	# uses the `true` flag and every freshly-initialized bucket contributes
	# the empty set (DL_L_S.values_init_some).
	define values_fc_empty :=
		(forall ll hf rv htl . (values (dht_empty ll hf rv htl)) = (SOME Set.null))
	conclude values_fc_empty
		pick-any ll:(Lst Location) hf:(fn 'S N) rv:N htl:Location
			let { init_some := (!uspec* DL_L_S.values_init_some
									[ll hf htl (Set.null:(Set.Set 'S))]) }
			(!chain [ (values (dht_empty ll hf rv htl))
					= (values_aux (rep (dht_empty ll hf rv htl)))              [values_axiom]
					= (values_aux (dhtr hf rv htl (initDPrList hf htl ll)))    [rep_axioms]
					= (DL_L_S.values (initDPrList hf htl ll) Set.null true)    [values_aux_axioms]
					= (SOME Set.null)                                          [init_some] ])


	# Insert-DHT case. The value set after inserting v0 is exactly Set.insert v0
	# of the value set before. Reduces, through rep/values_aux, to the single
	# remaining list-level obligation DL_L_S.values_after_insert; the pre-insert
	# value set is furnished by the PROVEN DL_L_S.values_true_some, and the live
	# window by `available` on the freshly inserted bucket.
	define values_fc_insert :=
		(forall dht0 v0 . (available (dht_insert dht0 v0)) ==>
			exists s s0 . ((values (dht_insert dht0 v0)) = (SOME s) &
			               (values dht0) = (SOME s0) &
			               (s = (Set.insert v0 s0))))
	conclude values_fc_insert
		pick-any dht0:(DHTable 'S) v0:'S
			assume avail := (available (dht_insert dht0 v0))
				let { rep0 := (!uspec rep_e dht0) }
				pick-witnesses hf rv htl dlls for rep0 rep0_def
				let {
					tot := (!uspec* DL_L_S.values_true_some
									[dlls (Set.null:(Set.Set 'S))]) }
				pick-witness s0 for tot tot_def
				let {
					vals0_some := (!chain
						[ (values dht0)
						= (values_aux (rep dht0))              [values_axiom]
						= (values_aux (dhtr hf rv htl dlls))   [rep0_def]
						= (DL_L_S.values dlls Set.null true)   [values_aux_axioms]
						= (SOME s0)                            [tot_def] ]);
					av_iff := (!chain->
						[ rep0_def
						==> ((available (dht_insert dht0 v0)) <==>
						     ((available dht0) & (available_key (hf at v0) rv dlls dlls)))
								[available_axioms] ]);
					availkey := (!chain->
						[ (!both avail av_iff)
						==> (available_key (hf at v0) rv dlls dlls) [prop-taut] ]);
					avf := (!uspec* DL_L_S.values_after_insert
									[(hf at v0) rv v0 dlls s0]);
					after := (!mp avf (!both availkey tot_def));
					vals_ins := (!chain
						[ (values (dht_insert dht0 v0))
						= (values_aux (rep (dht_insert dht0 v0)))                            [values_axiom]
						= (values_aux (dhtr hf rv htl (insertDPrList (hf at v0) rv v0 dlls))) [rep_axioms]
						= (DL_L_S.values (insertDPrList (hf at v0) rv v0 dlls) Set.null true) [values_aux_axioms]
						= (SOME (Set.insert v0 s0))                                          [after] ]);
					conj := (!both vals_ins
								(!both vals0_some (!reflex (Set.insert v0 s0)))) }
				(!egen* (exists s s0 . ((values (dht_insert dht0 v0)) = (SOME s) &
				                        (values dht0) = (SOME s0) &
				                        (s = (Set.insert v0 s0))))
						[(Set.insert v0 s0) s0])


	# values_functional_correctness is now a real datatype-cases proof (was a bare
	# `assert`). Its empty branch is fully proven (values_fc_empty); its insert
	# branch is proven modulo the single list-level lemma DL_L_S.values_after_insert.
	define values_functional_correctness :=
		(forall dht . (available dht ==>
				(exists ll hf rv htl .
						(dht = (dht_empty ll hf rv htl) &
								(values dht) = (SOME Set.null)))
				| (exists dht0 v0 s s0 . (
							dht = (dht_insert dht0 v0) &
							(values dht) = (SOME s) &
							(values dht0) = (SOME s0) &
							(s = (Set.insert v0 s0))))))
	datatype-cases values_functional_correctness {
		(dht as (dht_empty ll1 hf1 rv1 htl1)) =>
			assume avail := (available (dht_empty ll1 hf1 rv1 htl1))
				let {
					emp := (!instance values_fc_empty [ll1 hf1 rv1 htl1]);
					left := (!chain->
						[ emp
						==> (((dht_empty ll1 hf1 rv1 htl1) = (dht_empty ll1 hf1 rv1 htl1)) &
						     ((values (dht_empty ll1 hf1 rv1 htl1)) = (SOME Set.null)))
							[augment] ]) }
				(!either
					(!egen* (exists ll hf rv htl .
								((dht_empty ll1 hf1 rv1 htl1) = (dht_empty ll hf rv htl) &
								 (values (dht_empty ll1 hf1 rv1 htl1)) = (SOME Set.null)))
							[ll1 hf1 rv1 htl1])
					(exists dht0 v0 s s0 . (
							(dht_empty ll1 hf1 rv1 htl1) = (dht_insert dht0 v0) &
							(values (dht_empty ll1 hf1 rv1 htl1)) = (SOME s) &
							(values dht0) = (SOME s0) &
							(s = (Set.insert v0 s0)))))
	  | (dht as (dht_insert dht0 v0)) =>
			assume avail := (available (dht_insert dht0 v0))
				let { ins := (!mp (!instance values_fc_insert [dht0 v0]) avail) }
				pick-witnesses sw sw0 for ins ins_def
				let { full := (!both (!reflex (dht_insert dht0 v0)) ins_def) }
				(!either
					(exists ll hf rv htl .
						((dht_insert dht0 v0) = (dht_empty ll hf rv htl) &
						 (values (dht_insert dht0 v0)) = (SOME Set.null)))
					(!egen* (exists dht1 v1 s s0 . (
								(dht_insert dht0 v0) = (dht_insert dht1 v1) &
								(values (dht_insert dht0 v0)) = (SOME s) &
								(values dht1) = (SOME s0) &
								(s = (Set.insert v1 s0))))
							[dht0 v0 sw sw0]))
	}

	define dht_functional_correctness :=
		(forall dht v . (available dht ==>
			(exists ll hf rv htl .
				(dht = (dht_empty ll hf rv htl) &
				((query dht v) = (SOME false)) &
				(values dht = (SOME Set.null)) )) |
			(exists dht0 v0 b b0 s s0 .
				(dht = (dht_insert dht0 v0) &
				((query dht v)  = (SOME b) &
				(query dht0 v) = (SOME b0) &
				(b <==> ((v = v0) | b0))) &
				((values dht) = (SOME s) &
				(values dht0) = (SOME s0) &
				(s = (Set.insert v0 s0))))
			)))
				# & (hf dht = hf dht0)
	# Asserted (paper cites this sentence in Section III-D; full deduction deferred).
	assert dht_functional_correctness


	### dht_replication_correctness  (asserted — formal statement of the
	### abstract's replication claim)
	###
	### Paper claim (abstract): "as long as no `r` consecutive bucket
	### locations fail — with a replication value `r` — all the DHT
	### key-value pairs remain available." Concretely: if the bucket
	### list `dlls` underlying the DHT satisfies
	###   `no_consecutive_failures rv dlls dlls`
	### then `available dht` holds, so every inserted key passes the
	### per-key `available_key` precondition demanded by
	### `query_functional_correctness`.
	###
	### The `~ (dlls = (dempty htl))` precondition rules out the
	### degenerate case `(dht_empty empty hf rv htl)` (initialized with
	### an empty location list): there `dlls = (dempty htl)`,
	### `no_consecutive_failures` is vacuously true (no positions to
	### start a window from), but `available_key` returns false
	### unconditionally on a `dempty` o_dlls (`available_key_axioms`
	### first clause), so a `dht_insert` on top would be unavailable
	### even though the replication invariant trivially holds.
	###
	### Proof obligation (deferred):
	###   * Empty branch (dht = dht_empty ll hf rv htl): `available`
	###     evaluates to `true` directly via the first available_axiom.
	###   * Insert branch (dht = dht_insert dht0 v0): unfold `available`
	###     into the conjunction
	###         (available dht0) & (available_key (hf at v0) rv dlls dlls).
	###     (i) `available dht0` follows from the IH after translating
	###         the `no_consecutive_failures` hypothesis from the
	###         post-insert dlls back to the pre-insert dlls through
	###         `insertDPrList_preserves_locs` (dlls.ath:284) and
	###         `available_key_dlls_locs_inv` (dlls.ath:789) — both
	###         predicates depend on dlls only through its
	###         head-location projection `dlls_locs`.
	###     (ii) `available_key (hf at v0) rv dlls dlls` follows from a
	###         bucket-lookup lemma derived by induction on the bucket
	###         index from `no_consecutive_failures`: every starting
	###         position yields an alive window, so the specific
	###         position `(hf at v0)` does too.
	###
	###     The lookup lemma is the natural intermediate:
	###         forall bucket rv dlls .
	###             (~ (dlls = (dempty htl))) &
	###             (no_consecutive_failures rv dlls dlls)
	###             ==> (available_key bucket rv dlls dlls)
	###     proved by induction on (bucket, dlls). It is *not* declared
	###     here so the assumption base stays minimal; add it as a
	###     proved lemma when discharging this theorem.
	### Auxiliary lemma (ASSERTED): `no_consecutive_failures` is invariant
	### under `insertDPrList` when both the dlls and o_dlls slots are the
	### freshly-inserted list (the canonical form `available` uses).
	### Provable by structural induction on dlls using
	### `insertDPrList_preserves_locs` (dlls.ath:284) and
	### `available_key_dlls_locs_inv` (dlls.ath:789) — both available
	### predicates ultimately depend on dlls only through `dlls_locs`.
	define no_consecutive_failures_insert_inv :=
		(forall n rv1 v0 dlls0 .
			(no_consecutive_failures rv1
				(insertDPrList n rv1 v0 dlls0)
				(insertDPrList n rv1 v0 dlls0))
			<==>
			(no_consecutive_failures rv1 dlls0 dlls0))
	assert no_consecutive_failures_insert_inv

	### Auxiliary lemma (ASSERTED): the "every-position implies
	### this-position" lookup. If every (rv+1)-window in a non-empty
	### dlls is alive, then so is the window at any chosen bucket index.
	### Provable by induction on (bucket, dlls).
	define no_consecutive_failures_implies_key_available :=
		(forall n rv1 dlls0 htl .
			((~ (dlls0 = (dempty htl))) &
			 (no_consecutive_failures rv1 dlls0 dlls0))
			==>
			(available_key n rv1 dlls0 dlls0))
	assert no_consecutive_failures_implies_key_available

	### Auxiliary lemma (PROVED): `insertDPrList` preserves
	### non-emptiness. Discharged here by contradiction using
	### `insert_into_empty_dlls`.
	define insertDPrList_preserves_nonempty :=
		(forall n rv1 v0 dlls0 htl .
			(~ ((insertDPrList n rv1 v0 dlls0) = (dempty htl)))
			==>
			(~ (dlls0 = (dempty htl))))
	conclude insertDPrList_preserves_nonempty
		pick-any n:N rv1:N v0:'S dlls0:(DLst (Lst 'S)) htl:Location
		assume hyp_ne := (~ ((insertDPrList n rv1 v0 dlls0) = (dempty htl)))
			(!by-contradiction (~ (dlls0 = (dempty htl)))
				assume dlls0_empty := (dlls0 = (dempty htl))
					let { collapse := (!chain [
							(insertDPrList n rv1 v0 dlls0)
							= (insertDPrList n rv1 v0 (dempty htl)) [dlls0_empty]
							= (dempty htl)                          [DL_L_S.insert_into_empty_dlls]
						]) }
					(!absurd collapse hyp_ne))


	define dht_replication_correctness :=
		(forall dht hf rv htl dlls .
			(((rep dht) = (dhtr hf rv htl dlls)) &
			 (~ (dlls = (dempty htl))) &
			 (no_consecutive_failures rv dlls dlls))
			==>
			(available dht))

	by-induction dht_replication_correctness {
	  (dht as (dht_empty ll1 hf1 rv1 htl1)) =>
		pick-any hf:(fn 'S N) rv:N htl:Location dlls:(DLst (Lst 'S))
		assume hyp := (((rep dht) = (dhtr hf rv htl dlls)) &
		               (~ (dlls = (dempty htl))) &
		               (no_consecutive_failures rv dlls dlls))
			(!chain-> [
				true
				==> (available (dht_empty ll1 hf1 rv1 htl1)) [available_axioms]
			])
	| (dht as (dht_insert dht0 v0)) =>
		let { IH := (forall hf rv htl dlls .
		                (((rep dht0) = (dhtr hf rv htl dlls)) &
		                 (~ (dlls = (dempty htl))) &
		                 (no_consecutive_failures rv dlls dlls))
		                ==>
		                (available dht0)) }
		pick-any hf:(fn 'S N) rv:N htl:Location dlls_after:(DLst (Lst 'S))
		assume hyp := (((rep (dht_insert dht0 v0)) = (dhtr hf rv htl dlls_after)) &
		               (~ (dlls_after = (dempty htl))) &
		               (no_consecutive_failures rv dlls_after dlls_after))
			let {
				# Extract the three conjuncts of hyp.
				rep_eq_after  := (!chain-> [
					hyp ==> ((rep (dht_insert dht0 v0)) = (dhtr hf rv htl dlls_after))
						[prop-taut]]);
				nonempty_after := (!chain-> [
					hyp ==> (~ (dlls_after = (dempty htl))) [prop-taut]]);
				ncf_after := (!chain-> [
					hyp ==> (no_consecutive_failures rv dlls_after dlls_after) [prop-taut]]);
				# By rep_e applied to dht0, dht0 has an internal representation.
				ex_rep0 := (!uspec rep_e dht0)
			}
			pick-witnesses hf0 rv0 htl0 dlls0 for ex_rep0 rep0_eq
			let {
				# rep_axioms unfolds (rep (dht_insert dht0 v0)) using the
				# witnesses just bound (the `when` clause of the axiom).
				insert_rep_form := (!chain [
					(rep (dht_insert dht0 v0))
					= (dhtr hf0 rv0 htl0 (insertDPrList (hf0 at v0) rv0 v0 dlls0)) [rep_axioms]
				]);
				# Combine with rep_eq_after to compare two dhtr forms.
				dhtr_eq := (!chain [
					(dhtr hf rv htl dlls_after)
					= (rep (dht_insert dht0 v0))                                       [rep_eq_after]
					= (dhtr hf0 rv0 htl0 (insertDPrList (hf0 at v0) rv0 v0 dlls0))     [insert_rep_form]
				]);
				# dhtr_no_conf gives us the four component equalities.
				fields_iff := (!chain-> [
					dhtr_eq
					==> ((hf = hf0) & (rv = rv0) & (htl = htl0) &
					     (dlls_after = (insertDPrList (hf0 at v0) rv0 v0 dlls0)))
						[dhtr_no_conf]
				]);
				rv_eq   := (!chain-> [fields_iff ==> (rv = rv0)    [prop-taut]]);
				htl_eq  := (!chain-> [fields_iff ==> (htl = htl0)  [prop-taut]]);
				dlls_eq := (!chain-> [fields_iff
					==> (dlls_after = (insertDPrList (hf0 at v0) rv0 v0 dlls0))
						[prop-taut]]);
				# Transport ncf to the witness-named form so insert_inv can fire.
				ncf_insert_form := (!chain-> [
					ncf_after
					==> (no_consecutive_failures rv
							(insertDPrList (hf0 at v0) rv0 v0 dlls0)
							(insertDPrList (hf0 at v0) rv0 v0 dlls0))
						[dlls_eq]
					==> (no_consecutive_failures rv0
							(insertDPrList (hf0 at v0) rv0 v0 dlls0)
							(insertDPrList (hf0 at v0) rv0 v0 dlls0))
						[rv_eq]
				]);
				ncf_before := (!chain-> [
					ncf_insert_form
					==> (no_consecutive_failures rv0 dlls0 dlls0)
						[no_consecutive_failures_insert_inv]
				]);
				# Non-emptiness of dlls0: translate through htl_eq and dlls_eq,
				# then apply the contrapositive lemma.
				nonempty_insert_form := (!chain-> [
					nonempty_after
					==> (~ (dlls_after = (dempty htl0))) [htl_eq]
					==> (~ ((insertDPrList (hf0 at v0) rv0 v0 dlls0) = (dempty htl0)))
						[dlls_eq]
				]);
				nonempty_before := (!mp
					(!uspec* insertDPrList_preserves_nonempty
						[(hf0 at v0) rv0 v0 dlls0 htl0])
					nonempty_insert_form);
				# Apply IH at the witness names.
				ih_premise := (!both rep0_eq (!both nonempty_before ncf_before));
				avail_dht0 := (!mp (!uspec* IH [hf0 rv0 htl0 dlls0]) ih_premise);
				# Lookup lemma: available_key holds at (hf0 at v0).
				lookup_premise := (!both nonempty_before ncf_before);
				avail_key := (!mp
					(!uspec* no_consecutive_failures_implies_key_available
						[(hf0 at v0) rv0 dlls0 htl0])
					lookup_premise);
				# available_axioms (dht_insert clause) fires because rep0_eq
				# supplies its `when` antecedent with the same witnesses.
				avail_conj := (!both avail_dht0 avail_key);
				avail_iff := (!chain-> [
					rep0_eq
					==> ((available (dht_insert dht0 v0)) <==>
					     ((available dht0) &
					      (available_key (hf0 at v0) rv0 dlls0 dlls0)))
						[available_axioms]
				])
			}
			(!chain-> [
				avail_conj
				==> (available (dht_insert dht0 v0)) [avail_iff]
			])
	}
}