Generalize initial blockchain state

huynhtrankhanh · Nov 4, 2024 · 413a532 · 413a532
1 parent 593d136
commit 413a532
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 8 deletions.
diff --git a/theories/DisjointSetUnionCode.v b/theories/DisjointSetUnionCode.v
@@ -786,7 +786,7 @@ end
 end)). { apply functional_extensionality_dep. intro x. destruct x; simpl; easy. } rewrite <- hh. clear hh. rewrite !(ltac:(cbv; reflexivity) : (coerceInt (coerceInt (Z.opp 1) 64) 8) = 255%Z) in previous. rewrite previous. rewrite insert_take_drop; [| lia]. rewrite (ltac:(lia) : Z.to_nat (100 - Z.of_nat n - 1) = 100 - S n). rewrite (ltac:(intros; listsEqual) : forall a b c, a ++ b :: c = (a ++ [b]) ++ c). pose proof take_app_length (take (100 - S n) l ++ [255%Z]) (drop (S (100 - S n)) l) as step. rewrite app_length in step. rewrite (ltac:(easy) : length [255%Z] = 1) in step. rewrite take_length in step. rewrite (ltac:(lia) : (100 - S n) `min` length l = 100 - S n) in step. rewrite (ltac:(lia) : 100 - S n + 1 = 100 - n) in step. rewrite step. clear step. rewrite (ltac:(intros; listsEqual) : forall a b c, (a ++ [b]) ++ c = a ++ (b :: c)). rewrite (ltac:(easy) : _ :: repeat _ _ = repeat 255%Z (S n)). case_decide as hIf; [reflexivity |]. pose proof (ltac:(lia) : @length (arrayType arrayIndex0 environment0 arraydef_0__dsu) l <= 100 - S n) as step. simpl in step. rewrite hL in step. lia.
 Qed.
 
-Lemma runAncestor1 (dsu : list Slot) (hL : length dsu = 100) (hM : Z.to_nat (dsuLeafCount dsu) = length dsu) (h1 : noIllegalIndices dsu) (h2 : withoutCyclesN dsu (length dsu)) (whatever2 a : Z) (hLe1 : Z.le 0 a) (hLt1 : Z.lt a 100) (communication : list Z) continuation continuation2 whatever n (hN : n <= 100) : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state
+Lemma runAncestor1 (dsu : list Slot) state1 state2 (hL : length dsu = 100) (hM : Z.to_nat (dsuLeafCount dsu) = length dsu) (h1 : noIllegalIndices dsu) (h2 : withoutCyclesN dsu (length dsu)) (whatever2 a : Z) (hLe1 : Z.le 0 a) (hLt1 : Z.lt a 100) (communication : list Z) continuation continuation2 whatever n (hN : n <= 100) : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state1 state2
   communication 1 arrayIndex0 arrayIndexEqualityDecidable0
   (arrayType arrayIndex0 environment0) (λ _0 : arrayIndex0,
   match
@@ -915,7 +915,7 @@ else
   (arrayType arrayIndex0 environment0)
   varsfuncdef_0__ancestor)
   withinLoopReturnValue ()
-  ())) >>= continuation) >>= continuation2) = invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state
+  ())) >>= continuation) >>= continuation2) = invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state1 state2
   communication 1 arrayIndex0 arrayIndexEqualityDecidable0
   (arrayType arrayIndex0 environment0) (λ _0 : arrayIndex0,
   match

diff --git a/theories/DisjointSetUnionCode2.v b/theories/DisjointSetUnionCode2.v
@@ -8,7 +8,7 @@ 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 whatever (n : nat) (hN : n <= 100) continuation : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state communication
+Lemma runCompressLoop (dsu : list Slot) state1 state2 (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 state1 state2 communication
   1 arrayIndex0 arrayIndexEqualityDecidable0
   (arrayType arrayIndex0 environment0)
   (λ _0 : arrayIndex0,
@@ -153,7 +153,7 @@ Lemma runCompressLoop (dsu : list Slot) (hL : length dsu = 100) (hL1 : Z.to_nat
                   (arrayType arrayIndex0 environment0)
                   varsfuncdef_0__ancestor) withLocalVariablesReturnValue ()
                ())) >>= continuation) =
-invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state state communication 1 arrayIndex0 arrayIndexEqualityDecidable0
+invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state1 state2 communication 1 arrayIndex0 arrayIndexEqualityDecidable0
   (arrayType arrayIndex0 environment0)
   (λ _0 : arrayIndex0,
      match
@@ -304,7 +304,7 @@ length
   { simpl. rewrite hhh anc. reflexivity. } rewrite -finale anc. reflexivity.
 Qed.
 
-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
+Lemma runAncestor (dsu : list Slot) state1 state2 (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 state1 state2
   communication 1 arrayIndex0 arrayIndexEqualityDecidable0
   (arrayType arrayIndex0 environment0) (λ _0 : arrayIndex0,
   match
@@ -329,7 +329,7 @@ end)
   (funcdef_0__ancestor (λ _ : varsfuncdef_0__ancestor, false)
   (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
+  (λ _ : varsfuncdef_0__ancestor, repeat 0%Z 20) >>= continuation) = invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state1 state2
   communication 1 arrayIndex0 arrayIndexEqualityDecidable0
   (arrayType arrayIndex0 environment0) (λ _0 : arrayIndex0,
   match
@@ -360,7 +360,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 communication g gg whatever (Z.to_nat 100%Z) ltac:(lia).
+  have av := fun g gg => runAncestor1 dsu state1 state2 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,
@@ -393,7 +393,22 @@ Proof.
 Qed.
 
 Lemma runUnite (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) : invokeContractAux (repeat 1%Z 20) (repeat 0%Z 20) 0 state
-  state [a; b] 1 arrayIndex0 arrayIndexEqualityDecidable0
+  (stateAfterInteractions (λ _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 => [0%Z]
+end)
+  (dsuScore
+  dsu)) [a; b] 1 arrayIndex0 arrayIndexEqualityDecidable0
   (arrayType arrayIndex0 environment0) (λ _0 : arrayIndex0,
   match
   _0 as _1