Weierstrass curve is a group

5 files changed, 212 insertions, 230 deletions

diff --git a/_CoqProject b/_CoqProject
index b50e07652..ae6eaef6a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -489,3 +489,4 @@ src/Util/Tactics/SplitInContext.v
 src/Util/Tactics/UniquePose.v
 src/Util/Tactics/VM.v
 src/WeierstrassCurve/Pre.v
+src/WeierstrassCurve/WeierstrassCurveTheorems.v
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index ddd2737a3..73a004cb3 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Util.Relations Crypto.Util.Tactics.
+Require Import Crypto.Util.Relations Crypto.Util.Tactics Crypto.Util.Notations.
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
 Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
 Require Coq.setoid_ring.Field_theory.
@@ -385,6 +385,30 @@ Module _fsatz_test.
 
     Lemma fractional_equation_no_solution x (A:x<>1) (B:x<>opp two) (C:x*x+x <> two) (X:nine/(x*x + x - two) = opp three/(x+two) + seven*inv(x-1)) : False.
     Proof. fsatz. Qed.
+
+    Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x^2*x).
+    Lemma weierstrass_associativity_main a b x1 y1 x2 y2 x4 y4
+          (A: y1^2=x1^3+a*x1+b)
+          (B: y2^2=x2^3+a*x2+b)
+          (C: y4^2=x4^3+a*x4+b)
+          (Hi3: x2 <> x1)
+          λ3 (Hλ3: λ3 = (y2-y1)/(x2-x1))
+          x3 (Hx3: x3 = λ3^2-x1-x2)
+          y3 (Hy3: y3 = λ3*(x1-x3)-y1)
+          (Hi7: x4 <> x3)
+          λ7 (Hλ7: λ7 = (y4-y3)/(x4-x3))
+          x7 (Hx7: x7 = λ7^2-x3-x4)
+          y7 (Hy7: y7 = λ7*(x3-x7)-y3)
+          (Hi6: x4 <> x2)
+          λ6 (Hλ6: λ6 = (y4-y2)/(x4-x2))
+          x6 (Hx6: x6 = λ6^2-x2-x4)
+          y6 (Hy6: y6 = λ6*(x2-x6)-y2)
+          (Hi9: x6 <> x1)
+          λ9 (Hλ9: λ9 = (y6-y1)/(x6-x1))
+          x9 (Hx9: x9 = λ9^2-x1-x6)
+          y9 (Hy9: y9 = λ9*(x1-x9)-y1)
+      : x7 = x9 /\ y7 = y9.
+    Proof. split; fsatz. Qed.
   End _test.
 End _fsatz_test.
 
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index 3f8ab2100..7f4b66d46 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -43,29 +43,26 @@ Module W.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Notation "2" := (1+1). Local Notation "3" := (1+2). 
 
-    Program Definition add (P1 P2:point) : point
-      := exist
-           _
-           (match coordinates P1, coordinates P2 return _ with
-            | (x1, y1), (x2, y2) =>
-              if x1 =? x2
-              then
-                if y2 =? -y1
-                then ∞
-                else let k := (3*x1^2+a)/(2*y1) in
-                     let x3 := k^2-x1-x1 in
-                     let y3 := k*(x1-x3)-y1 in
-                     (x3, y3)
-              else let k := (y2-y1)/(x2-x1) in
-                   let x3 := k^2-x1-x2 in
-                   let y3 := k*(x1-x3)-y1 in
-                   (x3, y3)
-            | ∞, ∞ => ∞
-            | ∞, _ => coordinates P2
-            | _, ∞ => coordinates P1
-            end)
-           _.
-    Next Obligation. Admitted.
+    Program Definition add (P1 P2:point) : point  := exist _
+      (match coordinates P1, coordinates P2 return _ with
+       | (x1, y1), (x2, y2) =>
+         if x1 =? x2
+         then
+           if y2 =? -y1
+           then ∞
+           else let k := (3*x1^2+a)/(2*y1) in
+                let x3 := k^2-x1-x1 in
+                let y3 := k*(x1-x3)-y1 in
+                (x3, y3)
+         else let k := (y2-y1)/(x2-x1) in
+              let x3 := k^2-x1-x2 in
+              let y3 := k*(x1-x3)-y1 in
+              (x3, y3)
+       | ∞, ∞ => ∞
+       | ∞, _ => coordinates P2
+       | _, ∞ => coordinates P1
+       end) _.
+    Next Obligation. exact (Pre.add_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed.
 
     Fixpoint mul (n:nat) (P : point) : point :=
       match n with
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v
index c33d14691..b809aa0b4 100644
--- a/src/WeierstrassCurve/Pre.v
+++ b/src/WeierstrassCurve/Pre.v
@@ -9,13 +9,16 @@ Local Open Scope core_scope.
 
 Generalizable All Variables.
 Section Pre.
-  Context {F eq zero one opp add sub mul inv div} {field:@field F eq zero one opp add sub mul inv div} {eq_dec: DecidableRel eq} {char_gt_2:@Ring.char_gt F eq zero one opp add sub mul 2%N}.
-  Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
-  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-  Local Notation "0" := zero.  Local Notation "1" := one.
-  Local Infix "+" := add. Local Infix "*" := mul.
-  Local Infix "-" := sub. Local Infix "/" := div.
-  Local Notation "- x" := (opp x).
+  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+          {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+          {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2%N}
+          {eq_dec: DecidableRel Feq}.
+  Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)).
+  Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+  Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+  Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+  Local Notation "- x" := (Fopp x).
   Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2).
   Local Notation "'∞'" := unit : type_scope.
   Local Notation "'∞'" := (inr tt) : core_scope.
@@ -26,31 +29,34 @@ Section Pre.
   Context {b:F}.
 
   (* the canonical definitions are in Spec *)
-  Definition onCurve (P:F*F + ∞) := match P with
-                                    | (x, y) => y^2 = x^3 + a*x + b
-                                    | ∞ => True
-                                    end.
-  Definition unifiedAdd' (P1' P2':F*F + ∞) : F*F + ∞ :=
-    match P1', P2' with
-    | (x1, y1), (x2, y2)
-      => if dec (x1 = x2) then
-           if dec (y2 = -y1) then
-             ∞
-           else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1,
-                   (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1)
-         else
-           ((y2-y1)^2 / (x2-x1)^2 - x1 - x2,
-            (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1)
+  Let onCurve (P:F*F + ∞) := match P with
+                             | (x, y) => y^2 = x^3 + a*x + b
+                             | ∞ => True
+                             end.
+  Let add (P1' P2':F*F + ∞) : F*F + ∞ :=
+    match P1', P2' return _ with
+    | (x1, y1), (x2, y2) =>
+      if dec (x1 = x2)
+      then
+        if dec (y2 = -y1)
+        then ∞
+        else let k := (3*x1^2+a)/(2*y1) in
+             let x3 := k^2-x1-x1 in
+             let y3 := k*(x1-x3)-y1 in
+             (x3, y3)
+      else let k := (y2-y1)/(x2-x1) in
+           let x3 := k^2-x1-x2 in
+           let y3 := k*(x1-x3)-y1 in
+           (x3, y3)
     | ∞, ∞ => ∞
     | ∞, _ => P2'
     | _, ∞ => P1'
     end.
 
-  Lemma unifiedAdd'_onCurve P1 P2 
-    (O1:onCurve P1) (O2:onCurve P2) : onCurve (unifiedAdd' P1 P2).
+  Lemma add_onCurve P1 P2 (_:onCurve P1) (_:onCurve P2) :
+    onCurve (add P1 P2).
   Proof.
     destruct_head' sum; destruct_head' prod;
-      cbv [onCurve unifiedAdd'] in *; break_match;
-        trivial; [|]; setoid_subst_rel eq; fsatz.
+      cbv [onCurve add] in *; break_match; trivial; [|]; fsatz.
   Qed.
 End Pre.
diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
index bc99c5e16..4a3f54154 100644
--- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v
+++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
@@ -9,7 +9,7 @@ Module W.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
             {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2}
-            {char_gt_10000:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 10000} (* TODO: we need only 3, but we may need to factor some coefficients *)
+            {char_huge:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 35481600} (* TODO: we need only 3, but we may need to factor some coefficients *)
             {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
@@ -23,11 +23,34 @@ Module W.
     Local Notation "16" := (1+(1+(1+(1+12)))). Local Notation "20" := (1+(1+(1+(1+16)))).
     Local Notation "24" := (1+(1+(1+(1+20)))). Local Notation "27" := (1+(1+(1+24))).
     Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30).
+    Context {discriminant_nonzero:4*a^3 + 27*b^2 <> 0}.
+
+    Lemma same_x_same_y
+          (xA yA : F)
+          (A : yA ^ 2 = xA ^ 3 + a * xA + b)
+          (xB yB : F)
+          (B : yB ^ 2 = xB ^ 3 + a * xB + b)
+          (Hx: xA = xB)
+          (Hy:yB <> Fopp yA)
+      : yB = yA.
+    Proof. fsatz. Qed.
+
+    Definition is_redundant {T} (x:T) := x.
+    Global Arguments is_redundant : simpl never.
+    Ltac clear_marked_redundant :=
+      repeat match goal with
+               [H:?P, Hr:is_redundant ?P |- _] => clear H Hr
+             end.
 
     Ltac t_step :=
       match goal with
       | _ => exact _
       | _ => intro
+      | [ A : ?yA ^ 2 = ?xA ^ 3 + a * ?xA + b,
+              B : ?yB ^ 2 = ?xB ^ 3 + a * ?xB + b,
+                  Hx: ?xA = ?xB,
+                      Hy: ?yB <> Fopp ?yA
+          |- _] => unique pose proof (same_x_same_y _ _ A _ _ B Hx Hy)
       | |- Equivalence _ => split
       | |- abelian_group => split | |- group => split | |- monoid => split
       | |- is_associative => split | |- is_commutative => split 
@@ -38,191 +61,122 @@ Module W.
       | _ => progress destruct_head' prod
       | _ => progress destruct_head' unit
       | _ => progress destruct_head' and
+      | |- context[?P] =>
+        unique pose proof (proj2_sig P);
+        unique pose proof (proj2_sig P:(is_redundant _))
       | _ => progress cbv [eq W.eq W.add W.coordinates proj1_sig] in *
-      (* [_gather_nonzeros] must run before [fst_pair] or [simpl] but after splitting E.eq and unfolding [E.add] *)
       | _ => progress simpl in *
+      | _ => progress break_match
       | |- _ /\ _ => split | |- _ <-> _ => split
-      | _ => solve [trivial]
+      | _ => abstract (trivial || contradiction || clear_marked_redundant; fsatz)
       end.
     Ltac t := repeat t_step.
 
-    (*
-    Lemma weierstrass_associativity_main x1 y1 x2 y2 x4 y4
-          (A: y1^2=x1^3+a*x1+b)
-          (B: y2^2=x2^3+a*x2+b)
-          (C: y4^2=x4^3+a*x4+b)
-          (Hi3: x2 <> x1)
-          λ3 (Hλ3: λ3 = (y2-y1)/(x2-x1))
-          x3 (Hx3: x3 = λ3^2-x1-x2)
-          y3 (Hy3: y3 = λ3*(x1-x3)-y1)
-          (Hi7: x4 <> x3)
-          λ7 (Hλ7: λ7 = (y4-y3)/(x4-x3))
-          x7 (Hx7: x7 = λ7^2-x3-x4)
-          y7 (Hy7: y7 = λ7*(x3-x7)-y3)
-          (Hi6: x4 <> x2)
-          λ6 (Hλ6: λ6 = (y4-y2)/(x4-x2))
-          x6 (Hx6: x6 = λ6^2-x2-x4)
-          y6 (Hy6: y6 = λ6*(x2-x6)-y2)
-          (Hi9: x6 <> x1)
-          λ9 (Hλ9: λ9 = (y6-y1)/(x6-x1))
-          x9 (Hx9: x9 = λ9^2-x1-x6)
-          y9 (Hy9: y9 = λ9*(x1-x9)-y1)
-      : x7 = x9 /\ y7 = y9.
-    Proof. split; fsatz. Qed.
-    *)
-
-    Definition opaque_id {T} := @id T.
-    Local Opaque opaque_id.
-    
-    Global Instance associative_add : is_associative(eq:=W.eq)(op:=W.add).
-    Proof.
-      (* the automation currently does not pick up
-       that x1 = x2 and y2 =? -y1 implies that y2 = y1 *)
-      split; intros [[[xA yA]|] A] [[[xB yB]|] B] [[[xC yC]|] C].
-      repeat (break_match || t).
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      { rewrite <-H in *; clear H xC.
-        rewrite H0 in *; clear H0 yC C.
-        assert (yB = ((yB - yA) / (xB - xA) * (xA - (((yB - yA) / (xB - xA)) ^ 2 - xA - xB)) -
-          yA)) by fsatz; clear H3.
-        symmetry in H2.
-        (* A+B = B? But A is a point with coordinates, not the identity *)
-        admit. }
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      { assert (yC = yB) by fsatz.
-        symmetry in H.
-        setoid_subst_rel Feq.
-
-        assert (yA<>Fopp((3 * xB ^ 2 + a) / (2 * yB) * (xB - (((3 * xB ^ 2 + a) / (2 * yB)) ^ 2 - xB - xB)) - yB)) by fsatz; clear H2.
-        destruct(dec((yA=((3 * xB ^ 2 + a) / (2 * yB) * (xB - (((3 * xB ^ 2 + a) / (2 * yB)) ^ 2 - xB - xB)) - yB)))). fsatz.
-        assert (yA^2 = ((3 * xB ^ 2 + a) / (2 * yB) *
-      (xB - (((3 * xB ^ 2 + a) / (2 * yB)) ^ 2 - xB - xB)) - yB)^2) by fsatz.
-        only_two_square_roots. }
-      { assert (yC = yB) by fsatz.
-        symmetry in H.
-        setoid_subst_rel Feq.
-
-        assert (yA<>Fopp((3 * xB ^ 2 + a) / (2 * yB) * (xB - (((3 * xB ^ 2 + a) / (2 * yB)) ^ 2 - xB - xB)) - yB)) by fsatz; clear H2.
-        destruct(dec((yA=((3 * xB ^ 2 + a) / (2 * yB) * (xB - (((3 * xB ^ 2 + a) / (2 * yB)) ^ 2 - xB - xB)) - yB)))). fsatz.
-        assert (yA^2 = ((3 * xB ^ 2 + a) / (2 * yB) *
-      (xB - (((3 * xB ^ 2 + a) / (2 * yB)) ^ 2 - xB - xB)) - yB)^2) by fsatz.
-        only_two_square_roots. }
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      { rewrite H3 in *; clear H3.
-        rewrite <-H2 in *; clear H2.
-        replace (Fopp yA ^ 2) with (yA^2) in * by admit.
-        clear B xB yB.
-        assert ((yC - Fopp yA) / (xC - xA) * (xA - (((yC - Fopp yA) / (xC - xA)) ^ 2 - xA - xC))=0) by fsatz; clear H1.
-        admit.
-        }
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      { 
-        assert (yA = (yC - yB) / (xC - xB) * (xB - (((yC - yB) / (xC - xB)) ^ 2 - xB - xC)) - yB) by admit.
-        assert (yC = 
-         ((yB - yA) / (xB - xA) *
-          (xA - (((yB - yA) / (xB - xA)) ^ 2 - xA - xB)) - yA)) by admit.
-        fsatz. }
-
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      { 
-        assert (yC = ((yB - yA) / (xB - xA) * (xA - (((yB - yA) / (xB - xA)) ^ 2 - xA - xB)) - yA)) by admit.
-        assert (yA = (yC - yB) / (xC - xB) * (xB - (((yC - yB) / (xC - xB)) ^ 2 - xB - xC)) - yB) by admit.
-        fsatz. }
-      { assert (yA = (yC - yB) / (xC - xB) * (xB - (((yC - yB) / (xC - xB)) ^ 2 - xB - xC)) - yB) by admit.
-        fsatz. }
-      { assert (yA = (yC - yB) / (xC - xB) * (xB - (((yC - yB) / (xC - xB)) ^ 2 - xB - xC)) - yB) by admit. fsatz. }
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-      fsatz.
-    Admitted.
+    Program Definition inv (P:point) : point
+      := exist
+           _
+           (match W.coordinates P return _ with
+            | inl (x1, y1) => inl (x1, Fopp y1)
+            | _ => P
+            end)
+           _.
+    Next Obligation. t. Qed.
 
+    Global Instance commutative_group : abelian_group(eq:=W.eq)(op:=W.add)(id:=W.zero)(inv:=inv).
+    Proof. Time t. Time Qed.
   End W.
 End W.
+
+(*
+Times for individual subgoal of the associativity proof:
+Finished transaction in 0.169 secs (0.17u,0.s) (successful)
+Finished transaction in 0.16 secs (0.159u,0.s) (successful)
+Finished transaction in 0.722 secs (0.723u,0.s) (successful)
+Finished transaction in 3.375 secs (3.373u,0.003s) (successful)
+Finished transaction in 7.166 secs (7.166u,0.s) (successful)
+Finished transaction in 1.862 secs (1.856u,0.003s) (successful)
+Finished transaction in 3.6 secs (3.603u,0.s) (successful)
+Finished transaction in 0.571 secs (0.569u,0.s) (successful)
+Finished transaction in 1.956 secs (1.959u,0.s) (successful)
+Finished transaction in 3.186 secs (3.186u,0.s) (successful)
+Finished transaction in 1.265 secs (1.266u,0.s) (successful)
+Finished transaction in 1.884 secs (1.883u,0.s) (successful)
+Finished transaction in 0.762 secs (0.763u,0.s) (successful)
+Finished transaction in 2.431 secs (2.433u,0.s) (successful)
+Finished transaction in 1.662 secs (1.663u,0.s) (successful)
+Finished transaction in 1.846 secs (1.846u,0.s) (successful)
+Finished transaction in 1.853 secs (1.853u,0.s) (successful)
+Finished transaction in 1.727 secs (1.73u,0.s) (successful)
+Finished transaction in 1.771 secs (1.769u,0.s) (successful)
+Finished transaction in 2.07 secs (2.073u,0.s) (successful)
+Finished transaction in 5.765 secs (5.766u,0.s) (successful)
+Finished transaction in 9.965 secs (9.966u,0.s) (successful)
+Finished transaction in 3.917 secs (3.916u,0.s) (successful)
+Finished transaction in 6.101 secs (6.099u,0.003s) (successful)
+Finished transaction in 2.042 secs (2.043u,0.s) (successful)
+Finished transaction in 5.398 secs (5.399u,0.s) (successful)
+Finished transaction in 6.346 secs (6.346u,0.s) (successful)
+Finished transaction in 4.726 secs (4.726u,0.s) (successful)
+Finished transaction in 5.872 secs (5.876u,0.s) (successful)
+Finished transaction in 1.852 secs (1.853u,0.s) (successful)
+Finished transaction in 3.189 secs (3.189u,0.s) (successful)
+Finished transaction in 1.489 secs (1.49u,0.s) (successful)
+Finished transaction in 6.602 secs (6.603u,0.s) (successful)
+Finished transaction in 12.172 secs (12.169u,0.003s) (successful)
+Finished transaction in 4.668 secs (4.669u,0.s) (successful)
+Finished transaction in 8.451 secs (8.449u,0.003s) (successful)
+Finished transaction in 1.304 secs (1.303u,0.s) (successful)
+Finished transaction in 4.818 secs (4.816u,0.003s) (successful)
+Finished transaction in 7.557 secs (7.559u,0.s) (successful)
+Finished transaction in 4.435 secs (4.436u,0.s) (successful)
+Finished transaction in 7.915 secs (7.916u,0.s) (successful)
+Finished transaction in 0.623 secs (0.623u,0.s) (successful)
+Finished transaction in 2.145 secs (2.146u,0.s) (successful)
+Finished transaction in 1.436 secs (1.436u,0.s) (successful)
+Finished transaction in 2.091 secs (2.09u,0.s) (successful)
+Finished transaction in 1.459 secs (1.46u,0.s) (successful)
+Finished transaction in 1.371 secs (1.373u,0.s) (successful)
+Finished transaction in 1.417 secs (1.416u,0.s) (successful)
+Finished transaction in 1.757 secs (1.756u,0.s) (successful)
+Finished transaction in 5.275 secs (5.276u,0.s) (successful)
+Finished transaction in 8.736 secs (8.736u,0.s) (successful)
+Finished transaction in 3.415 secs (3.416u,0.s) (successful)
+Finished transaction in 5.508 secs (5.506u,0.003s) (successful)
+Finished transaction in 1.881 secs (1.883u,0.s) (successful)
+Finished transaction in 21.631 secs (21.629u,0.003s) (successful)
+Finished transaction in 312.734 secs (312.723u,0.036s) (successful)
+Finished transaction in 4.439 secs (4.436u,0.s) (successful)
+Finished transaction in 6.267 secs (6.266u,0.003s) (successful)
+Finished transaction in 1.241 secs (1.24u,0.s) (successful)
+Finished transaction in 1.603 secs (1.603u,0.s) (successful)
+Finished transaction in 1.824 secs (1.823u,0.s) (successful)
+Finished transaction in 8.099 secs (8.099u,0.s) (successful)
+Finished transaction in 16.461 secs (16.456u,0.003s) (successful)
+Finished transaction in 4.722 secs (4.723u,0.s) (successful)
+Finished transaction in 9.305 secs (9.306u,0.s) (successful)
+Finished transaction in 1.398 secs (1.396u,0.s) (successful)
+Finished transaction in 4.721 secs (4.723u,0.s) (successful)
+Finished transaction in 7.226 secs (7.226u,0.s) (successful)
+Finished transaction in 3.282 secs (3.283u,0.s) (successful)
+Finished transaction in 4.536 secs (4.539u,0.s) (successful)
+Finished transaction in 0.379 secs (0.38u,0.s) (successful)
+Finished transaction in 0.438 secs (0.436u,0.s) (successful)
+Finished transaction in 0.323 secs (0.326u,0.s) (successful)
+Finished transaction in 0.372 secs (0.369u,0.s) (successful)
+Finished transaction in 0.378 secs (0.376u,0.s) (successful)
+Finished transaction in 0.438 secs (0.44u,0.s) (successful)
+Finished transaction in 0.33 secs (0.329u,0.s) (successful)
+Finished transaction in 0.368 secs (0.369u,0.s) (successful)
+Finished transaction in 0.088 secs (0.086u,0.s) (successful)
+Finished transaction in 0.087 secs (0.09u,0.s) (successful)
+Finished transaction in 0.371 secs (0.369u,0.s) (successful)
+Finished transaction in 0.441 secs (0.44u,0.s) (successful)
+Finished transaction in 0.322 secs (0.319u,0.s) (successful)
+Finished transaction in 0.37 secs (0.373u,0.s) (successful)
+Finished transaction in 0.089 secs (0.086u,0.s) (successful)
+Finished transaction in 0.091 secs (0.093u,0.s) (successful)
+Finished transaction in 0.088 secs (0.089u,0.s) (successful)
+Finished transaction in 0.086 secs (0.086u,0.s) (successful)
+
+Finished transaction in 268.648 secs (268.609u,0.096s) (successful)
+*)
\ No newline at end of file