Skip to content

Commit

Permalink
Almost finish proof of ancestor function
Browse files Browse the repository at this point in the history
  • Loading branch information
@huynhtrankhanh
huynhtrankhanh committed Nov 3, 2024
1 parent 4ec18d6 commit 4b20f96
Showing 1 changed file with 127 additions and 78 deletions.
205 changes: 127 additions & 78 deletions theories/DisjointSetUnionCode2.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma runCompressLoop (dsu : list Slot) (hL : length dsu = 100) (hL1 : Z.to_nat (dsuLeafCount dsu) = length dsu) (h1 : noIllegalIndices dsu) (h2 : withoutCyclesN dsu (length dsu)) (a : Z) (hLe1 : Z.le 0 a) (hLt1 : Z.lt a 100) communication (n : nat) (hN : n <= 100) continuation : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state communication 1 arrayIndex0 arrayIndexEqualityDecidable0
Lemma runCompressLoop (dsu : list Slot) (hL : length dsu = 100) (hL1 : Z.to_nat (dsuLeafCount dsu) = length dsu) (h1 : noIllegalIndices dsu) (h2 : withoutCyclesN dsu (length dsu)) (a : Z) (hLe1 : Z.le 0 a) (hLt1 : Z.lt a 100) communication whatever (n : nat) (hN : n <= 100) continuation : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state communication
1 arrayIndex0 arrayIndexEqualityDecidable0
(arrayType arrayIndex0 environment0)
(λ _0 : arrayIndex0,
match
Expand All @@ -22,7 +23,7 @@ Lemma runCompressLoop (dsu : list Slot) (hL : length dsu = 100) (hL1 : Z.to_nat
(eliminateLocalVariables xpred0
(λ _0 : varsfuncdef_0__ancestor,
match _0 with
| vardef_0__ancestor_vertex | _ => a
| vardef_0__ancestor_vertex => whatever | _ => a
end) (fun=> repeat 0%Z 20)
(loop n
(fun=> dropWithinLoop
Expand Down Expand Up @@ -95,12 +96,12 @@ Lemma runCompressLoop (dsu : list Slot) (hL : length dsu = 100) (hL1 : Z.to_nat
λ _2 : Z,
retrieve arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
arraydef_0__result 0 >>=
[eta store arrayIndex0
varsfuncdef_0__ancestor arraydef_0__dsu
_2 >>=
[eta numberLocalSet arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
arraydef_0__dsu _2]) >>=
vardef_0__ancestor_vertex]) >>=
(fun=> liftToWithinLoop
(numberLocalGet arrayIndex0
(arrayType arrayIndex0 environment0)
Expand All @@ -124,18 +125,29 @@ Lemma runCompressLoop (dsu : list Slot) (hL : length dsu = 100) (hL1 : Z.to_nat
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor
arraydef_0__dsu _2 >>=
[eta numberLocalSet arrayIndex0
arraydef_0__result 0 >>=
[eta store arrayIndex0
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor
vardef_0__ancestor_work]) >>=
(fun=> Done
(WithinLoop arrayIndex0
arraydef_0__dsu _2]) >>=
(fun=> liftToWithinLoop
(numberLocalGet arrayIndex0
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor)
withinLoopReturnValue () ()))))) >>=
varsfuncdef_0__ancestor
vardef_0__ancestor_vertex >>=
[eta numberLocalSet arrayIndex0
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor
vardef_0__ancestor_work]) >>=
(fun=> Done
(WithinLoop arrayIndex0
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor)
withinLoopReturnValue () ())))))) >>=
(fun=> Done
(WithLocalVariables arrayIndex0
(arrayType arrayIndex0 environment0)
Expand All @@ -157,18 +169,11 @@ invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state communication 1
end) (funcdef_0__main xpred0 (fun=> 0%Z) (fun=> repeat 0%Z 20))
(continuation ()).
Proof.
move : a hLe1 hLt1 dsu h1 hL hL1 h2. elim : n hN.
{ move => hN a hLe1 hLt1. rewrite (ltac:(simpl; reflexivity) : loop 0 _ = _) leftIdentity (ltac:(simpl; reflexivity) : eliminateLocalVariables xpred0
(λ _0 : varsfuncdef_0__ancestor,
match _0 with
| vardef_0__ancestor_vertex | _ => a
end) (fun=> repeat 0%Z 20)
(Done
(WithLocalVariables arrayIndex0 (arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor) withLocalVariablesReturnValue () ()) = _) leftIdentity.
move => dsu h1 hL hL1 h2.
move : a hLe1 hLt1 dsu h1 hL hL1 h2 whatever. elim : n hN.
{ move => hN a hLe1 hLt1. rewrite (ltac:(simpl; reflexivity) : loop 0 _ = _) leftIdentity.
move => dsu h1 hL hL1 h2 whatever.
rewrite (ltac:(intros; simpl; reflexivity) : forall a b c, pathCompress a 0 b c = _) hL. easy. }
move => n IH hN a hLe1 hLt1 dsu h1 hL hL1 h2. rewrite loop_S -!bindAssoc dropWithinLoopLiftToWithinLoop. unfold numberLocalGet at 1. rewrite -!bindAssoc pushNumberGet2 !leftIdentity.
move => n IH hN a hLe1 hLt1 dsu h1 hL hL1 h2 whatever. rewrite loop_S -!bindAssoc dropWithinLoopLiftToWithinLoop. unfold numberLocalGet at 1. rewrite -!bindAssoc pushNumberGet2 !leftIdentity.
have ra : coerceInt a 64 = a.
{ unfold coerceInt. rewrite Z.mod_small; lia. }
rewrite ra. unfold retrieve at 1. rewrite pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Retrieve. case_decide as xxx; [| rewrite lengthConvert in xxx; lia].
Expand All @@ -188,62 +193,106 @@ Proof.
(ancestor dsu (length dsu) (Z.to_nat a)) = dsu.
{ simpl. rewrite hhh. reflexivity. }
rewrite red hL. reflexivity.
- rewrite !leftIdentity dropWithinLoopLiftToWithinLoop. unfold numberLocalGet at 1. rewrite -!bindAssoc pushNumberGet2 !leftIdentity. unfold retrieve at 1. rewrite pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Retrieve. case_decide as ppp; [| simpl in ppp; lia]. rewrite pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Store (ltac:(simpl; reflexivity) : nth_lt [_] (Z.to_nat 0) _ = _) ra.
have gda : (λ _0 : arrayIndex0,
match decide (_0 = arraydef_0__dsu) with
| left _1 =>
eq_rect_r
(λ _2 : arrayIndex0,
list (arrayType arrayIndex0 environment0 _2))
(@insert nat
(arrayType arrayIndex0 environment0 arraydef_0__dsu)
(list (arrayType arrayIndex0 environment0 arraydef_0__dsu))
(@list_insert
(arrayType arrayIndex0 environment0 arraydef_0__dsu))
(Z.to_nat a)
(Z.of_nat (ancestor dsu (Z.to_nat 100) (Z.to_nat a)))
(convertToArray dsu)) _1
| right _ =>
match
_0 as _2 return (list (arrayType arrayIndex0 environment0 _2))
with
| arraydef_0__dsu => convertToArray dsu
| arraydef_0__hasBeenInitialized => [1%Z]
| arraydef_0__result =>
[Z.of_nat (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]
end
end) = fun xx => match xx with | arraydef_0__dsu => (<[Z.to_nat a:=Z.of_nat
(ancestor dsu (Z.to_nat 100) (Z.to_nat a))]>
(convertToArray dsu)) | arraydef_0__hasBeenInitialized => [1%Z]
| arraydef_0__result =>
[Z.of_nat (ancestor dsu (Z.to_nat 100) (Z.to_nat a))] end.
{ apply functional_extensionality_dep. intro jak. destruct jak; easy. }
rewrite gda. clear gda.
rewrite insertConvertReferTo; [lia | lia |]. rewrite Nat2Z.id dropWithinLoopLiftToWithinLoop. unfold numberLocalGet at 1. rewrite -!bindAssoc pushNumberGet2 ra !leftIdentity. unfold retrieve at 1. rewrite pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Retrieve. clear ppp xxx. case_decide as xxx; [| rewrite lengthConvert in xxx; lia]. case_decide as ppp; [| rewrite lengthConvert in ppp; rewrite insert_length in ppp; lia]. rewrite pushNumberSet2 /update.
assert (red : forall _0,
( match
@decide (@eq varsfuncdef_0__ancestor _0 vardef_0__ancestor_work)
(@decide_rel varsfuncdef_0__ancestor varsfuncdef_0__ancestor
(@eq varsfuncdef_0__ancestor)
variableIndexEqualityDecidablevarsfuncdef_0__ancestor _0
vardef_0__ancestor_work)
with |left _ =>
@nth_lt (arrayType arrayIndex0 environment0 arraydef_0__dsu)
(convertToArray
(@insert nat Slot (list Slot) (@list_insert Slot)
(Z.to_nat a)
(ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))) dsu))
(Z.to_nat a) ppp
| right _ => match _0 with
| vardef_0__ancestor_vertex | _ => a
end end) = match _0 with | vardef_0__ancestor_work => nth_lt
(convertToArray
- rewrite !leftIdentity dropWithinLoopLiftToWithinLoop. unfold numberLocalGet at 1. rewrite -!bindAssoc pushNumberGet2 !leftIdentity. unfold retrieve at 1. rewrite pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Retrieve ra. case_decide as ppp; [| rewrite lengthConvert in ppp; lia]. rewrite pushNumberSet2 dropWithinLoopLiftToWithinLoop. unfold numberLocalGet at 1. rewrite -!bindAssoc pushNumberGet2. rewrite (ltac:(cbv) : update _ _ _ vardef_0__ancestor_work = a). { easy. } rewrite !leftIdentity. unfold retrieve at 1. rewrite pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Retrieve. case_decide as nnn; [| simpl in nnn; lia]. rewrite pushDispatch2 (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Store. rewrite (ltac:(simpl; reflexivity) : forall xx, nth_lt [xx] _ nnn = xx) insertConvertReferTo. { rewrite ra. lia. } { lia. } rewrite Nat2Z.id.
have red: (update
(λ _0 : varsfuncdef_0__ancestor,
match _0 with
| vardef_0__ancestor_vertex => whatever
| vardef_0__ancestor_work => a
end) vardef_0__ancestor_vertex
(nth_lt (convertToArray dsu) (Z.to_nat a) ppp)) = fun x => match x with | vardef_0__ancestor_vertex => nth_lt (convertToArray dsu) (Z.to_nat a) ppp | _ => a end.
{ apply functional_extensionality_dep. intro g. destruct g; easy. }
rewrite red. clear red.
rewrite dropWithinLoopLiftToWithinLoop. unfold numberLocalGet at 1. rewrite -!bindAssoc pushNumberGet2. unfold numberLocalSet at 1. rewrite pushNumberSet2 (nth_lt_default _ _ _ 0%Z).
destruct hh as [hh | hh]; [| simpl in hhh; pose proof oneLeqLeafCount hh; lia]. clear nnn ppp xxx. rewrite ra lengthConvert. case_decide as mww; [| lia]; clear mww. rewrite (ltac:(easy) : dropWithinLoop (Done _ _ _ _) = Done _ _ _ _) leftIdentity.
have red : (λ _0 : arrayIndex0,
match decide (_0 = arraydef_0__dsu) with
| left _1 =>
@eq_rect_r arrayIndex0 arraydef_0__dsu
(fun _2 : arrayIndex0 =>
list (arrayType arrayIndex0 environment0 _2))
(convertToArray
(@insert nat Slot (list Slot) (@list_insert Slot)
(Z.to_nat a)
(ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))) dsu))
_0 _1
| right _ =>
match
_0 as _2 return (list (arrayType arrayIndex0 environment0 _2))
with
| arraydef_0__dsu => convertToArray dsu
| arraydef_0__hasBeenInitialized => [1%Z]
| arraydef_0__result =>
[Z.of_nat (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]
end
end) = fun x => match x with | arraydef_0__dsu => convertToArray
(<[Z.to_nat a:=ReferTo
(ancestor dsu (Z.to_nat 100) (Z.to_nat a))]>
dsu)) (Z.to_nat a) ppp | _ => a end).
{ intro g. destruct g; easy. }
have red2 := functional_extensionality_dep _ _ red.
rewrite red2. clear red red2. rewrite (nth_lt_default _ _ _ 0%Z) nthConvert. { rewrite insert_length. lia. } rewrite nth_lookup list_lookup_insert. { lia. } rewrite (ltac:(simpl; reflexivity) : default _ (Some _) = _).
dsu)
| arraydef_0__hasBeenInitialized => [1%Z]
| arraydef_0__result =>
[Z.of_nat (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]
end.
{ apply functional_extensionality_dep. intro g. destruct g; easy. }
rewrite red. clear red.
rewrite nthConvert. { lia. } rewrite hhh.
have red : (update
(λ _0 : varsfuncdef_0__ancestor,
match _0 with
| vardef_0__ancestor_vertex => Z.of_nat hh
| vardef_0__ancestor_work => a
end) vardef_0__ancestor_work (Z.of_nat hh)) = fun x => match x with
| vardef_0__ancestor_vertex => Z.of_nat hh
| vardef_0__ancestor_work => Z.of_nat hh
end.
{ apply functional_extensionality_dep. intro g. destruct g; easy. }
rewrite red. clear red.
have red1 : noIllegalIndices
(<[Z.to_nat a:=ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]> dsu).
{ clear hs. intros a1 a2 a3. destruct (decide (a1 = Z.to_nat a)) as [hs | hs]. { rewrite -> nth_lookup, <- hs, list_lookup_insert in a3; [| lia]. rewrite (ltac:(simpl; reflexivity) : default _ (Some _) = _) in a3. rewrite insert_length. pose proof (ltac:(clear; intros a b h; injection h; easy) : forall a b, ReferTo a = ReferTo b -> a = b) _ _ a3 as a4. rewrite <- a4. apply ancestorLtLength; (assumption || lia). } rewrite insert_length. rewrite nth_lookup list_lookup_insert_ne in a3. { lia. } rewrite <- (nth_lookup _ _ (Ancestor Unit)) in a3. pose proof h1 _ _ a3. lia. }
have red2 : Z.to_nat
(dsuLeafCount
(<[Z.to_nat a:=ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]> dsu)) =
length
(<[Z.to_nat a:=ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]> dsu).
{ unfold dsuLeafCount. rewrite Nat2Z.id insert_length insert_take_drop. { lia. } rewrite (ltac:(intros; listsEqual) : forall a b, a :: b = [a] ++ b) !map_app !list_sum_app.
assert (hst : list_sum
(map
(λ _1 : Slot,
match _1 with
| ReferTo _ => 0
| Ancestor _2 => leafCount _2
end) [ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]) = list_sum
(map
(λ _1 : Slot,
match _1 with
| ReferTo _ => 0
| Ancestor _2 => leafCount _2
end) [nth (Z.to_nat a) dsu (Ancestor Unit)])).
{ rewrite hhh. easy. } rewrite hst. clear hst. rewrite -!list_sum_app -!map_app -(ltac:(intros; listsEqual) : forall a b, a :: b = [a] ++ b) nthConsDrop; try lia. { intro cona. rewrite cona in hL; simpl in hL; lia. } rewrite take_drop. unfold dsuLeafCount in hL1. rewrite Nat2Z.id in hL1. exact hL1. }
have red3 : withoutCyclesN
(<[Z.to_nat a:=ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]> dsu)
(length
(<[Z.to_nat a:=ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]> dsu)).
{ intros b c. rewrite insert_length in c. rewrite insert_length (ltac:(lia) : Z.to_nat 100%Z = length dsu) -ancestorInsert; try (assumption || lia). { rewrite hhh. easy. }
destruct (decide (ancestor dsu (length dsu) b = Z.to_nat a)) as [hw | hw].
- pose proof h2 b c as st. rewrite hw hhh in st. exfalso. exact st.
- rewrite nth_lookup list_lookup_insert_ne. { lia. } rewrite <- (nth_lookup _ _ (Ancestor Unit)). pose proof h2 b c. assumption. }
pose proof IH ltac:(lia) (Z.of_nat hh) ltac:(lia) ltac:(pose proof h1 _ _ hhh; lia) (<[Z.to_nat a:=ReferTo (ancestor dsu (Z.to_nat 100) (Z.to_nat a))]> dsu) red1 ltac:(rewrite -> insert_length; lia) red2 red3 (Z.of_nat hh) as ffi.
rewrite dropWithinLoopLiftToWithinLoop -!bindAssoc in ffi.
assert (closer : Z.of_nat
(ancestor
(<[Z.to_nat a:=ReferTo
(ancestor dsu (Z.to_nat 100) (Z.to_nat a))]>
dsu) (Z.to_nat 100) (Z.to_nat (Z.of_nat hh))) = Z.of_nat (ancestor dsu (Z.to_nat 100) (Z.to_nat a))).
{ rewrite !(ltac:(lia) : Z.to_nat 100%Z = length dsu) Nat2Z.id -ancestorInsert; try (assumption || lia). { pose proof h1 _ _ hhh. lia. } { rewrite hhh. easy. }
assert (subtask : ancestor dsu (length dsu) (Z.to_nat a) = ancestor dsu (S (length dsu - 1)) (Z.to_nat a)). { rewrite (ltac:(lia) : S (length dsu - 1) = length dsu). reflexivity. } rewrite subtask. simpl. rewrite hhh.
pose proof h2 (Z.to_nat a) ltac:(lia) as subtask2. rewrite subtask in subtask2. simpl in subtask2. rewrite hhh in subtask2.
assert (subtask3 : ancestor dsu (length dsu) hh = ancestor dsu (S (length dsu - 1)) hh). { rewrite (ltac:(lia) : S (length dsu - 1) = length dsu). reflexivity. } rewrite subtask3.
pose proof h1 (Z.to_nat a) _ hhh as lh.
pose proof validChainAncestorChain dsu (length dsu - 1) hh ltac:(lia) h1 as mh.
epose proof validChainAncestorLength dsu (ancestorChain dsu (length dsu - 1) hh) h1 ltac:(split; try assumption; rewrite ancestorEqLastAncestorChain; destruct (nth (ancestor dsu (length dsu - 1) hh) dsu (Ancestor Unit)) as [xx | xx]; try (exfalso; exact subtask2); exists xx; reflexivity) hh ltac:(clear; destruct (length dsu - 1); simpl; try reflexivity; destruct (nth hh dsu (Ancestor Unit)); easy) as nh. rewrite -subtask3 -ancestorEqLastAncestorChain -nh ancestorEqLastAncestorChain. reflexivity. }
rewrite closer in ffi. rewrite ffi.
Admitted.

Lemma runAncestor (dsu : list Slot) (hL : length dsu = 100) (hL1 : Z.to_nat (dsuLeafCount dsu) = length dsu) (h1 : noIllegalIndices dsu) (h2 : withoutCyclesN dsu (length dsu)) (a : Z) (hLe1 : Z.le 0 a) (hLt1 : Z.lt a 100) communication continuation whatever : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state
Expand Down

0 comments on commit 4b20f96

Please sign in to comment.