dhtable.ath

load "htable.ath"
load "dpair.ath"

# Hashtable inductive generation as a sequence of API calls:
structure (DHTable S) := (dht-empty  (Pr Location Location) (fn S N)) |
                         (dht-insert (DHTable S) S)

# Hashtable representation using lists
datatype (DHTRep S) := (dhtr (fn S N) (DPr (Lst S) (Lst S)))

module DHTable {
			
	assert dht-st-axioms := (structure-axioms "DHTable")
	define [dht-no-conf dht-no-junk] := dht-st-axioms


	define [f f']      := [?f:(fn 'S N) ?f':(fn 'S N)]
	define [e o e' o'] := [?e:(Lst 'S) ?o:(Lst 'S) ?e':(Lst 'S) ?o':(Lst 'S)]
	define [le lo le' lo'] := [?le:Location  ?lo:Location ?le':Location ?lo':Location]

	assert* dhtr-no-conf :=
	((dhtr f (dpr le e lo o)) = (dhtr f' (dpr le' e' lo' o')) <==>
	((f = f') & (le = le') & (e = e') & (lo = lo') & (o = o')))
		
	#---dht-rep

	declare rep : (S) [(DHTable S)] -> (DHTRep S)	       

	overload rep HTable.rep

	define [dt v v'] := [?dt:(DHTable 'S) ?v:'S ?v':'S]

	assert rep-axioms :=
	(fun [
		(rep (dht-empty (pr le lo) f)) = (dhtr f (dpr le empty lo empty))
		(rep (dht-insert dt v)) = 
		[
			(dhtr f (dpr le (lst v e) lo o)) when 
								((rep dt) = (dhtr f (dpr le e lo o)) & (f at v = zero))
			(dhtr f (dpr le e lo (lst v o))) when
							    ((rep dt) = (dhtr f (dpr le e lo o)) & (~ f at v = zero))
		]
	])

	
	define rep-e :=
	(forall dt . exists f le e lo o .
		((rep dt) = (dhtr f (dpr le e lo o))))

	by-induction rep-e {
	(dt as (dht-empty (pr le' lo') f')) =>				  
	let{rep-dt := (!chain [(rep dt)
				= (dhtr f' (dpr le' empty lo' empty)) [rep-axioms]])}
	(!egen* (exists f le e lo o . ((rep dt) = (dhtr f (dpr le e lo o))))
		[f' le' empty lo' empty])
	| (dt as (dht-insert dt' v)) =>
	let {ih := (exists f' le' e' lo' o' .
				((rep dt') = (dhtr f' (dpr le' e' lo' o'))))}
	pick-witnesses f' le' e' lo' o' for ih rep-dt'-def
		let { m := (method (a le' el lo' ol)
		assume a
			let{ rep-dt := (!chain<- [((rep dt) =
					(dhtr f' (dpr le' el lo' ol)))
					<== (rep-dt'-def & a)        [rep-axioms]])}
		(!egen* (exists f le e lo o .
				((rep dt) = (dhtr f (dpr le e lo o))))
			[f' le' el lo' ol]))}	     
		(!two-cases
		(!m (f' at v = zero)    le' (lst v e')  lo' o')
		(!m (~ f' at v = zero)  le' e'          lo' (lst v o')))}


	#cvarela: following two lemmas can be exercises.

	define [e0 o0] := [?e0:(Lst 'S) ?o0:(Lst 'S)]

	define rep-loc-eq :=
	(forall dt f le e lo o f' le' e' lo' o' .
		((rep dt = (dhtr f (dpr le e lo o)) &
		(rep dt = (dhtr f' (dpr le' e' lo' o')))) ==>
		(le = le' & lo = lo')))

	conclude rep-loc-eq
	pick-any dt:(DHTable 'S) f le e lo o f' le' e' lo' o'
		let {a1 := (rep dt = (dhtr f  (dpr le e lo o)));
		a2 := (rep dt = (dhtr f' (dpr le' e' lo' o')))}
		assume (a1 & a2)
		(!chain-> [(dhtr f (dpr le e lo o))
			= (rep dt)                               [a1]
			= (dhtr f' (dpr le' e' lo' o'))          [a2]
			==> (f = f' & le = le' & e = e' & lo = lo' & o = o')
														[dhtr-no-conf]
			==> (le = le' & lo = lo')                [prop-taut]])


	define rep-loc :=
	(forall dt v f le e lo o .
		((rep (dht-insert dt v)) = (dhtr f (dpr le e lo o)) ==>
		exists e0 o0 . (rep dt = (dhtr f (dpr le e0 lo o0)))))

	conclude rep-loc
	pick-any dt:(DHTable 'S) v f le e lo o
	assume rep-dt' := (rep (dht-insert dt v) = (dhtr f (dpr le e lo o)))
		let{rep-dt0 := (!fire rep-e [dt])}
		pick-witnesses f' le' e' lo' o' for rep-dt0 rep-dt-def
		# (rep dt) = (dhtr f' (dpr le' e' lo' o'))
		let {m := (method (a e'' o'')
		assume a
			let {rep-dt'' :=
				(!chain<- [((rep (dht-insert dt v))
					= (dhtr f' (dpr le' e'' lo' o'')))
				<== (rep-dt-def & a)                 [rep-axioms]]);
				le=le' := (!chain<- [(le = le' & lo = lo')
					<== (rep-dt' & rep-dt'')  [rep-loc-eq]]);
			dhtr-eq := (!combine-equations
						(!sym rep-dt') (!sym rep-dt''));
			f=f' := (!chain<- [(f = f')
						<== dhtr-eq            [dhtr-no-conf]])}
			(!chain [(rep dt)
						= (dhtr f' (dpr le' e' lo' o'))       [rep-dt-def]
				= (dhtr f' (dpr le  e' lo  o'))       [le=le']
				= (dhtr f (dpr le e' lo o'))          [f=f']]));
		_ := (!two-cases
			(!m (f' at v = zero)   (lst v e') o')
			(!m (~ f' at v = zero) e'         (lst v o')))}
		(!egen* (exists e0 o0 . (rep dt = (dhtr f (dpr le e0 lo o0))))
			[e' o'])

	#---rep-inv

			
	#---dht-query

	declare query : (S) [(DHTable S) S] -> (Option Boolean)

	overload query HTable.query

	assert query-axioms :=
	(fun
	[(query dt v) =
		[(SOME (v in e)) when
		(((rep dt) = (dhtr f (dpr le e lo o))) &
		(f at v = zero) & (alive le))
		NONE when
		(((rep dt) = (dhtr f (dpr le e lo o))) &
		(f at v = zero) & (~ alive le))
		(SOME (v in o)) when
		(((rep dt) = (dhtr f (dpr le e lo o))) &
		(~ f at v = zero) & (alive lo))
		NONE when
		(((rep dt) = (dhtr f (dpr le e lo o))) &
		(~ f at v = zero) & (~ alive lo))]])


	#---dht-values

	declare values : (S) [(DHTable S)] -> (Option (Set.Set S))

	overload values HTable.values

	assert values-axioms :=
	(fun
		[(values dt) =
		[(SOME ((l2s e) \/ (l2s o))) when
							((rep dt) = (dhtr f (dpr le e lo o)) &
					(alive le) & (alive lo))
		(SOME (l2s e)) when  ((rep dt) = (dhtr f (dpr le e lo o)) &
					(alive le) & (~ alive lo))
		(SOME (l2s o)) when  ((rep dt) = (dhtr f (dpr le e lo o)) &
					(~ alive le) & (alive lo))
		NONE when            ((rep dt) = (dhtr f (dpr le e lo o)) &
					(~ alive le) & (~ alive lo))]])


	#---dht-hf

	declare hf : (S) [(DHTable S)] -> (fn S N)

	overload hf HTable.hf

	assert hf-axioms :=
	(fun
	[(hf (dht-empty (pr le lo) f))    = f
		(hf (dht-insert dt v))           = (hf dt)])
	
	#cvarela: where is hf located?  It could be replicated in both le and
	#lo, then a partial definition would be: 
	#
	#  [(hf (dht-empty (pr le lo) f)) = f when ((alive le) | (alive lo)) 
	#
	# OR it could be assumed common knowledge?! (as defined)
	# OR modeled optional as (Option (fn S N))


	#---equal
	#
	# When are two distributed hashtables equal?

	define [dt']  := [?dt':(DHTable 'S)]

	# assert* dht-equal-axiom := (dt = dt' <==> ((hf dt) = (hf dt') &
	# 					   (values dt) = (values dt')))
	# cvarela: make it failure-independent:
	assert dht-equal-axiom :=
	(forall dt dt' . (dt = dt') <==>
				exists f e o le lo e' o' le' lo' .
				((rep dt)  = (dhtr f (dpr le  e  lo  o)) &
				(rep dt') = (dhtr f (dpr le' e' lo' o')) &
				(l2s e) = (l2s e') &
				(l2s o) = (l2s o')))

	# No failure equivalence proofs

	# Essentially, we want to prove that a distributed hashtable behaves
	# like a local hashtable when there are no failures, and that two
	# equal non-failing distributed hashtables behave equivalently.

	# when is a hashtable equal to a distributed hashtable
	declare equal: (S) [(HTable S) (DHTable S)] -> Boolean
	#cvarela: how to make the arguments interchangeable?

	#---ht-dht-equal

	define [de do] := [?de:(Lst 'S) ?do:(Lst 'S)]

	# a hashtable is equal to a dht, if their functions are identical, and
	# their sets of even numbers and odd numbers are respectively equal.
	# The equality relationship is independent of the locations of the
	# lists of numbers.
	assert ht-dht-equal-axiom :=
	(forall t dt . (t equal dt) <==>
				exists f e o le de lo do .
				((rep t) = (htr f (pr e o)) &
				(rep dt) = (dhtr f (dpr le de lo do)) &
				(l2s e) = (l2s de) &
				(l2s o) = (l2s do)))

	# cvarela: exercise: prove a lemma of correspondence between empty
	# hashtables, which states that if an empty hashtable is equal to a
	# distributed hashtable {\tt dt}, then {\tt dt} must be {\tt
	# (dht-empty lp f)} for some location pair {\tt lp}.

	#---dht-canonical

	#
	# every distributed hashtable has a "canonical" non-distributed
	# hashtable where all location information has been removed

	declare canonical: (S) [(DHTable S)] -> (HTable S)

	define [lp]   := [?lp:(Pr Location Location)]

	assert* canonical-dempty :=
	(canonical (dht-empty lp f) = (ht-empty f))

	assert* canonical-dinsert :=
	(canonical (dht-insert dt v) = (ht-insert (canonical dt) v))
	
	
	define canonical-equal := (forall dt . (canonical dt) equal dt)

	by-induction canonical-equal {
	(dt as (dht-empty (pr le' lo') f'))   =>
	let{de' := empty; do' := empty; e' := empty; o' := empty;
		t     := (canonical dt);
		t-def := (!chain [t = (ht-empty f')          [canonical-dempty]]);
		_     := (!chain [(rep t)
				= (rep (ht-empty f'))        [t-def]
				= (htr f' (pr e' o'))        [HTable.rep-axioms]]);
		_     := (!chain [(rep dt)
				= (dhtr f' (dpr le' de' lo' do'))  [rep-axioms]]);
		_ := (!chain<- [((rep t) = (htr f' (pr e' o')) &
				(rep dt) = (dhtr f' (dpr le' de' lo' do')) &
				(l2s e') = (l2s de') &
				(l2s o') = (l2s do'))
			<== true                         [augment]]);
		wit := (!egen* (exists f e o le de lo do .
				((rep t) = (htr f (pr e o)) &
				(rep dt) = (dhtr f (dpr le de lo do)) &
				(l2s e) = (l2s de) &
				(l2s o) = (l2s do)))
				[f' e' o' le' de' lo' do'])}
	(!chain-> [wit
		==> (t equal dt)                        [ht-dht-equal-axiom]])
	| (dt as (dht-insert dt0 v)) =>
	let{t     := (canonical dt);
		t0    := (canonical dt0);
		t-def := (!chain [t = (ht-insert t0 v)       [canonical-dinsert]]);
		ih    := (t0 equal dt0);
		ih-c  := (!fire ht-dht-equal-axiom [t0 dt0])}
	pick-witnesses f0 e0 o0 le0 de0 lo0 do0 for ih-c
		let{rep-t0  := ((rep t0) = (htr f0 (pr e0 o0)));
		rep-dt0 := ((rep dt0) = (dhtr f0 (dpr le0 de0 lo0 do0)));
		e-de0   := ((l2s e0) = (l2s de0));      
		o-do0   := ((l2s o0) = (l2s do0));
			m := (method (a e' o' de' do')
			assume a
			let{     
		rep-t   := (!chain<- [((rep t) = (htr f0 (pr e' o')))
					<== ((rep (ht-insert t0 v))
					= (htr f0 (pr e' o')))    [t-def]
					<== (rep-t0 & a)    [HTable.rep-axioms]]);
		rep-dt  := (!chain<- [((rep dt)
						= (dhtr f0 (dpr le0 de' lo0 do')))
					<== (rep-dt0 & a)              [rep-axioms]]);
			m' := (method (e' de' e0 de0 o' do')
					let {e-de :=
					(!chain [(l2s e') 
					= (Set.insert v (l2s e0))
									[Lst.toSet.toSet-lst-axiom]
					= (Set.insert v (l2s de0))     [e-de0 o-do0]
					= (l2s de')	    [Lst.toSet.toSet-lst-axiom]]);
						o-do := 
					(!chain [(l2s o')  = (l2s do')       [o-do0 e-de0]])}
				(!both e-de o-do));
		_ := try { (!m' e' de' e0 de0 o' do') |
				(!m' o' do' o0 do0 e' de') }}
			(!chain-> [((rep t) = (htr f0 (pr e' o')) &
				(rep dt) = (dhtr f0 (dpr le0 de' lo0 do')) &
				(l2s e') = (l2s de') &
				(l2s o') = (l2s do'))
			==> (exists f e o le de lo do .
				((rep t) = (htr f (pr e o)) &
					(rep dt) = (dhtr f (dpr le de lo do)) &
					(l2s e) = (l2s de) &
					(l2s o) = (l2s do)))            [existence]
				==> (t equal dt)               [ht-dht-equal-axiom]]))}
	(!two-cases
	(!m (f0 at v = zero)   (lst v e0) o0         (lst v de0) do0)
	(!m (~ f0 at v = zero) e0         (lst v o0) de0         (lst v do0)))}

		
	define [dt1 dt2] := [?dt1:(DHTable 'S) ?dt2:(DHTable 'S)]

	# if two distributed hashtables are equal, they have equal
	# canonical hashtables
	define equal-preserves-canonical :=
	(forall dt1 dt2 . dt1 = dt2 ==> (canonical dt1) = (canonical dt2))

	#cvarela: exercise.
	(!force equal-preserves-canonical)


	#---dht-ht-equiv

	# when are a hashtable and a distributed hashtable behaviorally
	# equivalent (i.e., observationally undistinguishable)
	declare ht-equiv: (S) [(HTable S) (DHTable S)] -> Boolean

	assert ht-dht-equiv-def :=
	(forall t dt . (t ht-equiv dt) <==>
			forall v . ((query dt v) = (SOME (query t v))))

	# cvarela: could have different hashing functions...
	# cvarela: values equal is a theorem that follows from ht-equiv def.

	define ht-dht-equiv-lemma :=
	(forall t dt v . (t ht-equiv dt) ==> ((query dt v) = (SOME (query t v))))

	conclude ht-dht-equiv-lemma
	pick-any t dt:(DHTable 'S) v
	assume (t ht-equiv dt)
		let{ht-dht-equiv-> := (!fire ht-dht-equiv-def [t dt])}
		(!chain [(query dt v) = (SOME (query t v)) [ht-dht-equiv->]])

	# cvarela: following could be exercises.
	define no-local-failures-empty :=
	(forall f .
		((ht-empty f) ht-equiv (dht-empty (pr localhost localhost) f)))

	define no-local-failures-insert :=
	(forall t dt v .
		((t ht-equiv dt) ==>
		(ht-insert t v) ht-equiv (dht-insert dt v)))
	#cvarela: <== is not true: (insert empty 1) ht-equiv (dht-insert [1] 1).

	# define ht-dht-equiv-equal :=
	#   (forall t dt1 dt2 .
	#     ((t ht-equiv dt1) & (t ht-equiv dt2)) ==> dt1 = dt2)	
	# cvarela: does not hold if dt1 and dt2 use different hashing
	# functions, we have to use alternative definition:
	define ht-dht-equiv-equal :=
	(forall t dt1 dt2 .
		((t ht-equiv dt1) & (t ht-equiv dt2) & (hf dt1 = hf dt2)) ==>
		dt1 = dt2)

	# exercise: hashtable equivalent to local distributed hashtable

	#---dht-alive

	# we lift 'alive' predicate to distributed hashtables:
	declare alive: (S) [(DHTable S)] -> Boolean

	overload alive Location.alive

	assert* alive-dht-empty :=
	((alive (dht-empty (pr le lo) f)) <==> (alive le) & (alive lo))

	assert* alive-dht-insert :=
	((alive (dht-insert dt v)) <==> (alive dt))


	define alive-le-lo :=
	(forall dt f le e lo o .
		(((alive dt) & (rep dt = (dhtr f (dpr le e lo o)))) ==>
		(alive le & alive lo)))

	by-induction alive-le-lo {
	(dt as (dht-empty (pr le' lo') f')) =>
	pick-any f le e lo o
		assume ((alive dt) & (rep dt = (dhtr f (dpr le e lo o))))
		let {_ := (!chain [(rep dt)
				= (dhtr f' (dpr le' empty lo' empty)) [rep-axioms]]); 
			eql := (!chain<- [(le = le' & lo = lo')
				<== ((rep dt = (dhtr f (dpr le e lo o))) &
					(rep dt = (dhtr f' (dpr le' empty lo' empty))))
										[rep-loc-eq]])}
		(!chain<- [(alive le & alive lo)
		<== (alive le' & alive lo')       [eql]
		<== (alive dt)                    [alive-dht-empty]])
	| (dt as (dht-insert dt' v)) =>
	let {ih := (forall f le e lo o .
				(((alive dt') & (rep dt' = (dhtr f (dpr le e lo o)))) ==>
			(alive le & alive lo)))}
	pick-any f le e lo o
		assume ((alive dt) & (rep dt = (dhtr f (dpr le e lo o))))
		let{rep-dt0 := (!fire rep-loc [dt' v f le e lo o])}
		pick-witnesses e0 o0 for rep-dt0 rep-dt
								# (rep dt' = (dhtr f (dpr le e0 lo o0)))
		(!chain<- [(alive le & alive lo)
			<== ((alive dt') & rep-dt)        [ih]
			<== (alive dt')                   [augment]
			<== (alive dt)                    [alive-dht-insert]])}
			

	# an alive distributed hashtable is equivalent to its equal
	# (non-distributed) hashtable.
	define ht-dht-no-failures :=
	(forall t dt . ((t equal dt) & (alive dt)) ==> (t ht-equiv dt))
	#cvarela: if and only if? No!  Even though local hashtables never fail,
	#                              hashing functions could be different.

	conclude ht-dht-no-failures
	pick-any t dt:(DHTable 'S)
	assume ((t equal dt) & (alive dt))
		let{e-feo := (!fire ht-dht-equal-axiom [t dt])}
		pick-witnesses f e o le de lo do for e-feo e-feo-c
		let{rep-t  := ((rep t) = (htr f (pr e o)));
		rep-dt := ((rep dt) = (dhtr f (dpr le de lo do)));
		e-de   := ((l2s e) = (l2s de));      
		o-do   := ((l2s o) = (l2s do));      
			_ := (!chain<- [((alive le) & (alive lo))
				<== ((alive dt) & rep-dt)             [alive-le-lo]]);
		in-e := (!fire Lst.toSet.in-equal [e de]);
			in-o := (!fire Lst.toSet.in-equal [o do]);
		m := (method (v a e de le in-e)
			assume a
					let{qtv := (!chain<- [((query t v) = (v in e))
					<== (rep-t & a) [HTable.query-axioms]]);
				qdtv :=
				(!chain<- [((query dt v) = (SOME (v in de)))
					<== (rep-dt & a & alive le) [query-axioms]])}
				(!chain [(query dt v)
				= (SOME (v in de))                  [qdtv]
				= (SOME (v in e))                   [in-e]
				= (SOME (query t v))                [qtv]]));
			qtdtv :=
		pick-any v:'S
			(!two-cases
			(!m v (f at v = zero)   e de le in-e)
			(!m v (~ f at v = zero) o do lo in-o))}
		(!chain-> [qtdtv
		==> (t ht-equiv dt)                       [ht-dht-equiv-def]])

	define canonical-equiv :=
		(forall dt . (alive dt) ==> ((canonical dt) ht-equiv dt))

	conclude canonical-equiv
	pick-any dt:(DHTable 'S)
	(!chain [(alive dt)
		==> (true & alive dt)                        [augment]
		==> (((canonical dt) equal dt) & (alive dt)) [canonical-equal]
		==> ((canonical dt) ht-equiv dt)             [ht-dht-no-failures]])

	#---dht-equiv

	# when are two distributed hashtables behaviorally equivalent
	declare dht-equiv: (S) [(DHTable S) (DHTable S)] -> Boolean

	define [t dt1 dt2] := [?t:(HTable 'S) ?dt1:(DHTable 'S) ?dt2:(DHTable 'S)]

	assert* dht-equiv-def :=
	(dt1 dht-equiv dt2 <==> exists t . (t ht-equiv dt1) & (t ht-equiv dt2))

	define dht-equiv-lemma :=
	(forall dt1 dt2 .
		(canonical dt1 = canonical dt2 & alive dt1 & alive dt2) ==>
		(dt1 dht-equiv dt2))

	conclude dht-equiv-lemma
	pick-any dt1:(DHTable 'S) dt2:(DHTable 'S)
	assume (canonical dt1 = canonical dt2 & alive dt1 & alive dt2)
		(!chain<- [(dt1 dht-equiv dt2)
		<== (exists t . (t ht-equiv dt1) & (t ht-equiv dt2)) [dht-equiv-def]
		<== ((canonical dt1) ht-equiv dt1 & (canonical dt1) ht-equiv dt2)
														[existence]
		<== ((canonical dt1) ht-equiv dt1 & (canonical dt2) ht-equiv dt2)
										[(canonical dt1 = canonical dt2)]
		<== (alive dt1 & alive dt2)        [canonical-equiv]])

	# two equal and alive distributed hashtables are behaviorally equivalent
	define dht-equiv-no-failures :=
	(forall dt1 dt2 . (dt1 = dt2) & (alive dt1) & (alive dt2)
						==> dt1 dht-equiv dt2)

	conclude dht-equiv-no-failures
	pick-any dt1:(DHTable 'S) dt2:(DHTable 'S)
		(!chain [ ((dt1 = dt2) & (alive dt1) & (alive dt2))
		==> (((canonical dt1) = (canonical dt2)) &
			(alive dt1) & (alive dt2))    [equal-preserves-canonical]
		==> (dt1 dht-equiv dt2)            [dht-equiv-lemma]])


	module Query {

		define [opt-noconf-none opt-noconf-some opt-nojunk] :=
		(datatype-axioms "Option")

		define query-preserves-equiv :=
		(forall t dt v . (t ht-equiv dt) ==>
			((  (query t v) <==> (query dt v) = (SOME true)) &
			((~ query t v) <==> (query dt v) = (SOME false))))

		conclude query-preserves-equiv
		pick-any t dt:(DHTable 'S) v
		assume (t ht-equiv dt)
			let{ qtdtv := (!fire ht-dht-equiv-def [t dt]);
			1A := assume a := ((query dt v) = (SOME true))
				(!chain-> [(SOME (query t v))
					= (query dt v)                [qtdtv]
					= (SOME true)                 [a]
				==> ((query t v) = true)        [opt-noconf-some]
				==> (query t v)                 [bool-true]]);
			1B := assume (query t v)
			(!chain [(query dt v)
				= (SOME (query t v))             [qtdtv]
				= (SOME true)         [((query t v) = true)
							<== (query t v)     [true-bool]]]);
			2A := assume a := ((query dt v) = (SOME false))
				(!chain-> [(SOME (query t v))
					= (query dt v)                [qtdtv]
					= (SOME false)                [a]
				==> ((query t v) = false)       [opt-noconf-some]
				==> (~ query t v)               [bool-false]]);
			2B := assume (~ query t v)
			(!chain [(query dt v)
				= (SOME (query t v))             [qtdtv]
				= (SOME false)        [((query t v) = false)
							<== (~ query t v)   [false-bool]]])}
			(!both (!equiv 1B 1A) (!equiv 2B 2A))
				

		# We lift the proofs from HTable.Query.query-fc-*

		define query-fc-empty :=
		(forall lp f v . ((alive (dht-empty lp f)) ==>
					(query (dht-empty lp f) v) = (SOME false)))

		conclude query-fc-empty
		pick-any lp f v
		assume (alive (dht-empty lp f))
			let{dt := (dht-empty lp f);
				t:(HTable 'S) := (canonical dt);
				t-def  := (!chain [t = (ht-empty f)       [canonical-dempty]]);
			_      := conclude (~ (query (ht-empty f) v))
						(!fire HTable.query-fc-empty [f v]);
			q-eq   := (!chain<- [((~ query t v) <==>
						((query dt v) = SOME false))
					<== (t ht-equiv dt)     [query-preserves-equiv]
					<== (alive dt)          [canonical-equiv]])}
			(!chain<- [((query dt v) = SOME false)
			<== (~ query t v)                   [q-eq]
			<== (~ query (ht-empty f) v)        [t-def]])


		define [b b'] := [?b:Boolean ?b':Boolean]

		define query-fc-insert :=
		(forall dt' v' v . (alive (dht-insert dt' v')) ==>
			exists b b' .
			(((query (dht-insert dt' v') v) = (SOME b)) &
			((query dt' v) = (SOME b')) &
			(b <==> ((v = v') | b'))))

		conclude query-fc-insert
		pick-any dt0:(DHTable 'S) v0 v
		assume (alive (dht-insert dt0 v0))
			let { dt    := (dht-insert dt0 v0);
			t     := (canonical dt);
			t0    := (canonical dt0);
			t-def := (!chain [t = (ht-insert t0 v0)   [canonical-dinsert]]);
				b0    := (query t v);
				b0'   := (query t0 v);
			h-c   := conclude ((query (ht-insert t0 v0) v) <==>
						((v = v0) | (query t0 v)))
						(!instance HTable.query-fc-insert [t0 v0 v]);
				_     := (!chain<- [ (b0 <==> (v = v0) | b0')
							<== h-c                   [t-def]]);
				_     := (!chain<- [ ((query dt v)  = (SOME b0))
						<== (t ht-equiv dt)       [ht-dht-equiv-lemma]
					<== (alive dt)            [canonical-equiv]]);
				_     := (!chain<- [ ((query dt0 v)  = (SOME b0'))
						<== (t0 ht-equiv dt0)     [ht-dht-equiv-lemma]
					<== (alive dt0)           [canonical-equiv]
					<== (alive dt)            [alive-dht-insert]]);
				_     := (!chain<- [((query dt v)  = (SOME b0) &
						(query dt0 v) = (SOME b0') &
						(b0 <==> ((v = v0) | b0'))) 
						<== true                   [augment]])}
			(!egen* (exists b b' .
					(((query (dht-insert dt0 v0) v) = (SOME b)) &
					((query dt0 v) = (SOME b')) &
					(b <==> ((v = v0) | b'))))
				[b0 b0'])

		# lp: location pair
		# query's functional correctness
		define query-fc :=
		(forall dt v . (a		# lp: location pair
		# query's functional correctness
		define query-fc :=
		(forall dt v . (alive dt ==>
			((exists lp f .        (dt = (dht-empty lp f) &
						(query dt v) = (SOME false)))
			|
			(exists dt' v' b b' . (
						dt = (dht-insert dt' v') &
						(query dt v)  = (SOME b) &
						(query dt' v) = (SOME b') &
						(b <==> ((v = v') | b'))
						))
			)))live dt ==>
			((exists lp f .        (dt = (dht-empty lp f) &
						(query dt v) = (SOME false)))
			|
			(exists dt' v' b b' . (
						dt = (dht-insert dt' v') &
						(query dt v)  = (SOME b) &
						(query dt' v) = (SOME b') &
						(b <==> ((v = v') | b'))
						))
			)))

		datatype-cases query-fc {
		(dt as (dht-empty (pr le lo) f':(fn 'S N))) =>
		pick-any v:'S
			assume (alive dt)
			let{_ := (!chain<- [(dt = (dht-empty (pr le lo) f') &
					(query dt v) = SOME false)
					<== ((dt = dt) & (alive dt))    [query-fc-empty]])}
			(!either
				(!egen* (exists lp f . (dt = (dht-empty lp f) &
						(query dt v) = (SOME false)))
				[(pr le lo) f'])
				(exists dt' v' b b' . (dt = (dht-insert dt' v') &
						(query dt v)  = (SOME b) &
						(query dt' v) = (SOME b') &
						(b <==> ((v = v') | b')))))
		| (dt as (dht-insert dt0 v0)) =>
		pick-any v
			assume (alive dt)
			let{ebs := (!fire query-fc-insert [dt0 v0 v])}
			pick-witnesses b0 b0' for ebs
				let{_ := (!chain<- [(dt = (dht-insert dt0 v0) &
						(query dt v)  = (SOME b0) &
						(query dt0 v) = (SOME b0') &
						(b0 <==> ((v = v0) | b0'))) 
						<== true                        [augment]])}
			(!either    
				(exists lp f .                (dt = (dht-empty lp f) &
							(query dt v) = (SOME false)))
				(!egen* (exists dt' v' b b' . (dt = (dht-insert dt' v') &
							(query dt v)  = (SOME b) &
							(query dt' v) = (SOME b') &
							(b <==> ((v = v') | b'))))
				[dt0 v0 b0 b0']))}
	
	} # close module DHTable.Query

	module Values{

		define [s s'] := [?s:(Set.Set 'S) ?s':(Set.Set 'S)]

		# cvarela:  following could be a great exercise:
		# theorem relating query and values
		define query-values :=
		(forall dt v .
			(alive dt) ==> exists b s . ((query dt v) = (SOME b) &
						(b <==> v in s) &
						(values dt = SOME s)))

		conclude query-values
		pick-any dt:(DHTable 'S) v:'S
		assume (alive dt)
			let{t:(HTable 'S) := (canonical dt);
			qvfc := conclude ((query t v) <==> (v in values t))
					(!instance HTable.query-values [t v]);
				_      := (!chain<- [ (t equal dt)
					<== true                   [canonical-equal]]);
			t=dt := (!fire ht-dht-equal-axiom [t dt])}
			pick-witnesses f e o le de lo do for t=dt
												# rep-t & rep-dt & e-de & o-o
			let{rep-t  := ((rep t) = (htr f (pr e o)));
			rep-dt := ((rep dt) = (dhtr f (dpr le de lo do)));
			e-de   := ((l2s e) = (l2s de));      
			o-do   := ((l2s o) = (l2s do));      
			_ := (!chain<- [ ((query dt v) = (SOME (query t v)))
					<== (t ht-equiv dt)           [ht-dht-equiv-lemma]
					<== (alive dt)                [canonical-equiv]]);
			_ := (!chain<- [((query t v) <==> v in ((l2s e) \/ (l2s o)))
					<== ((query t v) <==> (v in values t))
								[((values t) = ((l2s e) \/ (l2s o)))
							<== rep-t       [HTable.values-axiom]]]);
				_ := (!chain-> [(rep-dt & ((alive dt) & rep-dt))
					==> (rep-dt & (alive le) & (alive lo)) [alive-le-lo]
					==> ((values dt) = (SOME ((l2s de) \/ (l2s do))))
													[values-axioms]
							= (SOME ((l2s e) \/ (l2s o)))
									[e-de o-do]]);
				_ := (!chain<- [((query dt v) = (SOME (query t v)) &
					((query t v) <==> v in ((l2s e) \/ (l2s o))) &
					(values dt = SOME ((l2s e) \/ (l2s o))))
					<== true                               [augment]])}
				(!egen* (exists b s . ((query dt v) = (SOME b) &
						(b <==> v in s) &
						(values dt = SOME s)))
				[(query t v) ((l2s e) \/ (l2s o))])

		# cvarela: equiv is weaker than equal&alive
		#          eg, it accepts different hashing functions
		# following conjecture, while true, is harder to prove.
		define equiv-preserves-values :=
		(forall t dt .
			((t ht-equiv dt) ==> ((values dt) = (SOME (values t)))))


		define equal-preserves-values :=
		(forall t dt .
			((t equal dt) & (alive dt)) ==> (values dt = SOME values t))

		conclude equal-preserves-values
		pick-any t:(HTable 'S) dt:(DHTable 'S)
		assume ((t equal dt) & (alive dt))
			let{t=dt := (!fire ht-dht-equal-axiom [t dt])}
			pick-witnesses f e o le de lo do for t=dt t=dt-c
			let{rep-t  := ((rep t) = (htr f (pr e o)));
			rep-dt := ((rep dt) = (dhtr f (dpr le de lo do)));
			e-de   := ((l2s e) = (l2s de));      
			o-do   := ((l2s o) = (l2s do));      
			vt := (!chain<- [((values t)
					= ((l2s e) \/ (l2s o)))
					<== rep-t             [HTable.values-axiom]]);
				_ := (!chain<- [((alive le) & (alive lo))
					<== ((alive dt) & rep-dt)         [alive-le-lo]]);
			vdt := (!chain<- [((values dt)
						= (SOME ((l2s de) \/ (l2s do))))
					<== (rep-dt & (alive le) & (alive lo))
													[values-axioms]])}
			(!chain [(values dt)
				= (SOME ((l2s de) \/ (l2s do)))          [vdt]
				= (SOME ((l2s e) \/ (l2s o)))            [e-de o-do]
				= (SOME (values t))                      [vt]])


		define canonical-preserves-values :=
		(forall dt . (alive dt) ==>
						(values dt = SOME values (canonical dt)))

		conclude canonical-preserves-values
		pick-any dt:(DHTable 'S)
		assume (alive dt)
			(!chain<- [(values dt = SOME values (canonical dt))
			<== (((canonical dt) equal dt) & (alive dt)) [equal-preserves-values]
			<== ((canonical dt) equal dt)                [augment]
			<== true                                     [canonical-equal]])


		# lifted from Query.values-fc-*

		define values-fc-empty :=
		(forall lp f . ((alive (dht-empty lp f)) ==>
				(values (dht-empty lp f) = (SOME Set.null))))

		conclude values-fc-empty
		pick-any lp f
		assume (alive (dht-empty lp f))
			let{dt := (dht-empty lp f);
				t:(HTable 'S) := (canonical dt);
				t-def  := (!chain [t = (ht-empty f)     [canonical-dempty]])}
			(!chain-> [(true & alive dt)
			==> ((t equal dt) & (alive dt))      [canonical-equal]
			==> ((values dt)
				= (SOME (values t)))            [equal-preserves-values]
				= (SOME (values (ht-empty f)))  [t-def]
				= (SOME Set.null)               [HTable.values-fc-empty]])


		define values-fc-insert :=
		(forall dt' v' .
			((alive (dht-insert dt' v')) ==>
			exists s s' . ((values (dht-insert dt' v')) = (SOME s) &
					(values dt') = (SOME s') &
					(s = (Set.insert v' s')))))

		conclude values-fc-insert
		pick-any dt0:(DHTable 'S) v
		assume (alive (dht-insert dt0 v))
			let{dt := (dht-insert dt0 v);
				t:(HTable 'S) := (canonical dt);
			t0 := (canonical dt0);
				t-def  := (!chain [t = (ht-insert t0 v)     [canonical-dinsert]]);
				val-t := conclude ((values (ht-insert t0 v)) =
					(Set.insert v (values t0)))
					(!instance HTable.values-fc-insert [t0 v]);
				_ := (!chain<- [((values t) = (Set.insert v (values t0)))
					<== ((values (ht-insert t0 v)) =
					(Set.insert v (values t0)))           [t-def]]);
				_ := (!chain<- [((values dt) = (SOME values t))
					<== (alive dt)      [canonical-preserves-values]]);
				_ := (!chain<- [((values dt0) = (SOME values t0))
					<== (alive dt0)    [canonical-preserves-values]
					<== (alive dt)     [alive-dht-insert]]);
				_ := (!chain<- [((values dt) = (SOME (values t)) &
					(values dt0) = (SOME (values t0)) &
					((values t) = (Set.insert v (values t0))))
					<== true                         [augment]])}
			(!egen* (exists s s' . ((values (dht-insert dt0 v)) = (SOME s) &
							(values dt0) = (SOME s') &
						(s = (Set.insert v s'))))
				[(values t) (values t0)])


		# values-fc: (values ht-empty = null &
		#             values (ht-insert t v) = Set.insert v (values t))

		define [s s'] := [?s:(Set.Set 'S) ?s':(Set.Set 'S)]
		
		# values' functional correctness
		define values-fc :=
		(forall dt . ((alive dt) ==>
			((exists lp f .        (dt = (dht-empty lp f) &
							(values dt) = (SOME Set.null))) |
			(exists dt' v' s s' . (dt = (dht-insert dt' v') &
						(values dt) = (SOME s) &
						(values dt') = (SOME s') &
						(s = (Set.insert v' s')))))))

		datatype-cases values-fc{
		(dt as (dht-empty lp' f':(fn 'S N))) =>
		assume (alive dt)
			let{_ := (!chain<- [(dt = (dht-empty lp' f') &
					(values dt) = (SOME Set.null))
					<== ((dt = dt) & (alive dt))      [values-fc-empty]])}
			(!either
			(!egen* (exists lp f . (dt = (dht-empty lp f) &
						(values dt) = (SOME Set.null)))
				[lp' f'])
			(exists dt' v' s s' . (dt = (dht-insert dt' v') &
						(values dt) = (SOME s) &
						(values dt') = (SOME s') &
						(s = (Set.insert v' s')))))
		| (dt as (dht-insert dt0 v)) =>
		assume (alive dt)
			let{ess := (!fire values-fc-insert [dt0 v])}
			pick-witnesses s0 s0' for ess
			let{_ := (!chain<- [(dt = (dht-insert dt0 v) &
					(values dt) = (SOME s0) &
					(values dt0) = (SOME s0') &
					(s0 = (Set.insert v s0')))
					<== ((dt = dt) & true)          [augment]])}
			(!either
			(exists lp f .        (dt = (dht-empty lp f) &
							(values dt) = (SOME Set.null)))
			(!egen* (exists dt' v' s s' . (dt = (dht-insert dt' v') &
								(values dt) = (SOME s) &
								(values dt') = (SOME s') &
								(s = (Set.insert v' s'))))
					[dt0 v s0 s0']))}


	} # close module DHTable.Values


	module Hf{
		#cvarela: exercises: lift hf properties (hf-lemma, hf-sel) from htable.ath

		define hf-fc-empty :=
		(forall le lo f . (hf (dht-empty (pr le lo) f)) = f)

		conclude hf-fc-empty
		pick-any le lo f
		(!chain [(hf (dht-empty (pr le lo) f)) = f              [hf-axioms]])

		define hf-fc-insert :=
		(forall dt v . (hf (dht-insert dt v)) = (hf dt))

		conclude hf-fc-insert
		pick-any dt:(DHTable 'S) v
		(!chain [(hf (dht-insert dt v)) = (hf dt)               [hf-axioms]])


		#cvarela: hf's functional correctness (exercise)
		define hf-fc :=
		(forall dt . ((exists lp f . (dt = (dht-empty lp f) & (hf dt) = f)) |
				exists dt' v . (dt = (dht-insert dt' v) &
						(hf dt) = (hf dt'))))

		datatype-cases hf-fc{
		(dt as (dht-empty (pr le lo) f')) =>
		let{_ := (!chain<- [(dt = (dht-empty (pr le lo) f') & (hf dt) = f')
				<== (dt = (dht-empty (pr le lo) f') & (hf dt) = (hf dt))
													[hf-fc-empty]])}
		(!either
			(!egen* (exists lp f . (dt = (dht-empty lp f) & (hf dt) = f))
				[(pr le lo) f'])
			(exists dt' v . (dt = (dht-insert dt' v) &
						(hf dt) = (hf dt'))))
		| (dt as (dht-insert dt0 v0)) =>
		let {_ := (!chain<- [(dt = (dht-insert dt0 v0) & (hf dt) = (hf dt0))
				<== (dt = (dht-insert dt0 v0) & (hf dt) = (hf dt))
												[hf-fc-insert]])}
		(!either
			(exists lp f . (dt = (dht-empty lp f) & (hf dt) = f))
			(!egen* (exists dt' v . (dt = (dht-insert dt' v) &
						(hf dt) = (hf dt')))
				[dt0 v0]))}
	} # close module DHTable.Hf

	define [s s'] := [?s:(Set.Set 'S) ?s':(Set.Set 'S)]
	define [b b'] := [?b:Boolean ?b':Boolean]

	# dht's fc corollary:
	define dht-fc :=
	(forall dt v . ((alive dt) ==>
		(exists lp f .             (dt = (dht-empty lp f) &
					((query dt v) = (SOME false)) &
					(values dt = (SOME Set.null)) &
					(hf dt = f))) |
		(exists dt' v' b b' s s' . (dt = (dht-insert dt' v') &
					((query dt v)  = (SOME b) &
					(query dt' v) = (SOME b') &
					(b <==> ((v = v') | b'))) &
					((values dt) = (SOME s) &
					(values dt') = (SOME s') &
					(s = (Set.insert v' s'))) &
					(hf dt = hf dt')))))

	datatype-cases dht-fc{
	(dt as (dht-empty (pr le lo) f')) =>
	pick-any v
		assume (alive dt)
		let {_ := (!fire Query.query-fc-empty [(pr le lo) f' v]); 
		_ := (!fire Values.values-fc-empty [(pr le lo) f']);
		_ := (!instance Hf.hf-fc-empty [le lo f']);
			_ := (!chain<- [(dt = (dht-empty (pr le lo) f') &
					((query dt v) = (SOME false)) &
					(values dt = (SOME Set.null)) &
					(hf dt = f'))
				<== true                           [augment]])}
		(!either
			(!egen* (exists lp f . (dt = (dht-empty lp f) &
					((query dt v) = (SOME false)) &
					(values dt = (SOME Set.null)) &
					(hf dt = f)))
			[(pr le lo) f'])
			(exists dt' v' b b' s s' . (dt = (dht-insert dt' v') &
						((query dt v)  = (SOME b) &
						(query dt' v) = (SOME b') &
						(b <==> ((v = v') | b'))) &
						((values dt) = (SOME s) &
						(values dt') = (SOME s') &
						(s = (Set.insert v' s'))) &
						(hf dt = hf dt'))))
	| (dt as (dht-insert dt0 v0)) =>
	pick-any v
		assume (alive dt)
		let{ebs := (!fire Query.query-fc-insert [dt0 v0 v]);
		ess := (!fire Values.values-fc-insert [dt0 v0]);
		_ := (!instance Hf.hf-fc-insert [dt0 v0])}    
		pick-witnesses b0 b0' for ebs
		pick-witnesses s0 s0' for ess
		let {_ := (!chain<- [(dt = (dht-insert dt0 v0) &
					((query dt v)  = (SOME b0) &
					(query dt0 v) = (SOME b0') &
					(b0 <==> ((v = v0) | b0'))) &
					((values dt) = (SOME s0) &
					(values dt0) = (SOME s0') &
					(s0 = (Set.insert v0 s0'))) &
					(hf dt = hf dt0))
				<== true                          [augment]])}
		(!either
			(exists lp f . (dt = (dht-empty lp f) &
					((query dt v) = (SOME false)) &
					(values dt = (SOME Set.null)) &
					(hf dt = f)))
			(!egen* (exists dt' v' b b' s s' . (dt = (dht-insert dt' v') &
						((query dt v)  = (SOME b) &
						(query dt' v) = (SOME b') &
						(b <==> ((v = v') | b'))) &
						((values dt) = (SOME s) &
						(values dt') = (SOME s') &
						(s = (Set.insert v' s'))) &
						(hf dt = hf dt')))
			[dt0 v0 b0 b0' s0 s0']))}


} # close module DHTable

open DHTable

#_ := (print "\n1st:\n" 1st);
#let {_ := (print "\nAtrue:\n" Atrue)}

    # let{rep-dt0 := (!fire rep-e [dt])}
    # pick-witnesses f le e lo o for rep-dt0 rep-dt
    #   # (rep dt) = (dhtr f (dpr le e lo o))