From bc2444209e6c38ba5465d4a05f771b4983b9a0b6 Mon Sep 17 00:00:00 2001
From: Greg Weng <snowmantw@gmail.com>
Date: Thu, 29 Jun 2023 23:51:19 +0900
Subject: [PATCH 1/6] 2023/6/29: WIP: monad_model.v:2031

shows the difficulties to have monads in one monad? Because of the universe inconsistency issue
---
 hierarchy.v   | 229 ++++++++++++++++++++++++++++++++++++++++++++++++++
 monad_model.v | 149 +++++++++++++++++++++++++++++++-
 2 files changed, 377 insertions(+), 1 deletion(-)

diff --git a/hierarchy.v b/hierarchy.v
index 0edb9016..0517def1 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -3,6 +3,7 @@
 Ltac typeof X := type of X.
 
 Require Import ssrmatching Reals.
+Require Import Floats ssreflect.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 From infotheo Require Import Reals_ext.
@@ -1217,3 +1218,231 @@ HB.mixin Record isMonadFailFresh (S : eqType) (M : UU0 -> UU0)
 HB.structure Definition MonadFailFresh (S : eqType) :=
   { M of isMonadFailFresh S M & isFunctor M & isMonad M & isMonadFresh S M &
          isMonadFail M }.
+
+
+(*
+
+For example, if we have a monadic SMC code:
+
+    compare x
+
+Then:
+
+1. `x` must exist at both locals
+    (like, index in array monad could be out of range -- but using default value instead).
+2. `x` must be SMC-type.
+3. Both locals must commit some state changes to execute the `compare` (a model thing?)
+
+What is a "local" and how to have it when defining the interface?
+Like in the isMonadArray interface: there is no "array" can be seen.
+
+  aget : I -> M S ;
+  aput : I -> S -> M unit ;
+
+(Where is the "array"? It becomes a model thing so hidden at the interface level)
+
+----
+
+About laws:
+
+Some interface methods are extended from basic operations.
+And they are laws. Like `aputput` is a law to require two put operations to store
+values at the same index, it equals to only storing the later one's result.
+
+(Ref: https://prg.is.titech.ac.jp/wp-content/uploads/2022/04/ppl2022_v2.pdf)
+
+This "law" of `aputput` is defined in `hierachy.v`:
+
+  aputput : forall i s s', aput i s >> aput i s' = aput i s' ;
+
+With a proof  in the `monad_model.v`:
+
+  Let aputput i s s' : aput i s >> aput i s' = aput i s'.
+  Proof.
+  rewrite state_bindE; apply boolp.funext => a/=.
+  by rewrite /aput insert_insert.
+  Qed.
+
+Therefore, if we define basic SMC operations at the interface,
+we can also define necessary laws the same interface,
+then prove them in the model file.
+
+And of course, these operations and laws,
+must represent SMC style on the SMC computation structure.
+
+So if SMC computation structure is about two locals,
+the laws must describe these two locals explicitly,
+and thus the two locals must be in type signatures of those interface methods.
+
+One critical thing is to keep the monad useful for the operations.
+Since now two locals are in the type signatures,
+if the operation itself can done the all things without what inside the monad,
+then having a monad becomes useless (although, at least, monad allows us to 
+have sequence of execution; but it is a pure monad, no SMC features inside.)
+
+** What is SMC feature for a monad **
+
+There could be some extra steps before or after the operation itself,
+and two locals may have or have no information exchange.
+
+*)
+
+Inductive smcty : Set :=
+(*  | Int    --cannot define Int because Uint63 defined a conflicting `_>>_`  notation *)
+  | Float
+  | Array of nat & smcty.
+
+(* cannot have pair because 
+Syntax error: [pattern level 200] expected after '(' (in [pattern]).
+  | Pair of smcty & smcty.
+*)
+
+Fixpoint smc2ty (ty : smcty) : Type :=
+  match ty with
+(*  | Int => int  *)
+  | Float => float
+  | Array n ty => n.-tuple (smc2ty ty)
+(*
+  | Pair ty1 ty2 => smc2ty ty1 * smc2ty ty2
+*)
+  end.
+Inductive loc : smcty -> smcty -> Type :=
+  | Here ty : loc ty ty
+(*
+  | Left ty1 ty2 : loc (Pair ty1 ty2) ty1
+  | Right ty1 ty2 : loc (Pair ty1 ty2) ty2
+*)
+  | Nth n ty (i : 'I_n) : loc (Array n ty) ty.
+
+Definition smcget (ty ty' : smcty) (l : loc ty ty') :=
+  match l in loc ty ty' return smc2ty ty -> smc2ty ty' with
+  | Here ty => fun v => v
+(* cannot have pair because 
+Syntax error: [pattern level 200] expected after '(' (in [pattern]).
+  | Left ty1 ty2 => fun '(v1, v2) => v1
+  | Right ty1 ty2 => fun '(v1, v2) => v2
+*)
+  | Nth n ty i => fun v => tnth v i
+  end.
+Check smcget.
+Definition SMC (shared : smcty) (res : Type) :=
+  smc2ty shared -> res * smc2ty shared.
+
+  (*
+Notation SMCLocal := [tuple smcty; smcty].
+
+Notation SMCStates := [tuple SMCLocal; SMCLocal].
+
+Check eqType.
+Locate eqType.
+*)
+
+(* the same issue as GADT: since `compare in Monad` needs a generic `a`, not restricted type *)
+(*
+Inductive smcstates : Set :=
+| States : [tuple SMCLocal; SMCLocal]. 
+
+
+
+Notation "'SMCState'" := ((S * S * S * S) % type) (at level 99).
+Notation "'SMCExpr'" := (S -> (S * S * S * S) % type) (at level 99).
+
+Notation  (*Memo: an "abbreviation"; doesn't need `level`*)
+*)
+
+Section smc_monad_local.
+
+Variables F P : UU0.
+Variable VarName : eqType.
+
+Definition SMCLocal : UU0 := F * P.
+Definition SMCStates : UU0 := SMCLocal * SMCLocal.
+
+
+End smc_monad_local.
+(* Note: do mixin outside a section*)
+(* When shortening def by Definition, providing arguments like `SMCStates F P`, not just `SMCStates`*)
+
+(* Each local: doing local computation faithfully; no swap or other global ops*)
+HB.mixin Record isMonadSMCLocal (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
+
+  (* The "internal" interface for the Global to call, so the Global can get the local values
+     when it needs to do magic SMC things for locals. Locals don't need to know how to make
+     such protocol operations happen.
+  *)
+  get : VarName -> M (SMCLocal F P);
+
+  (* You give me a VarName I give you a value (assume only valid VarName will be passed),
+     Then you need to judge how to execute the op to complete the computation,
+     And how to return a new temporary (not committed yet; new results only) SMCLocals.
+
+        equal to: `expr var`
+
+     This `expr` can only handles the pure local expression.
+     Because there is no global monad passed here.
+     The direction is unidirectional `Global -> Local`, not bidirectional `Global <-> Local`
+  *)
+  expr : (SMCLocal F P -> SMCLocal F P) -> VarName -> M (SMCLocal F P);
+
+  (* assign the expression result to var *)
+  assign : VarName -> SMCLocal F P -> M unit;
+}.
+
+#[short(type=smcLocalMonad)]
+HB.structure Definition MonadSMCLocal (F P : UU0) (VarName : eqType) :=
+  {M of isMonadSMCLocal F P VarName M & isMonad M & isFunctor M }.
+  
+Section smc_monad.
+
+Variables F P : UU0.
+Variable VarName : eqType.
+Definition MonadSMCLocals : UU0 := (smcLocalMonad F P VarName * smcLocalMonad F P VarName).
+
+End smc_monad.
+
+HB.mixin Record isMonadSMCGlobal (MonadSMCLocals : UU0 -> UU0 -> eqType -> UU0) (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
+
+  (* For monadic program after the compilation.
+     One `get` in global means two local `get` steps on local machines.
+  *)
+  get : VarName -> M (MonadSMCLocals F P VarName)
+
+  (* expr related to Global = SMC protocols
+    
+    Whenever there is an computation over a Partial value bound to one VarName,
+     the expression needs to call the built-in SMC protocol functions to complete the computation,
+     and what those protocol functions do are simplified here as:
+
+     1. Get both locals' target Partial values by local `get`.
+     2. Generate new partial values from those partial values.
+     3. Put the generated SMC values back to locals by local `assign`.
+  *)
+  expr : (MonadSMCLocals F P VarName -> MonadSMCLocals F P VarName) -> VarName -> M (MonadSMCLocals F P VarName);
+
+  (* A simplified "SMC protocol" for two-party communications.
+
+     It exchange the "partial" var in two locals with the same VarName.
+     So the two parties must prepare the exchanging target first,
+     and then this method call will do the "communication".
+  *)
+  exchange : MonadSMCLocals F P VarName -> VarName -> M unit;
+
+  (*TODO: getResult? From this global SMC *)
+  (*TODO: Partial and Full data flow view: all Fulls eventually become Partials;
+    and "Global" is actually a Partial data handler *)
+}.
+
+#[short(type=smcMonadGlobal)]
+HB.structure Definition MonadSMCGlobal (MonadSMCLocals : UU0 -> UU0 -> eqType -> UU0) (F P : UU0) (V : eqType) :=
+  {M of isMonadSMCGlobal MonadSMCLocals F P V M & isMonad M & isFunctor M }.
+
+(* Use smcMonad and smcMonadLocal, to represent the language smcSL*)
+HB.mixin Record isMonadSMCLang (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
+
+    (* The `compare` built-in function at the language lavel*)
+    compare : VarName -> M (bool * smcty) %type;
+}.
+
+#[short(type=smcMonadLang)]
+HB.structure Definition MonadSMCLang (F P : UU0) (V : eqType) :=
+  {M of isMonadSMCLang F P V M & isMonad M & isFunctor M }.
\ No newline at end of file
diff --git a/monad_model.v b/monad_model.v
index fc73811c..66ea347c 100644
--- a/monad_model.v
+++ b/monad_model.v
@@ -150,9 +150,29 @@ Proof. by []. Qed.
 Let right_neutral : BindLaws.right_neutral bind (NId FId).
 Proof. by []. Qed.
 Let associative : BindLaws.associative bind. Proof. by []. Qed.
-Let acto := (@idfun UU0).
+
+(** SMC notes **)
+(* When expressing like this, it generates a specialized version of @idfun*)
+(* The original signature of @idfun is:
+
+    forall T : UU0, T -> T
+  
+  But (@idfun UU0), namely `acto`, becomes:
+
+    UU0 -> UU0
+
+  So (@idfun UU0) is a specialized version.
+  And then we can use it with any UU0 input.
+
+*)
+Let acto := (@idfun UU0).  
+Check left_neutral.
+
+(* `isMonad_ret_bind.Build` receives `acto` and other functions, then instance the monad *)
+
 HB.instance Definition _ := isMonad_ret_bind.Build
   acto left_neutral right_neutral associative.
+
 End identitymonad.
 End IdentityMonad.
 HB.export IdentityMonad.
@@ -160,6 +180,9 @@ HB.export IdentityMonad.
 Module ListMonad.
 Section listmonad.
 Definition acto := fun A : UU0 => seq A.
+
+Check acto.
+
 Local Notation M := acto.
 Let ret : FId ~~> M := fun (A : UU0) x => (@cons A) x [::].
 Let bind := fun A B (m : M A) (f : A -> M B) => flatten (map f m).
@@ -186,6 +209,9 @@ Module SetMonad.
 Section setmonad.
 Local Open Scope classical_set_scope.
 Definition acto := set.
+
+Check set.
+Check @bigcup.
 Local Notation M := acto.
 Let ret : idfun ~~> M := @set1.
 Let bind := fun A B => @bigcup B A.
@@ -211,10 +237,24 @@ Module ExceptMonad.
 Section exceptmonad.
 Variable E : UU0.
 Definition acto := fun A : UU0 => (E + A)%type.
+Check fun A : UU0 => (E + A)%type.
+
+(** SMC note
+
+Different `acto` has the same type signature,
+but their implementation receives different types in different monads.
+
+**)
+
 Local Notation M := acto.
 Let ret : FId ~~> M := @inr E.
+
+Check @inr.
+
 Let bind := fun A B (m : M A) (f : A -> M B) =>
   match m with inl z => inl z | inr b => f b end.
+
+Check inl.
 Let left_neutral : BindLaws.left_neutral bind ret.
 Proof. by []. Qed.
 Let right_neutral : BindLaws.right_neutral bind ret.
@@ -1939,3 +1979,110 @@ HB.instance Definition _ := @isMonadExceptStateRun.Build S N (MS S N)
 
 End modelmonadexceptstaterun.
 End ModelMonadExceptStateRun.
+
+(* Models of SMC monads *)
+
+(* SMC Local Monad: 
+   Basically a MonadArray but every element is a `(F * P)` instead of a single `S`. *)
+
+Module ModelSMCLocal.
+Section modelsmc_local.
+
+Variables (F P : UU0) (VarName : eqType).
+Local Notation SMCLocalVars := (VarName -> SMCLocal F P).
+Implicit Types (v : VarName) (l : SMCLocal F P) (e : SMCLocal F P -> SMCLocal F P) (A : UU0).
+
+Definition acto := StateMonad.acto SMCLocalVars.
+Local Notation M := acto.
+
+(* From the registry of all variables on one local machine, `get` and lift one var to the local monad. *)
+Definition get v : M (SMCLocal F P) := fun vars => (vars v, vars).
+
+(* NOTE: how `vars v` indexes the values is unknown here, but this still can be defined. *)
+(* Because it will be defined when init the "state" monad with an init state, which must provide
+   how to get the var from `vars v`. *)
+Definition expr e v : M (SMCLocal F P) := fun vars => (e (vars v), vars).
+
+(* Update the content registered to the var name: `var = (full, pair)` *)
+Definition assign v l : M unit := fun vars => (tt, insert v l vars).
+
+HB.about isMonadSMCLocal.
+
+(* Memo: this line must be in order *)
+HB.instance Definition _ := isMonadSMCLocal.Build
+  F P VarName acto get expr assign.
+
+End modelsmc_local.
+End ModelSMCLocal.
+
+(* ---- ---- *)
+
+(* SMC Global: a monad composes of two local monads *)
+
+Module ModelSMCGlobal.
+Section modelsmc_global.
+
+Variables (F P : UU0) (VarName : eqType).
+Local Notation SMCGlobalVars :=  (VarName -> MonadSMCLocals F P VarName).
+Implicit Types (v : VarName) (g : MonadSMCLocals F P VarName) (e : MonadSMCLocals F P VarName -> MonadSMCLocals F P VarName) (A : UU0).
+
+Check SMCGlobalVars.
+Check MonadSMCLocals F P VarName.
+Check StateMonad.acto (VarName -> MonadSMCLocals F P VarName).
+
+
+(*
+Memo: acto application must be UU0 -> UU0.
+
+StateMonad.acto
+	 : UU0 -> UU0 -> UU0
+StateMonad.acto (VarName -> SMCLocal F P)
+	 : UU0 -> UU0
+
+
+In array monad:
+
+  Variables (S : UU0) (I : eqType).
+  Implicit Types (i j : I) (A : UU0).
+  Definition acto := StateMonad.acto (I -> S).
+*)
+
+Definition acto := StateMonad.acto SMCGlobalVars.
+Local Notation M := acto.
+
+Definition get 
+
+End modelsmc_global.
+End ModelSMCGlobal.
+
+
+(* Memo:
+
+What does "universe inconsistency" means:
+
+https://stackoverflow.com/questions/32153710/what-does-error-universe-inconsistency-mean-in-coq
+
+(constrains like: Type_i, Type_j, and i < j -- cannot be solved internally in Coq.)
+
+*)
+
+(* Memo:
+
+1. `Int` means an interface for `()` (???), so that the caller can use Int's operations over `()`.
+2. `Array Int` means an interface for Int, so that the caller can use Array's operations over Int.
+3. `M (Array Int)` means an interface for Array Int, so that the caller can use M's operations over `Array Int`
+    --> And how to define all operations of `M` by the underlying `Array` operations is what monad transformer does.
+
+*)
+
+(*
+Require Import PrimInt63.
+Require Sint63.
+Section Int63.
+
+Inductive smcty : Set :=
+  | Int
+  | Float
+  | Array of nat & smcty.
+
+*)
\ No newline at end of file

From 8d61782347d880ba17cafcbea3ffde1b501792a0 Mon Sep 17 00:00:00 2001
From: Greg Weng <snowmantw@gmail.com>
Date: Fri, 30 Jun 2023 07:30:55 +0900
Subject: [PATCH 2/6] 2023/6/29: WIP: change Global from monad of monads to
 monad of data instances

But how to define the `extract` method for the local monad becomes a modeling problem.
See monad_model.v:2009.
---
 hierarchy.v   | 62 ++++++++++++++++++++++++++++++++++++++++++---------
 monad_model.v | 17 ++++++++++----
 2 files changed, 64 insertions(+), 15 deletions(-)

diff --git a/hierarchy.v b/hierarchy.v
index 0517def1..816c6578 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -1366,10 +1366,7 @@ End smc_monad_local.
 (* Each local: doing local computation faithfully; no swap or other global ops*)
 HB.mixin Record isMonadSMCLocal (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
 
-  (* The "internal" interface for the Global to call, so the Global can get the local values
-     when it needs to do magic SMC things for locals. Locals don't need to know how to make
-     such protocol operations happen.
-  *)
+  (* To start a local monad computation chain. *)
   get : VarName -> M (SMCLocal F P);
 
   (* You give me a VarName I give you a value (assume only valid VarName will be passed),
@@ -1384,8 +1381,35 @@ HB.mixin Record isMonadSMCLocal (F P : UU0) (VarName : eqType) (M : UU0 -> UU0)
   *)
   expr : (SMCLocal F P -> SMCLocal F P) -> VarName -> M (SMCLocal F P);
 
-  (* assign the expression result to var *)
+  (* Assign the expression result to var *)
   assign : VarName -> SMCLocal F P -> M unit;
+
+  (* Actually a comonad method: this is necessary when the global holds two instances of actual local data,
+     not two monads:
+
+         SMCLocal : (F * P)
+         SMCGlobal : (F * P * F * P)
+
+         smcGlobalMonad : Monad (F P VarName)
+
+     So if the global monad needs to change its pair of SMCLocal data,
+     it "install" the monad interface to the SMCLocal data it owns:
+
+         (smcLocalMonad F P VarName * smcLocalMonad F P VarName)
+
+     And delegate operations to the locals like:
+
+     Then delegate the operations to each local by a global monad method `local`:
+
+         local >>=
+            fun (ma, mb) => (ma >>= fun a => a + 1 >>= extract, mb >>= fun b => b - 1 >>= extract)
+     
+     Without this `extract` method, the value cannot go back
+     to the SMCGlobal: (F * P * F * P) but monadic values `(smcLocalMonad F P VarName * smcLocalMonad F P VarName)`,
+     which doesn't match the expected data type owned by the `smcGlobalMonad`.
+  *)
+  extract : M (SMCLocal F P) -> SMCLocal F P;
+
 }.
 
 #[short(type=smcLocalMonad)]
@@ -1396,16 +1420,32 @@ Section smc_monad.
 
 Variables F P : UU0.
 Variable VarName : eqType.
+Definition SMCGlobal : UU0 := SMCLocal F P * SMCLocal F P.
 Definition MonadSMCLocals : UU0 := (smcLocalMonad F P VarName * smcLocalMonad F P VarName).
 
 End smc_monad.
 
-HB.mixin Record isMonadSMCGlobal (MonadSMCLocals : UU0 -> UU0 -> eqType -> UU0) (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
+HB.mixin Record isMonadSMCGlobal (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
+
+  (* From one pair of both locals' variables,
+     install two local monad interfaces to them,
+     and thus allow the following operations be expressed in local monad operations.
+
+     After the moadic program at the local leve, this method calls local monad's `extract` method,
+     to put their computation results back to the global.
+
+     For example:
+
+     local >>=
+         fun (a , b ) => (ma >>= fun a => a + 1, mb >>= fun b => b - 1) >>=
+         fun (a', b') => globalFunc a' b'
+  *)
+  local : (SMCGlobal F P -> (MonadSMCLocals F P VarName)) -> M (SMCGlobal F P);
 
   (* For monadic program after the compilation.
      One `get` in global means two local `get` steps on local machines.
   *)
-  get : VarName -> M (MonadSMCLocals F P VarName)
+  get : VarName -> M (SMCGlobal F P);
 
   (* expr related to Global = SMC protocols
     
@@ -1417,7 +1457,7 @@ HB.mixin Record isMonadSMCGlobal (MonadSMCLocals : UU0 -> UU0 -> eqType -> UU0)
      2. Generate new partial values from those partial values.
      3. Put the generated SMC values back to locals by local `assign`.
   *)
-  expr : (MonadSMCLocals F P VarName -> MonadSMCLocals F P VarName) -> VarName -> M (MonadSMCLocals F P VarName);
+  expr : (SMCGlobal F P -> SMCGlobal F P) -> VarName -> M (SMCGlobal F P);
 
   (* A simplified "SMC protocol" for two-party communications.
 
@@ -1425,7 +1465,7 @@ HB.mixin Record isMonadSMCGlobal (MonadSMCLocals : UU0 -> UU0 -> eqType -> UU0)
      So the two parties must prepare the exchanging target first,
      and then this method call will do the "communication".
   *)
-  exchange : MonadSMCLocals F P VarName -> VarName -> M unit;
+  exchange : SMCGlobal F P -> VarName -> M unit;
 
   (*TODO: getResult? From this global SMC *)
   (*TODO: Partial and Full data flow view: all Fulls eventually become Partials;
@@ -1433,8 +1473,8 @@ HB.mixin Record isMonadSMCGlobal (MonadSMCLocals : UU0 -> UU0 -> eqType -> UU0)
 }.
 
 #[short(type=smcMonadGlobal)]
-HB.structure Definition MonadSMCGlobal (MonadSMCLocals : UU0 -> UU0 -> eqType -> UU0) (F P : UU0) (V : eqType) :=
-  {M of isMonadSMCGlobal MonadSMCLocals F P V M & isMonad M & isFunctor M }.
+HB.structure Definition MonadSMCGlobal (F P : UU0) (V : eqType) :=
+  {M of isMonadSMCGlobal F P V M & isMonad M & isFunctor M }.
 
 (* Use smcMonad and smcMonadLocal, to represent the language smcSL*)
 HB.mixin Record isMonadSMCLang (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
diff --git a/monad_model.v b/monad_model.v
index 66ea347c..fba94243 100644
--- a/monad_model.v
+++ b/monad_model.v
@@ -2006,30 +2006,35 @@ Definition expr e v : M (SMCLocal F P) := fun vars => (e (vars v), vars).
 (* Update the content registered to the var name: `var = (full, pair)` *)
 Definition assign v l : M unit := fun vars => (tt, insert v l vars).
 
-HB.about isMonadSMCLocal.
+Definition extract mvars : SMCLocal F P := fun vars => 
 
 (* Memo: this line must be in order *)
 HB.instance Definition _ := isMonadSMCLocal.Build
-  F P VarName acto get expr assign.
+  F P VarName acto get expr assign extract.
 
 End modelsmc_local.
 End ModelSMCLocal.
 
 (* ---- ---- *)
 
-(* SMC Global: a monad composes of two local monads *)
+(* SMC Global: a monad composes of two instances of local data,
+   and use the local monad inteface to manipuate them
+*)
+
 
+(*
 Module ModelSMCGlobal.
 Section modelsmc_global.
 
 Variables (F P : UU0) (VarName : eqType).
-Local Notation SMCGlobalVars :=  (VarName -> MonadSMCLocals F P VarName).
+Local Notation SMCGlobalVars :=  (VarName -> SMCGlobal F P).
 Implicit Types (v : VarName) (g : MonadSMCLocals F P VarName) (e : MonadSMCLocals F P VarName -> MonadSMCLocals F P VarName) (A : UU0).
 
 Check SMCGlobalVars.
 Check MonadSMCLocals F P VarName.
 Check StateMonad.acto (VarName -> MonadSMCLocals F P VarName).
 
+*)
 
 (*
 Memo: acto application must be UU0 -> UU0.
@@ -2047,6 +2052,8 @@ In array monad:
   Definition acto := StateMonad.acto (I -> S).
 *)
 
+
+(*
 Definition acto := StateMonad.acto SMCGlobalVars.
 Local Notation M := acto.
 
@@ -2055,6 +2062,8 @@ Definition get
 End modelsmc_global.
 End ModelSMCGlobal.
 
+*)
+
 
 (* Memo:
 

From 81dc8ba7e3696b42959dabcdb04d1174d8055913 Mon Sep 17 00:00:00 2001
From: Greg Weng <snowmantw@gmail.com>
Date: Fri, 7 Jul 2023 10:01:11 +0900
Subject: [PATCH 3/6] WIP: smcLocalMonad debugging

---
 hierarchy.v   | 302 +++++++++++++++++---------------------------------
 monad_model.v | 190 ++++++++++++++++++++++++++-----
 2 files changed, 263 insertions(+), 229 deletions(-)

diff --git a/hierarchy.v b/hierarchy.v
index 816c6578..266a0a5c 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -1219,6 +1219,106 @@ HB.structure Definition MonadFailFresh (S : eqType) :=
   { M of isMonadFailFresh S M & isFunctor M & isMonad M & isMonadFresh S M &
          isMonadFail M }.
 
+(* ---- SMC Monads ---- *)
+(* These interfaces represent the single-assignment form computations
+   over Full or Partial values on local machines.
+
+   For Full values, they belong to and exist only on one party.
+   Computations over Full values means private computations that the countpart neither knows nor involves.
+   These computation results will be assigned back to local environment.
+
+   For Partial values, they are split and shared among parties.
+   Computations over Partial values means parties execute SMC protocols collaborately to get a Partial result,
+   and this result will be split and shared among parties as a result variable.
+*)
+(*
+   About variable types:
+
+   We start with a "dynamic typing" approach at the beginning.
+   Variables in each monadic operation's type signature are with their
+   names only. The actual dispatching and checking will be proceeded
+   in the monad_model.v.
+
+   If in the future we decide to extend this interface file with exposing
+   more details here, we may then have static types at interface level.
+*)
+
+Section smc_monad_local.
+Variable VarName : eqType.
+
+End smc_monad_local.
+(* Note: do mixin outside a section*)
+
+(* SMC local monad: computes over Full variables only. *)
+HB.mixin Record isMonadSMCLocal (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
+  
+  (* Pure local addition for two Full variables. *)
+  add : VarName -> VarName -> VarName -> M unit;
+}.
+
+#[short(type=smcLocalMonad)]
+HB.structure Definition MonadSMCLocal (VarName : eqType) :=
+  {M of isMonadSMCLocal VarName M & isMonad M & isFunctor M }.
+  
+Section smc_monad.
+
+Variable VarName : eqType.
+
+End smc_monad.
+
+
+
+(* SMC global monad: computes over Partial values only. *)
+HB.mixin Record isMonadSMCGlobal (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
+
+  (* SMC global represent the whole SMC program,
+     so there are some local-only computations for Full variables.
+     
+     These local-only computations happen in the local monad.
+     And it will directly assign related variables to the local env.
+  *)
+  
+  (* At interface level define a type in a record. *)
+  (* Got all deps in a record. *)
+  localM : smcLocalMonad VarName;
+  local : localM unit -> M unit;
+
+  (* Note: smcLocalMonad is a record -- the type of computation in the monad *)
+  (*local :  smcLocalMonad VarName -> M unit;*)
+
+  (* Exchange two partial variables with the same name at the both locals. *)
+  exchange : VarName -> M unit;
+
+  (* Split a Full variable to Partial SMC variable by SMC protocols. *)
+  (* Example: at Alice side, `split wealth result` equal to:
+
+       tmp = smc_zntoz2 wealth_alice
+       result_alice = smc_zntoz2
+  *)
+  split : VarName -> VarName -> M unit;
+
+  (* Execute SMC compare both local's one Partial variable, then store the result as a new Partial. *)
+  (* Example: at Alice side, `compare wealth result` equal to:
+  
+      tmp = smc_compare wealth_alice  // wealth_alice: converted from Full to Partial already.
+      bar_alice = tmp
+  
+  *)
+  compare : VarName -> VarName -> M unit;
+
+  (* Execute SMC add on two Partial variables, then store the result as a new Partial. *)
+  (* Example: at Alice side, `add foo bar result`  equal to:
+  
+      tmp = smc_add foo_alice bar_alice
+      result_alice = tmp
+  
+  *)
+  add : VarName -> VarName -> VarName -> M unit;
+}.
+
+#[short(type=smcMonadGlobal)]
+HB.structure Definition MonadSMCGlobal (V : eqType) :=
+  {M of isMonadSMCGlobal V M & isMonad M & isFunctor M }.
 
 (*
 
@@ -1285,204 +1385,4 @@ have sequence of execution; but it is a pure monad, no SMC features inside.)
 There could be some extra steps before or after the operation itself,
 and two locals may have or have no information exchange.
 
-*)
-
-Inductive smcty : Set :=
-(*  | Int    --cannot define Int because Uint63 defined a conflicting `_>>_`  notation *)
-  | Float
-  | Array of nat & smcty.
-
-(* cannot have pair because 
-Syntax error: [pattern level 200] expected after '(' (in [pattern]).
-  | Pair of smcty & smcty.
-*)
-
-Fixpoint smc2ty (ty : smcty) : Type :=
-  match ty with
-(*  | Int => int  *)
-  | Float => float
-  | Array n ty => n.-tuple (smc2ty ty)
-(*
-  | Pair ty1 ty2 => smc2ty ty1 * smc2ty ty2
-*)
-  end.
-Inductive loc : smcty -> smcty -> Type :=
-  | Here ty : loc ty ty
-(*
-  | Left ty1 ty2 : loc (Pair ty1 ty2) ty1
-  | Right ty1 ty2 : loc (Pair ty1 ty2) ty2
-*)
-  | Nth n ty (i : 'I_n) : loc (Array n ty) ty.
-
-Definition smcget (ty ty' : smcty) (l : loc ty ty') :=
-  match l in loc ty ty' return smc2ty ty -> smc2ty ty' with
-  | Here ty => fun v => v
-(* cannot have pair because 
-Syntax error: [pattern level 200] expected after '(' (in [pattern]).
-  | Left ty1 ty2 => fun '(v1, v2) => v1
-  | Right ty1 ty2 => fun '(v1, v2) => v2
-*)
-  | Nth n ty i => fun v => tnth v i
-  end.
-Check smcget.
-Definition SMC (shared : smcty) (res : Type) :=
-  smc2ty shared -> res * smc2ty shared.
-
-  (*
-Notation SMCLocal := [tuple smcty; smcty].
-
-Notation SMCStates := [tuple SMCLocal; SMCLocal].
-
-Check eqType.
-Locate eqType.
-*)
-
-(* the same issue as GADT: since `compare in Monad` needs a generic `a`, not restricted type *)
-(*
-Inductive smcstates : Set :=
-| States : [tuple SMCLocal; SMCLocal]. 
-
-
-
-Notation "'SMCState'" := ((S * S * S * S) % type) (at level 99).
-Notation "'SMCExpr'" := (S -> (S * S * S * S) % type) (at level 99).
-
-Notation  (*Memo: an "abbreviation"; doesn't need `level`*)
-*)
-
-Section smc_monad_local.
-
-Variables F P : UU0.
-Variable VarName : eqType.
-
-Definition SMCLocal : UU0 := F * P.
-Definition SMCStates : UU0 := SMCLocal * SMCLocal.
-
-
-End smc_monad_local.
-(* Note: do mixin outside a section*)
-(* When shortening def by Definition, providing arguments like `SMCStates F P`, not just `SMCStates`*)
-
-(* Each local: doing local computation faithfully; no swap or other global ops*)
-HB.mixin Record isMonadSMCLocal (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
-
-  (* To start a local monad computation chain. *)
-  get : VarName -> M (SMCLocal F P);
-
-  (* You give me a VarName I give you a value (assume only valid VarName will be passed),
-     Then you need to judge how to execute the op to complete the computation,
-     And how to return a new temporary (not committed yet; new results only) SMCLocals.
-
-        equal to: `expr var`
-
-     This `expr` can only handles the pure local expression.
-     Because there is no global monad passed here.
-     The direction is unidirectional `Global -> Local`, not bidirectional `Global <-> Local`
-  *)
-  expr : (SMCLocal F P -> SMCLocal F P) -> VarName -> M (SMCLocal F P);
-
-  (* Assign the expression result to var *)
-  assign : VarName -> SMCLocal F P -> M unit;
-
-  (* Actually a comonad method: this is necessary when the global holds two instances of actual local data,
-     not two monads:
-
-         SMCLocal : (F * P)
-         SMCGlobal : (F * P * F * P)
-
-         smcGlobalMonad : Monad (F P VarName)
-
-     So if the global monad needs to change its pair of SMCLocal data,
-     it "install" the monad interface to the SMCLocal data it owns:
-
-         (smcLocalMonad F P VarName * smcLocalMonad F P VarName)
-
-     And delegate operations to the locals like:
-
-     Then delegate the operations to each local by a global monad method `local`:
-
-         local >>=
-            fun (ma, mb) => (ma >>= fun a => a + 1 >>= extract, mb >>= fun b => b - 1 >>= extract)
-     
-     Without this `extract` method, the value cannot go back
-     to the SMCGlobal: (F * P * F * P) but monadic values `(smcLocalMonad F P VarName * smcLocalMonad F P VarName)`,
-     which doesn't match the expected data type owned by the `smcGlobalMonad`.
-  *)
-  extract : M (SMCLocal F P) -> SMCLocal F P;
-
-}.
-
-#[short(type=smcLocalMonad)]
-HB.structure Definition MonadSMCLocal (F P : UU0) (VarName : eqType) :=
-  {M of isMonadSMCLocal F P VarName M & isMonad M & isFunctor M }.
-  
-Section smc_monad.
-
-Variables F P : UU0.
-Variable VarName : eqType.
-Definition SMCGlobal : UU0 := SMCLocal F P * SMCLocal F P.
-Definition MonadSMCLocals : UU0 := (smcLocalMonad F P VarName * smcLocalMonad F P VarName).
-
-End smc_monad.
-
-HB.mixin Record isMonadSMCGlobal (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
-
-  (* From one pair of both locals' variables,
-     install two local monad interfaces to them,
-     and thus allow the following operations be expressed in local monad operations.
-
-     After the moadic program at the local leve, this method calls local monad's `extract` method,
-     to put their computation results back to the global.
-
-     For example:
-
-     local >>=
-         fun (a , b ) => (ma >>= fun a => a + 1, mb >>= fun b => b - 1) >>=
-         fun (a', b') => globalFunc a' b'
-  *)
-  local : (SMCGlobal F P -> (MonadSMCLocals F P VarName)) -> M (SMCGlobal F P);
-
-  (* For monadic program after the compilation.
-     One `get` in global means two local `get` steps on local machines.
-  *)
-  get : VarName -> M (SMCGlobal F P);
-
-  (* expr related to Global = SMC protocols
-    
-    Whenever there is an computation over a Partial value bound to one VarName,
-     the expression needs to call the built-in SMC protocol functions to complete the computation,
-     and what those protocol functions do are simplified here as:
-
-     1. Get both locals' target Partial values by local `get`.
-     2. Generate new partial values from those partial values.
-     3. Put the generated SMC values back to locals by local `assign`.
-  *)
-  expr : (SMCGlobal F P -> SMCGlobal F P) -> VarName -> M (SMCGlobal F P);
-
-  (* A simplified "SMC protocol" for two-party communications.
-
-     It exchange the "partial" var in two locals with the same VarName.
-     So the two parties must prepare the exchanging target first,
-     and then this method call will do the "communication".
-  *)
-  exchange : SMCGlobal F P -> VarName -> M unit;
-
-  (*TODO: getResult? From this global SMC *)
-  (*TODO: Partial and Full data flow view: all Fulls eventually become Partials;
-    and "Global" is actually a Partial data handler *)
-}.
-
-#[short(type=smcMonadGlobal)]
-HB.structure Definition MonadSMCGlobal (F P : UU0) (V : eqType) :=
-  {M of isMonadSMCGlobal F P V M & isMonad M & isFunctor M }.
-
-(* Use smcMonad and smcMonadLocal, to represent the language smcSL*)
-HB.mixin Record isMonadSMCLang (F P : UU0) (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
-
-    (* The `compare` built-in function at the language lavel*)
-    compare : VarName -> M (bool * smcty) %type;
-}.
-
-#[short(type=smcMonadLang)]
-HB.structure Definition MonadSMCLang (F P : UU0) (V : eqType) :=
-  {M of isMonadSMCLang F P V M & isMonad M & isFunctor M }.
\ No newline at end of file
+*)
\ No newline at end of file
diff --git a/monad_model.v b/monad_model.v
index fba94243..74fca9d5 100644
--- a/monad_model.v
+++ b/monad_model.v
@@ -1980,49 +1980,161 @@ HB.instance Definition _ := @isMonadExceptStateRun.Build S N (MS S N)
 End modelmonadexceptstaterun.
 End ModelMonadExceptStateRun.
 
-(* Models of SMC monads *)
 
-(* SMC Local Monad: 
-   Basically a MonadArray but every element is a `(F * P)` instead of a single `S`. *)
+
+
+(* ---- SMC type wrapper ---- *)
+(* ---- SMC data wrapper for dynamic typing ---- *)
+
+Require Import Floats PrimInt63.
+Require Import Bvector.
+Require Sint63.
+Section Int63.
+
+(* Memo: using `of` so it can be matched and extracted the wrapped inside *)
+Inductive smcvalue : Set :=
+| Int of int
+| Float of float
+| Bool of bool.
+
+(*Definition bvectorCapacity := 4611686018427387904*)
+Definition bvectorCapacity := 100.
+Definition smcglobal : UU0 := (smcvalue * Bvector bvectorCapacity * smcvalue * Bvector bvectorCapacity).
+
+End Int63.
+
+(* ---- Models of SMC monads ---- *)
+
+(* SMC Local Monad: a array monad with the element type is `smcvalue`. *)
 
 Module ModelSMCLocal.
 Section modelsmc_local.
 
-Variables (F P : UU0) (VarName : eqType).
-Local Notation SMCLocalVars := (VarName -> SMCLocal F P).
-Implicit Types (v : VarName) (l : SMCLocal F P) (e : SMCLocal F P -> SMCLocal F P) (A : UU0).
+Variables (VarName : eqType).
 
-Definition acto := StateMonad.acto SMCLocalVars.
-Local Notation M := acto.
+Implicit Types (v va vb assignee : VarName).
 
-(* From the registry of all variables on one local machine, `get` and lift one var to the local monad. *)
-Definition get v : M (SMCLocal F P) := fun vars => (vars v, vars).
+Definition acto := ModelArray.acto smcvalue VarName.
+(* Memo: by this we define a type-specified monad (?) *)
 
-(* NOTE: how `vars v` indexes the values is unknown here, but this still can be defined. *)
-(* Because it will be defined when init the "state" monad with an init state, which must provide
-   how to get the var from `vars v`. *)
-Definition expr e v : M (SMCLocal F P) := fun vars => (e (vars v), vars).
+(* Automatically got run already? *)
 
-(* Update the content registered to the var name: `var = (full, pair)` *)
-Definition assign v l : M unit := fun vars => (tt, insert v l vars).
+Local Notation M := acto.
+Definition aget := ModelArray.aget.
+Definition aput := ModelArray.aput.
 
-Definition extract mvars : SMCLocal F P := fun vars => 
+(* Otherwise they become monad PlusArray's aget and aput. *)
+
+Definition add va vb assignee : M unit :=
+  aget va >>= (fun a => aget vb >>= (fun b =>
+    match a, b with
+      | Int ia, Int ib => aput assignee (Int (add ia ib))
+      (* TODO: float + int by coercion, etc. *)
+      | _, _ => skip
+    end)).
 
 (* Memo: this line must be in order *)
 HB.instance Definition _ := isMonadSMCLocal.Build
-  F P VarName acto get expr assign extract.
+  VarName acto add.
 
 End modelsmc_local.
 End ModelSMCLocal.
 
-(* ---- ---- *)
+HB.export ModelSMCLocal.
+
+(* SMC Global: a array monad with (smcvalue * bitvector * smcvalue * bitvector) as its elements. *)
+
+Module ModelSMCGlobal.
+Section modelsmc_global.
+
+Variables (VarName : eqType).
 
-(* SMC Global: a monad composes of two instances of local data,
-   and use the local monad inteface to manipuate them
+Print MonadSMCLocal.
+HB.about MonadSMCLocal.
+
+Definition localM := [the smcLocalMonad VarName of ModelSMCLocal.acto VarName].
+
+
+Implicit Types (v va vb assignee : VarName) (MLocal : localM).
+
+Definition acto := ModelArray.acto smcglobal VarName.
+(* Memo: by this we define a type-specified monad (?)
+   It seems that except those methods required by the monad and functor definition,
+   other methods can be type-specific, if the return value is still a monadic value,
+   like `M unit` for array monad or `M (r, s)` for state monad.
+*)
+
+Local Notation M := acto.
+Definition aget := ModelArray.aget.
+Definition aput := ModelArray.aput.
+(* Otherwise they become monad PlusArray's aget and aput. *)
+
+Check ModelArray.aget.
+
+(* the parameter is just a local cannot be ran;
+   local program -- work on some monads.
+
+   already exists in the global, cannot be any local monad.
 *)
 
+Definition local MLocal : M unit :=
+  localM >> skip.
 
 (*
+
+Ask questions:
+
+1. `local`
+
+In environment
+VarName : eqType
+localM : smcLocalMonad VarName
+The term "localM" has type "MonadSMCLocal.type VarName"
+while it is expected to have type "Monad.sort ?s ?A".
+
+
+2. Confirm that we cannot make a dispatch function in Coq, and ask why
+
+----
+
+Extend the array monad.
+
+To add the stateRun monad.
+
+Cannot use Comonad : extract cannot rely on the outside input.
+
+
+----
+
+
+Global and Local. At the interface level.
+
+Two models must be related.
+
+Local monad is a param to the gloal monad.
+
+*)
+
+Definition add va vb assignee : M unit :=
+  aget va >>= (fun a => aget vb >>= (fun b =>
+    match a, b with
+      | Int ia, Int ib => aput assignee (Int (add ia ib))
+      (* TODO: float + int by coercion, etc. *)
+      | _, _ => skip
+    end)).
+
+(* Memo: this line must be in order *)
+HB.instance Definition _ := isMonadSMCLocal.Build
+  VarName acto add.
+
+End modelsmc_local.
+End ModelSMCLocal.
+
+
+
+(*
+
+
 Module ModelSMCGlobal.
 Section modelsmc_global.
 
@@ -2030,12 +2142,9 @@ Variables (F P : UU0) (VarName : eqType).
 Local Notation SMCGlobalVars :=  (VarName -> SMCGlobal F P).
 Implicit Types (v : VarName) (g : MonadSMCLocals F P VarName) (e : MonadSMCLocals F P VarName -> MonadSMCLocals F P VarName) (A : UU0).
 
-Check SMCGlobalVars.
-Check MonadSMCLocals F P VarName.
-Check StateMonad.acto (VarName -> MonadSMCLocals F P VarName).
+Definition .
 
 *)
-
 (*
 Memo: acto application must be UU0 -> UU0.
 
@@ -2085,13 +2194,38 @@ https://stackoverflow.com/questions/32153710/what-does-error-universe-inconsiste
 *)
 
 (*
-Require Import PrimInt63.
-Require Sint63.
-Section Int63.
+
 
 Inductive smcty : Set :=
   | Int
   | Float
   | Array of nat & smcty.
 
+*)
+
+(*Memo:
+
+Maybe I'm wrong but it seems that we cannot define a dispatch function
+like this, because `a` will expect to have type `smcty`.
+
+The `a` is just a parametric type. It doesn't mean really "all" type.
+Maybe this is the reason?
+
+Definition checkSMC (a : Type) bool :=
+  match a with
+  | Int => true
+  | Float => true
+  | Array n ty => true
+  | _ => false
+  end.
+
+
+Definition checkSMC (F : UU0) (a : F) bool :=
+  match F with
+  | smcty => match a with
+             | Int => true
+             | _ => false
+             end
+  end.
+
 *)
\ No newline at end of file

From 07cd026de4d7471a376b5f5e907373de1dab07d2 Mon Sep 17 00:00:00 2001
From: Greg Weng <snowmantw@gmail.com>
Date: Fri, 14 Jul 2023 08:54:02 +0900
Subject: [PATCH 4/6] WIP: try to define scalar_product in SMC

---
 _CoqProject    |   1 +
 hierarchy.v    |  10 +++--
 monad_model.v  | 116 +++++++++++++++++++++++++++++++++----------------
 smc_protocol.v |  71 ++++++++++++++++++++++++++++++
 4 files changed, 157 insertions(+), 41 deletions(-)
 create mode 100644 smc_protocol.v

diff --git a/_CoqProject b/_CoqProject
index 66bb9250..1f4202be 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -29,5 +29,6 @@ example_monty.v
 smallstep.v
 example_transformer.v
 category_ext.v
+smc_protocol.v
 
 -R . monae
diff --git a/hierarchy.v b/hierarchy.v
index 266a0a5c..4320e710 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -1267,7 +1267,6 @@ Variable VarName : eqType.
 End smc_monad.
 
 
-
 (* SMC global monad: computes over Partial values only. *)
 HB.mixin Record isMonadSMCGlobal (VarName : eqType) (M : UU0 -> UU0) of Monad M := {
 
@@ -1278,8 +1277,11 @@ HB.mixin Record isMonadSMCGlobal (VarName : eqType) (M : UU0 -> UU0) of Monad M
      And it will directly assign related variables to the local env.
   *)
   
-  (* At interface level define a type in a record. *)
-  (* Got all deps in a record. *)
+  (* localM: At interface level define a type in a record.
+     it defines a "ready-to-run monad" can be run
+     by feeding the last argument unit.
+  *)
+  (* This is the way to get all deps in a record. *)
   localM : smcLocalMonad VarName;
   local : localM unit -> M unit;
 
@@ -1385,4 +1387,4 @@ have sequence of execution; but it is a pure monad, no SMC features inside.)
 There could be some extra steps before or after the operation itself,
 and two locals may have or have no information exchange.
 
-*)
\ No newline at end of file
+*)
diff --git a/monad_model.v b/monad_model.v
index 74fca9d5..da9564a4 100644
--- a/monad_model.v
+++ b/monad_model.v
@@ -5,7 +5,7 @@ From mathcomp Require Import classical_sets.
 From infotheo Require convex classical_sets_ext.
 Require Import monae_lib.
 From HB Require Import structures.
-Require Import hierarchy monad_lib fail_lib state_lib trace_lib.
+Require Import hierarchy smc_protocol monad_lib fail_lib state_lib trace_lib.
 Require Import monad_transformer.
 
 (******************************************************************************)
@@ -71,6 +71,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Locate UU0.
+
 Local Open Scope monae_scope.
 
 (* TODO *)
@@ -1981,28 +1983,6 @@ End modelmonadexceptstaterun.
 End ModelMonadExceptStateRun.
 
 
-
-
-(* ---- SMC type wrapper ---- *)
-(* ---- SMC data wrapper for dynamic typing ---- *)
-
-Require Import Floats PrimInt63.
-Require Import Bvector.
-Require Sint63.
-Section Int63.
-
-(* Memo: using `of` so it can be matched and extracted the wrapped inside *)
-Inductive smcvalue : Set :=
-| Int of int
-| Float of float
-| Bool of bool.
-
-(*Definition bvectorCapacity := 4611686018427387904*)
-Definition bvectorCapacity := 100.
-Definition smcglobal : UU0 := (smcvalue * Bvector bvectorCapacity * smcvalue * Bvector bvectorCapacity).
-
-End Int63.
-
 (* ---- Models of SMC monads ---- *)
 
 (* SMC Local Monad: a array monad with the element type is `smcvalue`. *)
@@ -2010,14 +1990,22 @@ End Int63.
 Module ModelSMCLocal.
 Section modelsmc_local.
 
+Require Import ZArith.
+
 Variables (VarName : eqType).
 
 Implicit Types (v va vb assignee : VarName).
 
-Definition acto := ModelArray.acto smcvalue VarName.
+Definition acto := ModelArray.acto smclocalval VarName.
 (* Memo: by this we define a type-specified monad (?) *)
 
 (* Automatically got run already? *)
+HB.instance Definition _ := Monad.on acto.
+(* The fix for the localM definition
+   Not instances from the HB outputs.
+   The defininion is a new thing and not completed (not equip all necessary types attach to that identifier).
+   So to solve it, define it here by copying
+*)
 
 Local Notation M := acto.
 Definition aget := ModelArray.aget.
@@ -2028,9 +2016,8 @@ Definition aput := ModelArray.aput.
 Definition add va vb assignee : M unit :=
   aget va >>= (fun a => aget vb >>= (fun b =>
     match a, b with
-      | Int ia, Int ib => aput assignee (Int (add ia ib))
+      | (Int ia, bva), (Int ib, bvb)=> aput assignee (Int (Z.add ia ib), bva)
       (* TODO: float + int by coercion, etc. *)
-      | _, _ => skip
     end)).
 
 (* Memo: this line must be in order *)
@@ -2054,10 +2041,12 @@ HB.about MonadSMCLocal.
 
 Definition localM := [the smcLocalMonad VarName of ModelSMCLocal.acto VarName].
 
+Implicit Types (v va vb assignee : VarName).
 
-Implicit Types (v va vb assignee : VarName) (MLocal : localM).
+(* Array of smclocal*)
+Definition smclocalstate := VarName -> smclocalval.
 
-Definition acto := ModelArray.acto smcglobal VarName.
+Definition acto := StateMonad.acto (smclocalstate * smclocalstate * commodity).
 (* Memo: by this we define a type-specified monad (?)
    It seems that except those methods required by the monad and functor definition,
    other methods can be type-specific, if the return value is still a monadic value,
@@ -2065,21 +2054,74 @@ Definition acto := ModelArray.acto smcglobal VarName.
 *)
 
 Local Notation M := acto.
-Definition aget := ModelArray.aget.
-Definition aput := ModelArray.aput.
-(* Otherwise they become monad PlusArray's aget and aput. *)
+ 
+(* symmetric local: they always run the same computation (like for SMC computations). *)
+(* NOT: only one local run it with its pure local variables. *)
+Definition local (F : localM unit) : M unit := fun state =>
+  match state with
+    | (localA, localB, c) => (tt, (snd (F localA), snd (F localB), c))
+  end.
 
-Check ModelArray.aget.
+Definition exchange v : M unit := fun state =>
+  match state with
+    | (localA, localB, c) => (tt, (insert v (localB v) localA, insert v (localB v) localA, c)) 
+  end.
+
+
+(* 1. Get Ra, Rb, ra, rb from commodity
+   2. Alice: Xa' = Xa + Ra, set as Bob's tmp var
+      --> issue: we cannot create new VarName `Xa'` inside, need to pass in.
+
+   3. Bob: Xb' = Xb + Rb, set as Alice's tmp var
+      --> issue: we cannot create new VarName `Xb'` inside, need to pass in.
 
-(* the parameter is just a local cannot be ran;
-   local program -- work on some monads.
+   4. Bob: generate a random variable yb
+      --> issue: we don't have random number generator. Need to assume that it exists.
+      --> issue: we cannot create new VarName `yb` inside, need to pass in.
 
-   already exists in the global, cannot be any local monad.
+   5. Bob: tb = Xa' x Xb'^t + rb - yb, set as Alice's tmp var
+      --> issue: we cannot create new VarName `tb` inside, need to pass in.
+
+   6. Alice: ya = tb - Ra x Xb'^t + Ra
+      --> issue: we cannot create new VarName `ya` inside, need to pass in.
 *)
+Definition sp_step1 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (xa : VarName) (xa' : VarName) : smclocalstate :=
+  insert xa' (only_partial (add_partial (get_Ra c) (get_partial (localA xa)))) localB.
+
+Definition sp_step2 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (xb : VarName) (xb' : VarName) : smclocalstate :=
+  insert xb' (only_partial (add_partial (get_Rb c) (get_partial (localB xb)))) localA.
+
+Definition sp_step4_5 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (xa' : VarName) (xb : VarName) (tb : VarName) : smclocalstate :=
+  insert tb (only_partial (dot_product (get_partial (localB xa')) (get_partial (localB xb))))
+
+Definition scalar_product va vb (xa : VarName) (xb : VarName) (ya : VarName) (yb : VarName) (tb : VarName) : M unit := fun state =>
+  match state with
+    | (localA, localB, c) =>
+    (tt,
+        (* step 1.)
+  end.
+
+
+(* Action Items
+1. Def the global monad as a state monad
+2. With two local monads
+3.
+
+LocalA [ vars --> (F, P), (F, P)... ]
+LocalB [ vars --> (F, P), (F, P)... ]
+Global steps to manipuate LocalA and LocalB.
 
-Definition local MLocal : M unit :=
-  localM >> skip.
+One global step will ... ?
 
+global_foo = compare
+
+runState (localMA, localMB)
+
+exchange 
+
+>>= fun (ma, mb) => 
+     aget v ma >>= (fun(va) => aget v mb >>= (fun (vb) => aput v vb ma) >> 
+*)
 (*
 
 Ask questions:
diff --git a/smc_protocol.v b/smc_protocol.v
new file mode 100644
index 00000000..9687423b
--- /dev/null
+++ b/smc_protocol.v
@@ -0,0 +1,71 @@
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require boolp.
+
+Require Import Bvector.
+Require Import ZArith.
+Require Import Zdigits.
+Require Export Zpower.
+Require Import Lia.
+Require Import Basics.
+Require Import hierarchy.
+
+Definition bvectorCapacity := 32.
+
+Inductive smcfull : Set :=
+| Int of Z.
+
+Definition smcpartial : UU0 := Bvector (S bvectorCapacity).
+
+Definition smclocalval : UU0 := (smcfull * smcpartial).
+
+(* Ra, Rb, ra, rb *)
+(* Assume that:
+   1. Ra, Rb are random vectors
+   2. ra is a random number
+   3. rb = Ra x Rb^t - ra
+*)
+Definition commodity : UU0 := (smcpartial * smcpartial * Z * Z).
+
+Definition get_Ra (c : commodity ) : smcpartial :=
+	match c with
+	| (Ra, _, _, _) => Ra
+	end.
+	
+Definition get_Rb (c : commodity ) : smcpartial :=
+	match c with
+	| (_, Rb, _, _) => Rb
+	end.
+
+Definition get_ra (c : commodity ) : Z :=
+	match c with
+	| (_, _, ra, _) => ra
+	end.
+
+Definition get_rb (c : commodity ) : Z :=
+	match c with
+	| (_, _, _, rb) => rb
+	end.
+
+Definition get_full (s : smclocalval) : smcfull := fst s.
+Definition get_partial (s : smclocalval) : smcpartial := snd s.
+
+Definition build_partial (s : smclocalval) : smclocalval :=
+	(get_full s,
+		match (get_full s) with
+		| Int i => Z_to_two_compl bvectorCapacity i
+		end
+	).
+
+Definition add_partial (a : smcpartial) (b : smcpartial) : smcpartial :=
+	Z_to_two_compl bvectorCapacity (Z.add (two_compl_value bvectorCapacity a) (two_compl_value bvectorCapacity b)).
+
+
+(* Dot product of two bit vectors and the result is a Z,
+   and then still return the result as a bit vector by the `Z_to_two_compl`
+   per the SMC requirement that computation parties hold partial results of SMC computations .
+*)
+Definition dot_product (a : smcpartial) (b : smcpartial) : smcpartial :=
+	a.  (*TODO: define it later*)
+
+Definition only_partial (p : smcpartial) : smclocalval :=
+	(Int 0, p).
\ No newline at end of file

From e61459acc83d21658681198391d7e146b8d5ed35 Mon Sep 17 00:00:00 2001
From: Greg Weng <snowmantw@gmail.com>
Date: Thu, 20 Jul 2023 23:13:34 +0900
Subject: [PATCH 5/6] WIP: refactor SMC scalar product steps

---
 hierarchy.v    |  1 +
 monad_model.v  | 61 +++++++++++++++++++++++++++++++++++++++-----------
 smc_protocol.v | 30 ++++++++++++++++++++-----
 3 files changed, 73 insertions(+), 19 deletions(-)

diff --git a/hierarchy.v b/hierarchy.v
index 4320e710..8db1391c 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -1291,6 +1291,7 @@ HB.mixin Record isMonadSMCGlobal (VarName : eqType) (M : UU0 -> UU0) of Monad M
   (* Exchange two partial variables with the same name at the both locals. *)
   exchange : VarName -> M unit;
 
+
   (* Split a Full variable to Partial SMC variable by SMC protocols. *)
   (* Example: at Alice side, `split wealth result` equal to:
 
diff --git a/monad_model.v b/monad_model.v
index da9564a4..7fa8f385 100644
--- a/monad_model.v
+++ b/monad_model.v
@@ -8,6 +8,7 @@ From HB Require Import structures.
 Require Import hierarchy smc_protocol monad_lib fail_lib state_lib trace_lib.
 Require Import monad_transformer.
 
+
 (******************************************************************************)
 (*                       Models for various monads                            *)
 (*                                                                            *)
@@ -2068,31 +2069,44 @@ Definition exchange v : M unit := fun state =>
   end.
 
 
-(* 1. Get Ra, Rb, ra, rb from commodity
-   2. Alice: Xa' = Xa + Ra, set as Bob's tmp var
+(* 0. Get Ra, Rb, ra, rb from commodity
+   1. Alice: Xa' = Xa + Ra, set as Bob's tmp var
       --> issue: we cannot create new VarName `Xa'` inside, need to pass in.
 
-   3. Bob: Xb' = Xb + Rb, set as Alice's tmp var
+   2. Bob: Xb' = Xb + Rb, set as Alice's tmp var
       --> issue: we cannot create new VarName `Xb'` inside, need to pass in.
 
-   4. Bob: generate a random variable yb
+   3. Bob: generate a random variable yb
       --> issue: we don't have random number generator. Need to assume that it exists.
       --> issue: we cannot create new VarName `yb` inside, need to pass in.
 
-   5. Bob: tb = Xa' x Xb'^t + rb - yb, set as Alice's tmp var
-      --> issue: we cannot create new VarName `tb` inside, need to pass in.
+   4. Bob: t_ = Xa' x Xb'^t + rb - yb, set `t_` as Alice's tmp var
+      --> issue: we cannot create new VarName `t_` inside, need to pass in.
 
-   6. Alice: ya = tb - Ra x Xb'^t + Ra
+   5. Alice: ya = t_ - Ra x Xb'^t + Ra
       --> issue: we cannot create new VarName `ya` inside, need to pass in.
+
+   Result: Alice, Bob: (ya, yb)
+   Property: ya + yb = Xa * Xb^t
+
 *)
-Definition sp_step1 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (xa : VarName) (xa' : VarName) : smclocalstate :=
-  insert xa' (only_partial (add_partial (get_Ra c) (get_partial (localA xa)))) localB.
 
-Definition sp_step2 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (xb : VarName) (xb' : VarName) : smclocalstate :=
-  insert xb' (only_partial (add_partial (get_Rb c) (get_partial (localB xb)))) localA.
+Definition sp_step1 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (Xa : VarName) (Xa' : VarName) : smclocalstate :=
+  insert Xa' (add_smcval (only_partial (get_Ra c)) (localA Xa)) localB. 
+
+Definition sp_step2 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (Xb : VarName) (Xb' : VarName) : smclocalstate :=
+  insert Xb' (add_smcval (only_partial (get_Rb c)) (localB Xb)) localA.
 
-Definition sp_step4_5 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (xa' : VarName) (xb : VarName) (tb : VarName) : smclocalstate :=
-  insert tb (only_partial (dot_product (get_partial (localB xa')) (get_partial (localB xb))))
+Definition sp_step3_4 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (Xa' : VarName) (Xb : VarName) (yb : VarName) (rb : VarName) (t_ : VarName) : smclocalstate :=
+  let Xa'_Xb' := dot_product_smcval (localB Xa') (localB Xb) in
+  let rb_yb := sub_smcval (localB rb) (localB yb) in
+    insert t_ (add_smcval Xa'_Xb' rb_yb) localA.
+
+Definition sp_step5 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (t_ : VarName) (Xb' : VarName) (ya : VarName) : smclocalstate :=
+  let Ra := only_partial (get_Ra c) in
+  let Ra_Xb' := dot_product_smcval Ra (localA Xb') in
+  let Ra_Xb'_Ra := add_smcval Ra_Xb' Ra in
+    insert ya (sub_smcval (localA t_) Ra_Xb'_Ra) localA.
 
 Definition scalar_product va vb (xa : VarName) (xb : VarName) (ya : VarName) (yb : VarName) (tb : VarName) : M unit := fun state =>
   match state with
@@ -2270,4 +2284,25 @@ Definition checkSMC (F : UU0) (a : F) bool :=
              end
   end.
 
+*)
+
+(*
+
+
+--> We need array as the heaps, but we also need named registers for computations
+    completed by a register machine (stack could also be used but we need to rewrite the algorithm).
+
+--> Each step, the new environment of the SMC program will be stored in the two heaps.
+    But for each program computation, it needs to load things from the heaps to this "register view",
+    (mainly for the vars will be used later),
+    and then compute the program,
+    and then store the result back to the two heaps.
+
+--> This is because the heaps (for the whole SMC program) are apparently different from the
+    environment needed by one specific SMC computation.
+
+--> But in theory we can compile the whole program and decide all named "register" the whole program
+    will use. So no need to have the heaps.
+
+
 *)
\ No newline at end of file
diff --git a/smc_protocol.v b/smc_protocol.v
index 9687423b..d05b1de4 100644
--- a/smc_protocol.v
+++ b/smc_protocol.v
@@ -56,16 +56,34 @@ Definition build_partial (s : smclocalval) : smclocalval :=
 		end
 	).
 
-Definition add_partial (a : smcpartial) (b : smcpartial) : smcpartial :=
-	Z_to_two_compl bvectorCapacity (Z.add (two_compl_value bvectorCapacity a) (two_compl_value bvectorCapacity b)).
-
-
 (* Dot product of two bit vectors and the result is a Z,
    and then still return the result as a bit vector by the `Z_to_two_compl`
    per the SMC requirement that computation parties hold partial results of SMC computations .
 *)
-Definition dot_product (a : smcpartial) (b : smcpartial) : smcpartial :=
+Definition dot_product_partial (a : smcpartial) (b : smcpartial) : smcpartial :=
 	a.  (*TODO: define it later*)
 
 Definition only_partial (p : smcpartial) : smclocalval :=
-	(Int 0, p).
\ No newline at end of file
+	(Int 0, p).
+
+Definition binop_partial (a : smcpartial) (b : smcpartial) (op: Z -> Z -> Z) : smcpartial :=
+	Z_to_two_compl bvectorCapacity (op (two_compl_value bvectorCapacity a) (two_compl_value bvectorCapacity b)).
+
+Definition add_partial (a : smcpartial) (b : smcpartial) : smcpartial :=
+	binop_partial a b Z.add.
+
+Definition sub_partial (a : smcpartial) (b : smcpartial) : smcpartial :=
+	binop_partial a b Z.sub.
+
+Definition binop (a : smclocalval) (b : smclocalval) (op: smcpartial -> smcpartial -> smcpartial) : smclocalval :=
+	only_partial (op (get_partial a) (get_partial b)).
+
+Definition add_smcval (a : smclocalval) (b : smclocalval) : smclocalval := 
+	only_partial (add_partial (get_partial a) (get_partial b)).
+
+Definition sub_smcval (a : smclocalval) (b : smclocalval) : smclocalval := 
+	only_partial (sub_partial (get_partial a) (get_partial b)).
+
+Definition dot_product_smcval (a : smclocalval) (b : smclocalval) : smclocalval :=
+	only_partial (dot_product_partial (get_partial a) (get_partial b)).
+	

From c3108886ffca2e483a7d7fe8632cdb6833bb6789 Mon Sep 17 00:00:00 2001
From: Greg Weng <snowmantw@gmail.com>
Date: Fri, 21 Jul 2023 08:05:50 +0900
Subject: [PATCH 6/6] WIP: try to make each step in the global monad a new env
 + rand numbers

---
 hierarchy.v   | 16 ++++++++++++++++
 monad_model.v | 39 +++++++++++++++++++++++++++++++--------
 2 files changed, 47 insertions(+), 8 deletions(-)

diff --git a/hierarchy.v b/hierarchy.v
index 8db1391c..da22f688 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -1285,6 +1285,22 @@ HB.mixin Record isMonadSMCGlobal (VarName : eqType) (M : UU0 -> UU0) of Monad M
   localM : smcLocalMonad VarName;
   local : localM unit -> M unit;
 
+  (* SMC version of the scalar product:
+
+       scalar_product Xa Xb -> (ya, yb), where ya + yb = Xa x Xb
+
+     In this interface it becomes a SMT style:
+ 
+       scalar_product x -> (ya, yb)
+    
+     Which means both Alice and Bob should hold the same name varialbe `x`
+     in their environments, not two variables with different names on two locals.
+
+     The second VarName is the assignee. So we can put the result back to the two locals.
+     This keeps the interface still in the single-assignment form.
+  *)
+  scalar_product : VarName -> VarName -> M unit;
+
   (* Note: smcLocalMonad is a record -- the type of computation in the monad *)
   (*local :  smcLocalMonad VarName -> M unit;*)
 
diff --git a/monad_model.v b/monad_model.v
index 7fa8f385..608893f7 100644
--- a/monad_model.v
+++ b/monad_model.v
@@ -2091,6 +2091,32 @@ Definition exchange v : M unit := fun state =>
 
 *)
 
+(* Before each stateful step in this global model monad,
+   since every global step means a new SMC protocol computation (otherwise it should be done by `local`),
+   the random variables from the commodity server must be refreshed. It should work like:
+
+    runState
+      step1 >>
+      step2 >>
+      step3
+
+    = (result, state)
+
+  becomes:
+
+    runState
+      refresh_env >> step1 >>
+      refresh_env >> step2 >>
+      refresh_env >> step3
+
+    = (result, state)
+
+  TODO: it is better to define a customized `pure` (>>) and `bind` (>>=) so each step of this monad
+  will naturally come with a new environment.
+*)
+Definition refresh_env : M unit := fun state =>
+  (tt, state).
+
 Definition sp_step1 (localA : smclocalstate) (localB : smclocalstate) (c : commodity) (Xa : VarName) (Xa' : VarName) : smclocalstate :=
   insert Xa' (add_smcval (only_partial (get_Ra c)) (localA Xa)) localB. 
 
@@ -2108,13 +2134,8 @@ Definition sp_step5 (localA : smclocalstate) (localB : smclocalstate) (c : commo
   let Ra_Xb'_Ra := add_smcval Ra_Xb' Ra in
     insert ya (sub_smcval (localA t_) Ra_Xb'_Ra) localA.
 
-Definition scalar_product va vb (xa : VarName) (xb : VarName) (ya : VarName) (yb : VarName) (tb : VarName) : M unit := fun state =>
-  match state with
-    | (localA, localB, c) =>
-    (tt,
-        (* step 1.)
-  end.
-
+Definition scalar_product v assignee : M unit := fun state =>
+  (tt, state).
 
 (* Action Items
 1. Def the global monad as a state monad
@@ -2288,6 +2309,7 @@ Definition checkSMC (F : UU0) (a : F) bool :=
 
 (*
 
+Not sure
 
 --> We need array as the heaps, but we also need named registers for computations
     completed by a register machine (stack could also be used but we need to rewrite the algorithm).
@@ -2305,4 +2327,5 @@ Definition checkSMC (F : UU0) (a : F) bool :=
     will use. So no need to have the heaps.
 
 
-*)
\ No newline at end of file
+*)
+