Skip to content

Commit

Permalink
Work on clearing the second loop
Browse files Browse the repository at this point in the history
  • Loading branch information
@huynhtrankhanh
huynhtrankhanh committed Nov 2, 2024
1 parent d54d0bd commit 8aa2241
Showing 1 changed file with 218 additions and 4 deletions.
222 changes: 218 additions & 4 deletions theories/DisjointSetUnionCode2.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,222 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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 b : Z) (hLe1 : Z.le 0 a) (hLt1 : Z.lt a 100) (hLe2 : Z.le 0 b) (hLt2 : Z.lt b 100) continuation whatever : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state
[a; b] 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 (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
_0 as _1 return (list (arrayType arrayIndex0 environment0 _1))
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) (funcdef_0__main xpred0 (fun=> 0%Z) (fun=> repeat 0%Z 20))
(eliminateLocalVariables xpred0
(λ _0 : varsfuncdef_0__ancestor,
match _0 with
| vardef_0__ancestor_vertex | _ => a
end) (fun=> repeat 0%Z 20)
(loop n
(fun=> dropWithinLoop
(liftToWithinLoop
(numberLocalGet arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor vardef_0__ancestor_work >>=
λ _0 : withLocalVariablesReturnValue
(NumberLocalGet arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
vardef_0__ancestor_work),
Done
(WithLocalVariables arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor)
withLocalVariablesReturnValue Z
(coerceInt _0 64) >>=
λ _1 : Z,
retrieve arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor arraydef_0__dsu _1 >>=
λ _2 : arrayType arrayIndex0 environment0
arraydef_0__dsu,
Done
(WithLocalVariables arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor)
withLocalVariablesReturnValue Z
(coerceInt 0 8) >>=
λ _3 : Z,
Done
(WithLocalVariables arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor)
withLocalVariablesReturnValue bool
(bool_decide (toSigned _2 8 < toSigned _3 8)%Z)) >>=
λ _0 : bool,
(if _0
then
break arrayIndex0 (arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor >>=
(fun=> Done
(WithinLoop arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor)
withinLoopReturnValue () ())
else
Done
(WithinLoop arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor) withinLoopReturnValue ()
()) >>=
(fun=> liftToWithinLoop
(numberLocalGet arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
vardef_0__ancestor_work >>=
λ _1 : withLocalVariablesReturnValue
(NumberLocalGet arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
vardef_0__ancestor_work),
Done
(WithLocalVariables arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor)
withLocalVariablesReturnValue Z
(coerceInt _1 64) >>=
λ _2 : Z,
retrieve arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
arraydef_0__result 0 >>=
[eta store arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
arraydef_0__dsu _2]) >>=
(fun=> liftToWithinLoop
(numberLocalGet arrayIndex0
(arrayType arrayIndex0 environment0)
varsfuncdef_0__ancestor
vardef_0__ancestor_work >>=
λ _1 : withLocalVariablesReturnValue
(NumberLocalGet arrayIndex0
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor
vardef_0__ancestor_work),
Done
(WithLocalVariables arrayIndex0
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor)
withLocalVariablesReturnValue Z
(coerceInt _1 64) >>=
λ _2 : Z,
retrieve arrayIndex0
(arrayType arrayIndex0
environment0)
varsfuncdef_0__ancestor
arraydef_0__dsu _2 >>=
[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)
varsfuncdef_0__ancestor) withLocalVariablesReturnValue ()
())) >>= continuation) =
invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state communication 1 arrayIndex0 arrayIndexEqualityDecidable0
(arrayType arrayIndex0 environment0)
(λ _0 : arrayIndex0,
match
_0 as _1 return (list (arrayType arrayIndex0 environment0 _1))
with
| arraydef_0__dsu =>
convertToArray
(pathCompress dsu n (Z.to_nat a)
(ancestor dsu (length dsu) (Z.to_nat a)))
| arraydef_0__hasBeenInitialized => [1%Z]
| arraydef_0__result =>
[Z.of_nat (ancestor dsu (length dsu) (Z.to_nat a))]
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.
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.
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].
rewrite (nth_lt_default _ _ _ 0%Z) nthConvert; [lia |]. rewrite (ltac:(easy) : (toSigned (coerceInt 0 8) 8 = 0)%Z).
have usk : toSigned
match nth (Z.to_nat a) dsu (Ancestor Unit) with
| ReferTo _0 => Z.of_nat _0
| Ancestor _0 => 256 - Z.of_nat (leafCount _0)
end 8 = match nth (Z.to_nat a) dsu (Ancestor Unit) with | ReferTo x => Z.of_nat x | Ancestor x => -Z.of_nat (leafCount x) end.
{ remember (nth (Z.to_nat a) dsu _) as hh eqn:hhh. symmetry in hhh. unfold toSigned. destruct hh as [hh | hh].
- pose proof h1 (Z.to_nat a) _ hhh. case_decide; lia.
- pose proof oneLeqLeafCount hh. case_decide; [| lia]. pose proof nthLowerBoundConvertAuxStep dsu ltac:(lia) ltac:(lia) (Z.to_nat a) ltac:(lia) _ hhh. lia. }
rewrite usk. clear usk. remember (nth (Z.to_nat a) dsu (Ancestor Unit)) as hh eqn:hhh. symmetry in hhh. case_bool_decide as hs.
- rewrite dropWithinLoop_4 !leftIdentity.
destruct hh as [hh | hh]. { lia. }
have red : pathCompress dsu (S n) (Z.to_nat a)
(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.

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
communication 1 arrayIndex0 arrayIndexEqualityDecidable0
(arrayType arrayIndex0 environment0) (λ _0 : arrayIndex0,
match
_0 as _1
Expand All @@ -34,7 +248,7 @@ end)
(update (λ _ : varsfuncdef_0__ancestor, 0%Z)
vardef_0__ancestor_vertex a)
(λ _ : varsfuncdef_0__ancestor, repeat 0%Z 20) >>= continuation) = invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state
[a; b] 1 arrayIndex0 arrayIndexEqualityDecidable0
communication 1 arrayIndex0 arrayIndexEqualityDecidable0
(arrayType arrayIndex0 environment0) (λ _0 : arrayIndex0,
match
_0 as _1
Expand Down Expand Up @@ -64,7 +278,7 @@ Proof.
vardef_0__ancestor_vertex)) = fun x => match x with | vardef_0__ancestor_vertex => a | vardef_0__ancestor_work => a end.
{ apply functional_extensionality_dep. intro x. destruct x; easy. }
move => h. rewrite h. clear h. rewrite leftIdentity.
have av := fun g gg => runAncestor1 dsu hL hL1 h1 h2 a a hLe1 hLt1 [a; b] g gg whatever (Z.to_nat 100%Z) ltac:(lia).
have av := fun g gg => runAncestor1 dsu hL hL1 h1 h2 a a hLe1 hLt1 communication g gg whatever (Z.to_nat 100%Z) ltac:(lia).
move : av. rewrite !leftIdentity !rightIdentity. move => av.
rewrite -bindAssoc av. unfold numberLocalGet at 1. rewrite pushNumberGet2. unfold store at 1. rewrite pushDispatch2. rewrite (ltac:(intros; simpl; reflexivity) : forall effect continuation f, Dispatch _ _ _ effect continuation >>= f = _) unfoldInvoke_S_Store. case_decide as xxx; [| simpl in xxx; lia]; clear xxx.
have jda : (λ _0 : arrayIndex0,
Expand Down

0 comments on commit 8aa2241

Please sign in to comment.