WIP

3 files changed, 81 insertions, 184 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 308879293..3539b18f1 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -9,51 +9,44 @@ Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.Tactics.
 Require Export Crypto.Util.FixCoqMistakes.
 
-Global Existing Instance E.char_gt_2.
-
 Module E.
   Import Group ScalarMult Ring Field CompleteEdwardsCurve.E.
 
   Notation onCurve_zero := Pre.onCurve_zero.
   Notation denominator_nonzero := Pre.denominator_nonzero.
-  Notation denominator_nonzero_x := denominator_nonzero_x.
+  Notation denominator_nonzero_x := Pre.denominator_nonzero_x.
   Notation denominator_nonzero_y := Pre.denominator_nonzero_y.
   Notation onCurve_add := Pre.onCurve_add.
 
-  (* used in Theorems and Homomorphism *)
-  Ltac _gather_nonzeros :=
-    match goal with
-      |- context[?t] =>
-      match type of t with
-        ?T =>
-        match type of T with
-          Prop =>
-          let T := (eval simpl in T) in
-          match T with
-            not (_ _ _) => unique pose proof (t:T)
-          end
-        end
-      end
-    end.
-
   Section CompleteEdwardsCurveTheorems.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {prm:@twisted_edwards_params F Feq Fzero Fone Fopp Fadd Fsub Fmul a d}
+            {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)}
             {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.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
     Local Notation "x ^ 2" := (x*x).
-    Local Notation point := (@point F Feq Fone Fadd Fmul a d).
-    Definition onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2).
-    (* TODO: remove uses of this defnition, then make it a local notation *)
-    Definition eq := @E.eq F Feq Fone Fadd Fmul a d.
+
+    Context {a d: F}
+            {nonzero_a : a <> 0}
+            {square_a : exists sqrt_a, sqrt_a^2 = a}
+            {nonsquare_d : forall x, x^2 <> d}.
+    
+    Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2).
+    Local Notation point := (@E.point F Feq Fone Fadd Fmul a d).
+    Local Notation eq    := (@E.eq F Feq Fone Fadd Fmul a d).
+    Local Notation zero  := (E.zero(nonzero_a:=nonzero_a)(d:=d)).
+    Local Notation add   := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+    Local Notation mul   := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+
+    Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)).
+    Next Obligation. destruct P as [ [??]?]; cbv; fsatz. Qed.
 
     Ltac t_step :=
       match goal with
-      | _ => exact _
+      | _ => solve [trivial | exact _ ]
       | _ => intro
       | |- Equivalence _ => split
       | |- abelian_group => split | |- group => split | |- monoid => split
@@ -63,34 +56,32 @@ Module E.
       | _ => progress destruct_head' @E.point
       | _ => progress destruct_head' prod
       | _ => progress destruct_head' and
-      | _ => progress cbv [onCurve eq E.eq E.add E.coordinates proj1_sig] in *
+      | |- context[E.add ?P ?Q] =>
+        unique pose proof (Pre.denominator_nonzero_x _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q));
+        unique pose proof (Pre.denominator_nonzero_y _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q))
+      | _ => progress cbv [opp E.zero E.eq E.add E.coordinates proj1_sig fieldwise fieldwise'] in *
       (* [_gather_nonzeros] must run before [fst_pair] or [simpl] but after splitting E.eq and unfolding [E.add] *)
-      | _ => _gather_nonzeros
-      | _ => progress simpl in *
       | |- _ /\ _ => split | |- _ <-> _ => split
-      | _ => solve [trivial]
       end.
     Ltac t := repeat t_step; fsatz.
 
-    Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)).
-    Next Obligation. t. Qed.
-
     Global Instance associative_add : is_associative(eq:=E.eq)(op:=add).
     Proof.
-      (* [fsatz] runs out of 6GB of stack space *)
+      (* [nsatz_compute] for a denominator runs out of 6GB of stack space *)
+      (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5359 *)
       Add Field _field : (Algebra.Field.field_theory_for_stdlib_tactic (T:=F)).
       Import Field_tac.
       repeat t_step; (field_simplify_eq; [IntegralDomain.nsatz|]); repeat split; trivial.
-      { intro. eapply H5. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
-      { intro. eapply H1. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
-      { intro. eapply H6. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
-      { intro. eapply H2. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+      { intro. eapply H3. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+      { intro. eapply H. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+      { intro. eapply H4. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
+      { intro. eapply H0. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. }
     Qed.
 
-    Global Instance edwards_curve_abelian_group : abelian_group (eq:=E.eq)(op:=add)(id:=zero)(inv:=opp).
+    Global Instance edwards_curve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
     Proof. t. Qed.
 
-    Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. t. Qed.
+    Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. repeat t_step. Qed.
 
     Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul.
     Proof.
@@ -116,19 +107,27 @@ Module E.
     End PointCompression.
   End CompleteEdwardsCurveTheorems.
   Section Homomorphism.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd}
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {Fprm:@twisted_edwards_params F Feq Fzero Fone Fopp Fadd Fsub Fmul Fa Fd}
+            {char_gt_2_F : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)}
             {Feq_dec:DecidableRel Feq}.
-    Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd}
+
+    Context {Fa Fd: F}
+            {nonzero_a : not (Feq Fa Fzero)}
+            {square_a : exists sqrt_a, Feq (Fmul sqrt_a sqrt_a) Fa}
+            {nonsquare_d : forall x, not (Feq (Fmul x x) Fd)}.
+    
+    Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
             {fieldK: @Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
-            {Kprm:@twisted_edwards_params K Keq Kzero Kone Kopp Kadd Ksub Kmul Ka Kd}
+            {char_gt_2_K : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)}
             {Keq_dec:DecidableRel Keq}.
     Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul
                                                    K Keq Kone Kadd Kmul phi}.
-    Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}.
+    Context {Ka} {Ha:Keq (phi Fa) Ka} {Kd} {Hd:Keq (phi Fd) Kd}.
     Local Notation Fpoint := (@E.point F Feq Fone Fadd Fmul Fa Fd).
     Local Notation Kpoint := (@E.point K Keq Kone Kadd Kmul Ka Kd).
+    Local Notation Fzero  := (E.zero(nonzero_a:=nonzero_a)(d:=Fd)).
+    Local Notation Fadd   := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
 
     Create HintDb field_homomorphism discriminated.
     Hint Rewrite <-
@@ -154,7 +153,8 @@ Module E.
             {point_phi_Proper:Proper (eq==>eq) point_phi}
             {point_phi_correct: forall (P:point), eq (point_phi P) (ref_phi P)}.
 
-    Lemma lift_homomorphism : @Monoid.is_homomorphism Fpoint eq add Kpoint eq add point_phi.
+    Lemma lift_homomorphism : @Monoid.is_homomorphism Fpoint eq add
+                                                      Kpoint eq add point_phi.
     Proof.
       repeat match goal with
              | |- _ => intro
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 770a2d02d..801b31ffc 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -9,40 +9,37 @@ Module E.
     * <https://eprint.iacr.org/2015/677.pdf>
     *)
 
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {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 (BinNat.N.succ_pos BinNat.N.one)}
+            {Feq_dec:Decidable.DecidableRel Feq}.
     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 "-" := Fsub. Local Infix "/" := Fdiv.
     Local Notation "x ^ 2" := (x*x) (at level 30).
-    Local Notation "n / d" := (fst (Fdiv n d, (_:(d <> 0)))). (* force nonzero d *)
-
-    Context {a d: F}.
-    Class twisted_edwards_params :=
-      {
-        char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one);
-        nonzero_a : a <> 0;
-        square_a : exists sqrt_a, sqrt_a^2 = a;
-        nonsquare_d : forall x, x^2 <> d
-      }.
-    Context `{twisted_edwards_params}. (* TODO: name me *)
-
-    Definition point := { P | let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2 }.
-    Definition coordinates (P:point) : (F*F) := proj1_sig P.
+
+    Context {a d: F}
+            {nonzero_a : a <> 0}
+            {square_a : exists sqrt_a, sqrt_a^2 = a}
+            {nonsquare_d : forall x, x^2 <> d}.
+
+    Definition point := { xy | let '(x, y) := xy in a*x^2 + y^2 = 1 + d*x^2*y^2 }.
+    Definition coordinates (P:point) : (F*F) := let (xy, xy_onCurve_proof) := P in xy.
     Definition eq (P Q:point) :=
-      fst (coordinates P) = fst (coordinates Q) /\
-      snd (coordinates P) = snd (coordinates Q).
+      match coordinates P, coordinates Q with
+        (x1,y1), (x2,y2) => x1 = x2 /\ y1 = y2
+      end.
 
     Program Definition zero : point := (0, 1).
-    Next Obligation. destruct H; eauto using Pre.onCurve_zero. Qed.
+    Next Obligation. eauto using Pre.onCurve_zero. Qed.
 
     Program Definition add (P1 P2:point) : point :=
-      let x1y1 := coordinates P1 in let x1 := fst x1y1 in let y1 := snd x1y1 in
-      let x2y2 := coordinates P2 in let x2 := fst x2y2 in let y2 := snd x2y2 in
-        (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
-    Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H. eauto using Pre.denominator_nonzero_x. Qed.
-    Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H; eauto using Pre.denominator_nonzero_y. Qed.
-    Next Obligation. destruct P1 as [[??]?], P2 as [[??]?], H; eauto using Pre.onCurve_add. Qed.
+      match coordinates P1, coordinates P2 return (F*F) with
+        (x1, y1), (x2, y2) =>
+        (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
+      end.
+    Next Obligation. destruct P1 as [[??]?], P2 as [[??]?]; eapply Pre.onCurve_add; eauto. Qed.
 
     Fixpoint mul (n:nat) (P : point) : point :=
       match n with
diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
index 5489a8ef0..bff8c2bc2 100644
--- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v
+++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
@@ -26,6 +26,13 @@ Module W.
     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}.
 
+    Program Definition inv (P:point) : point
+      := match W.coordinates P return F*F+_ with
+         | inl (x1, y1) => inl (x1, Fopp y1)
+         | _ => P
+         end.
+    Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed.
+
     Lemma same_x_same_y
           (xA yA : F)
           (A : yA ^ 2 = xA ^ 3 + a * xA + b)
@@ -36,16 +43,14 @@ Module W.
       : yB = yA.
     Proof. fsatz. Qed.
 
-    Definition is_redundant {T} (x:T) := x.
-    Global Arguments is_redundant : simpl never.
+    Let is_redundant {T} (x:T) := x.
     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 _
+      | _ => solve [ contradiction | trivial | exact _ ]
       | _ => intro
       | [ A : ?yA ^ 2 = ?xA ^ 3 + a * ?xA + b,
               B : ?yB ^ 2 = ?xB ^ 3 + a * ?xB + b,
@@ -65,119 +70,14 @@ Module W.
       | |- 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 *
-      | _ => progress simpl in *
+      | _ => progress cbv [inv W.eq W.zero W.add W.coordinates proj1_sig] in *
       | _ => progress break_match
       | |- _ /\ _ => split | |- _ <-> _ => split
-      | _ => abstract (trivial || contradiction || clear_marked_redundant; fsatz)
       end.
-    Ltac t := repeat t_step.
-
-    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.
+    Ltac t := repeat t_step; clear_marked_redundant.
 
     Global Instance commutative_group : abelian_group(eq:=W.eq)(op:=W.add)(id:=W.zero)(inv:=inv).
-    Proof. Time t. Time Qed.
+    Proof. t. all:try (abstract fsatz). 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