Repository: ergoplatform/sigma-rust (language: rust)

Issue:
Update SigmaUSD contracts serialization tests from EIP-15
https://github.com/ergoplatform/eips/pull/28


Discussion / hints:

Fix patch:
diff --git a/ergo-lib/CHANGELOG.md b/ergo-lib/CHANGELOG.md
index 66bb5f1e7..f06ce9475 100644
--- a/ergo-lib/CHANGELOG.md
+++ b/ergo-lib/CHANGELOG.md
@@ -11,6 +11,8 @@ and this project adheres to [Semantic Versioning](http://semver.org/).
 - `Coll.indexOf`, `flatMap`, `forall` IR nodes (evaluation, serialization) [#220](https://github.com/ergoplatform/sigma-rust/pull/220);
 - Complete types serialization implementation [#223](https://github.com/ergoplatform/sigma-rust/pull/223);
 - `Tuple` constructor evaluation and serialization [#223](https://github.com/ergoplatform/sigma-rust/pull/223);
+- Type unification (`SMethod` specialization) [#225](https://github.com/ergoplatform/sigma-rust/pull/226);
+- `SigmaAnd`, `SigmaOr` serialization [#225](https://github.com/ergoplatform/sigma-rust/pull/226);
 
 ## [0.8.0] - 2021-03-22
 
diff --git a/ergotree-interpreter/src/contracts.rs b/ergotree-interpreter/src/contracts.rs
index 6633ebcd1..8f822cd79 100644
--- a/ergotree-interpreter/src/contracts.rs
+++ b/ergotree-interpreter/src/contracts.rs
@@ -167,6 +167,48 @@ mod tests {
         assert!(res);
     }
 
+    #[test]
+    fn ageusd_bank_full() {
+        // from eip-15 https://github.com/ergoplatform/eips/pull/27/files
+        let p2s_addr_str = "MUbV38YgqHy7XbsoXWF5z7EZm524Ybdwe5p9WDrbhruZRtehkRPT92imXer2eTkjwPDfboa1pR3zb3deVKVq3H7Xt98qcTqLuSBSbHb7izzo5jphEpcnqyKJ2xhmpNPVvmtbdJNdvdopPrHHDBbAGGeW7XYTQwEeoRfosXzcDtiGgw97b2aqjTsNFmZk7khBEQywjYfmoDc9nUCJMZ3vbSspnYo3LarLe55mh2Np8MNJqUN9APA6XkhZCrTTDRZb1B4krgFY1sVMswg2ceqguZRvC9pqt3tUUxmSnB24N6dowfVJKhLXwHPbrkHViBv1AKAJTmEaQW2DN1fRmD9ypXxZk8GXmYtxTtrj3BiunQ4qzUCu1eGzxSREjpkFSi2ATLSSDqUwxtRz639sHM6Lav4axoJNPCHbY8pvuBKUxgnGRex8LEGM8DeEJwaJCaoy8dBw9Lz49nq5mSsXLeoC4xpTUmp47Bh7GAZtwkaNreCu74m9rcZ8Di4w1cmdsiK1NWuDh9pJ2Bv7u3EfcurHFVqCkT3P86JUbKnXeNxCypfrWsFuYNKYqmjsix82g9vWcGMmAcu5nagxD4iET86iE2tMMfZZ5vqZNvntQswJyQqv2Wc6MTh4jQx1q2qJZCQe4QdEK63meTGbZNNKMctHQbp3gRkZYNrBtxQyVtNLR8xEY8zGp85GeQKbb37vqLXxRpGiigAdMe3XZA4hhYPmAAU5hpSMYaRAjtvvMT3bNiHRACGrfjvSsEG9G2zY5in2YWz5X9zXQLGTYRsQ4uNFkYoQRCBdjNxGv6R58Xq74zCgt19TxYZ87gPWxkXpWwTaHogG1eps8WXt8QzwJ9rVx6Vu9a5GjtcGsQxHovWmYixgBU8X9fPNJ9UQhYyAWbjtRSuVBtDAmoV1gCBEPwnYVP5GCGhCocbwoYhZkZjFZy6ws4uxVLid3FxuvhWvQrVEDYp7WRvGXbNdCbcSXnbeTrPMey1WPaXX";
+        let encoder = AddressEncoder::new(NetworkPrefix::Mainnet);
+        let addr = encoder.parse_address_from_str(p2s_addr_str).unwrap();
+        let script: Rc<Expr> = addr.script().unwrap().proposition().unwrap();
+        dbg!(&script);
+        // let res: bool = eval_out_wo_ctx::<SigmaProp>(script.as_ref())
+        //     .try_into()
+        //     .unwrap();
+        // assert!(!res);
+    }
+
+    #[test]
+    fn ageusd_update() {
+        // from eip-15 https://github.com/ergoplatform/eips/pull/27/files
+        let p2s_addr_str = "VLyjpv3dse3PbatT83GnDkBQasGqY52dAEdi9XpXhuSUn1FS1Tm7XxtAgmBiqY9pJXtEAsDKwX9ygSjrFu7vnUQZudhC2sSmxhxqgD3ZxJ2VsGwmPG77F6EiEZhcq71oqEq31y9XvCCXL5nqqszdENPAVhu7xT296qZ7w1x6hmwdh9ZE89bjfgbhfNYopoqsCaNLWYHJ12TDSY93kaGqCVKSu6gEF1gLpXBfRCnAPPxYswJPmK8oWDn8PKrUGs3MjVsj6bGXiW3VTGP4VsNH8YSSkjyj1FZ9azLsyfnNJ3zah2zUHdCCqY6PjH9JfHf9joCPf6TusvXgr71XWvh5e2HPEPQr4eJMD4S96cGTiSs3J5XcRd1tCDYoiis8nxv99zFFhHgpqXHgeqjhJ5sPot9eRYTsmm4cRTVLXYAiuKPS2qW5";
+        let encoder = AddressEncoder::new(NetworkPrefix::Mainnet);
+        let addr = encoder.parse_address_from_str(p2s_addr_str).unwrap();
+        let script: Rc<Expr> = addr.script().unwrap().proposition().unwrap();
+        dbg!(&script);
+        // let res: bool = eval_out_wo_ctx::<SigmaProp>(script.as_ref())
+        //     .try_into()
+        //     .unwrap();
+        // assert!(!res);
+    }
+
+    #[test]
+    fn ageusd_ballot() {
+        // from eip-15 https://github.com/ergoplatform/eips/pull/27/files
+        let p2s_addr_str = "22ELWBHzyWGjPRE48ZJDfFmD24myYdG3vHz8CipSS7rgE65ABmEj9QJiy3rG2PTJeCaZw9VX56GY6uoA3hQch7i5BfFU3AprUWTABi4X1VWtRdK9yrYJkmN6fq8hGfvmWTrsyh4fXZoGETpLuXQViYo194ajej2h7dr3oqNATdMskSXzxJi83bFdAvQ";
+        let encoder = AddressEncoder::new(NetworkPrefix::Mainnet);
+        let addr = encoder.parse_address_from_str(p2s_addr_str).unwrap();
+        let script: Rc<Expr> = addr.script().unwrap().proposition().unwrap();
+        dbg!(&script);
+        // let res: bool = eval_out_wo_ctx::<SigmaProp>(script.as_ref())
+        //     .try_into()
+        //     .unwrap();
+        // assert!(!res);
+    }
+
     #[test]
     fn amm_simple_pool() {
         // from eip-14 https://github.com/ergoplatform/eips/pull/27/files
diff --git a/ergotree-interpreter/src/eval/expr.rs b/ergotree-interpreter/src/eval/expr.rs
index 8d47278ac..75a017442 100644
--- a/ergotree-interpreter/src/eval/expr.rs
+++ b/ergotree-interpreter/src/eval/expr.rs
@@ -50,6 +50,8 @@ impl Evaluable for Expr {
             Expr::Negation(op) => op.eval(env, ctx),
             Expr::ForAll(op) => op.eval(env, ctx),
             Expr::Tuple(op) => op.eval(env, ctx),
+            Expr::SigmaAnd(_) => todo!(),
+            Expr::SigmaOr(_) => todo!(),
         }
     }
 }
diff --git a/ergotree-ir/src/mir.rs b/ergotree-ir/src/mir.rs
index ce9df7a77..45f7cb408 100644
--- a/ergotree-ir/src/mir.rs
+++ b/ergotree-ir/src/mir.rs
@@ -60,6 +60,8 @@ pub mod or;
 pub mod property_call;
 /// Select a field of the tuple value
 pub mod select_field;
+pub mod sigma_and;
+pub mod sigma_or;
 /// Extract serialized bytes of a SigmaProp value
 pub mod sigma_prop_bytes;
 /// Tuple of elements
diff --git a/ergotree-ir/src/mir/expr.rs b/ergotree-ir/src/mir/expr.rs
index 60f660e82..2be3902fb 100644
--- a/ergotree-ir/src/mir/expr.rs
+++ b/ergotree-ir/src/mir/expr.rs
@@ -44,6 +44,8 @@ use super::option_is_defined::OptionIsDefined;
 use super::or::Or;
 use super::property_call::PropertyCall;
 use super::select_field::SelectField;
+use super::sigma_and::SigmaAnd;
+use super::sigma_or::SigmaOr;
 use super::sigma_prop_bytes::SigmaPropBytes;
 use super::tuple::Tuple;
 use super::upcast::Upcast;
@@ -141,6 +143,10 @@ pub enum Expr {
     CreateProveDlog(CreateProveDlog),
     /// Extract serialized bytes of a SigmaProp value
     SigmaPropBytes(SigmaPropBytes),
+    /// AND conjunction for sigma propositions
+    SigmaAnd(SigmaAnd),
+    /// OR conjunction for sigma propositions
+    SigmaOr(SigmaOr),
 }
 
 impl Expr {
@@ -187,6 +193,8 @@ impl Expr {
             Expr::Negation(op) => op.op_code(),
             Expr::ForAll(op) => op.op_code(),
             Expr::Tuple(op) => op.op_code(),
+            Expr::SigmaAnd(op) => op.op_code(),
+            Expr::SigmaOr(op) => op.op_code(),
         }
     }
 
@@ -233,6 +241,8 @@ impl Expr {
             Expr::Negation(v) => v.tpe(),
             Expr::ForAll(v) => v.tpe(),
             Expr::Tuple(v) => v.tpe(),
+            Expr::SigmaAnd(v) => v.tpe(),
+            Expr::SigmaOr(v) => v.tpe(),
         }
     }
 
diff --git a/ergotree-ir/src/mir/or.rs b/ergotree-ir/src/mir/or.rs
index 86ed8efef..2c6289614 100644
--- a/ergotree-ir/src/mir/or.rs
+++ b/ergotree-ir/src/mir/or.rs
@@ -74,7 +74,7 @@ mod tests {
     proptest! {
 
         #[test]
-        fn ser_roundtrip(v in any_with::<Or>(2)) {
+        fn ser_roundtrip(v in any_with::<Or>(1)) {
             let expr: Expr = v.into();
             prop_assert_eq![sigma_serialize_roundtrip(&expr), expr];
         }
diff --git a/ergotree-ir/src/mir/sigma_and.rs b/ergotree-ir/src/mir/sigma_and.rs
new file mode 100644
index 000000000..20e52baec
--- /dev/null
+++ b/ergotree-ir/src/mir/sigma_and.rs
@@ -0,0 +1,82 @@
+//! AND conjunction for sigma propositions
+
+use crate::serialization::op_code::OpCode;
+use crate::serialization::sigma_byte_reader::SigmaByteRead;
+use crate::serialization::sigma_byte_writer::SigmaByteWrite;
+use crate::serialization::SerializationError;
+use crate::serialization::SigmaSerializable;
+use crate::types::stype::SType;
+
+use super::expr::Expr;
+
+/// AND conjunction for sigma propositions
+#[derive(PartialEq, Eq, Debug, Clone)]
+pub struct SigmaAnd {
+    /// Collection of SSigmaProp
+    pub items: Vec<Expr>,
+}
+
+impl SigmaAnd {
+    pub(crate) const OP_CODE: OpCode = OpCode::SIGMA_AND;
+
+    /// Type
+    pub fn tpe(&self) -> SType {
+        SType::SSigmaProp
+    }
+
+    pub(crate) fn op_code(&self) -> OpCode {
+        Self::OP_CODE
+    }
+}
+
+impl SigmaSerializable for SigmaAnd {
+    fn sigma_serialize<W: SigmaByteWrite>(&self, w: &mut W) -> Result<(), std::io::Error> {
+        self.items.sigma_serialize(w)
+    }
+
+    fn sigma_parse<R: SigmaByteRead>(r: &mut R) -> Result<Self, SerializationError> {
+        Ok(Self {
+            items: Vec::<Expr>::sigma_parse(r)?,
+        })
+    }
+}
+
+/// Arbitrary impl
+#[cfg(feature = "arbitrary")]
+mod arbitrary {
+    use super::*;
+    use crate::mir::constant::Constant;
+    use proptest::collection::vec;
+    use proptest::prelude::*;
+
+    impl Arbitrary for SigmaAnd {
+        type Strategy = BoxedStrategy<Self>;
+        type Parameters = ();
+
+        fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
+            vec(any_with::<Constant>(SType::SSigmaProp.into()), 2..5)
+                .prop_map(|constants| Self {
+                    items: constants.into_iter().map(|c| c.into()).collect(),
+                })
+                .boxed()
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::mir::expr::Expr;
+    use crate::serialization::sigma_serialize_roundtrip;
+    use proptest::prelude::*;
+
+    proptest! {
+
+        #[test]
+        fn ser_roundtrip(v in any::<SigmaAnd>()) {
+            let expr: Expr = v.into();
+            prop_assert_eq![sigma_serialize_roundtrip(&expr), expr];
+        }
+
+    }
+}
diff --git a/ergotree-ir/src/mir/sigma_or.rs b/ergotree-ir/src/mir/sigma_or.rs
new file mode 100644
index 000000000..dbd666aff
--- /dev/null
+++ b/ergotree-ir/src/mir/sigma_or.rs
@@ -0,0 +1,82 @@
+//! OR conjunction for sigma propositions
+
+use crate::serialization::op_code::OpCode;
+use crate::serialization::sigma_byte_reader::SigmaByteRead;
+use crate::serialization::sigma_byte_writer::SigmaByteWrite;
+use crate::serialization::SerializationError;
+use crate::serialization::SigmaSerializable;
+use crate::types::stype::SType;
+
+use super::expr::Expr;
+
+/// OR conjunction for sigma propositions
+#[derive(PartialEq, Eq, Debug, Clone)]
+pub struct SigmaOr {
+    /// Collection of SSigmaProp
+    pub items: Vec<Expr>,
+}
+
+impl SigmaOr {
+    pub(crate) const OP_CODE: OpCode = OpCode::SIGMA_OR;
+
+    /// Type
+    pub fn tpe(&self) -> SType {
+        SType::SSigmaProp
+    }
+
+    pub(crate) fn op_code(&self) -> OpCode {
+        Self::OP_CODE
+    }
+}
+
+impl SigmaSerializable for SigmaOr {
+    fn sigma_serialize<W: SigmaByteWrite>(&self, w: &mut W) -> Result<(), std::io::Error> {
+        self.items.sigma_serialize(w)
+    }
+
+    fn sigma_parse<R: SigmaByteRead>(r: &mut R) -> Result<Self, SerializationError> {
+        Ok(Self {
+            items: Vec::<Expr>::sigma_parse(r)?,
+        })
+    }
+}
+
+/// Arbitrary impl
+#[cfg(feature = "arbitrary")]
+mod arbitrary {
+    use super::*;
+    use crate::mir::constant::Constant;
+    use proptest::collection::vec;
+    use proptest::prelude::*;
+
+    impl Arbitrary for SigmaOr {
+        type Strategy = BoxedStrategy<Self>;
+        type Parameters = ();
+
+        fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
+            vec(any_with::<Constant>(SType::SSigmaProp.into()), 2..5)
+                .prop_map(|constants| Self {
+                    items: constants.into_iter().map(|c| c.into()).collect(),
+                })
+                .boxed()
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::mir::expr::Expr;
+    use crate::serialization::sigma_serialize_roundtrip;
+    use proptest::prelude::*;
+
+    proptest! {
+
+        #[test]
+        fn ser_roundtrip(v in any::<SigmaOr>()) {
+            let expr: Expr = v.into();
+            prop_assert_eq![sigma_serialize_roundtrip(&expr), expr];
+        }
+
+    }
+}
diff --git a/ergotree-ir/src/serialization/expr.rs b/ergotree-ir/src/serialization/expr.rs
index 1b4c79fba..34f057e51 100644
--- a/ergotree-ir/src/serialization/expr.rs
+++ b/ergotree-ir/src/serialization/expr.rs
@@ -39,6 +39,8 @@ use crate::mir::option_is_defined::OptionIsDefined;
 use crate::mir::or::Or;
 use crate::mir::property_call::PropertyCall;
 use crate::mir::select_field::SelectField;
+use crate::mir::sigma_and::SigmaAnd;
+use crate::mir::sigma_or::SigmaOr;
 use crate::mir::sigma_prop_bytes::SigmaPropBytes;
 use crate::mir::tuple::Tuple;
 use crate::mir::upcast::Upcast;
@@ -105,6 +107,8 @@ impl SigmaSerializable for Expr {
                     Expr::Negation(op) => op.sigma_serialize(w),
                     Expr::ForAll(op) => op.sigma_serialize(w),
                     Expr::Tuple(op) => op.sigma_serialize(w),
+                    Expr::SigmaAnd(op) => op.sigma_serialize(w),
+                    Expr::SigmaOr(op) => op.sigma_serialize(w),
                 }
             }
         }
@@ -192,6 +196,8 @@ impl SigmaSerializable for Expr {
                 CreateProveDlog::OP_CODE => Ok(CreateProveDlog::sigma_parse(r)?.into()),
                 SigmaPropBytes::OP_CODE => Ok(SigmaPropBytes::sigma_parse(r)?.into()),
                 Tuple::OP_CODE => Ok(Tuple::sigma_parse(r)?.into()),
+                SigmaAnd::OP_CODE => Ok(SigmaAnd::sigma_parse(r)?.into()),
+                SigmaOr::OP_CODE => Ok(SigmaOr::sigma_parse(r)?.into()),
                 o => Err(SerializationError::NotImplementedOpCode(format!(
                     "{0}(shift {1})",
                     o.value(),
diff --git a/ergotree-ir/src/serialization/method_call.rs b/ergotree-ir/src/serialization/method_call.rs
index 8603bd56d..5c3f47fd6 100644
--- a/ergotree-ir/src/serialization/method_call.rs
+++ b/ergotree-ir/src/serialization/method_call.rs
@@ -25,7 +25,8 @@ impl SigmaSerializable for MethodCall {
         let method_id = MethodId::sigma_parse(r)?;
         let obj = Expr::sigma_parse(r)?;
         let args = Vec::<Expr>::sigma_parse(r)?;
-        let method = SMethod::from_ids(type_id, method_id);
+        let arg_types = args.iter().map(|arg| arg.tpe()).collect();
+        let method = SMethod::from_ids(type_id, method_id).specialize_for(obj.tpe(), arg_types)?;
         Ok(MethodCall::new(obj, method, args)?)
     }
 }
@@ -33,19 +34,21 @@ impl SigmaSerializable for MethodCall {
 #[cfg(test)]
 #[cfg(feature = "arbitrary")]
 mod tests {
-    use crate::mir::constant::Constant;
     use crate::mir::expr::Expr;
-    use crate::mir::global_vars::GlobalVars;
     use crate::mir::method_call::MethodCall;
     use crate::serialization::sigma_serialize_roundtrip;
-    use crate::types::sbox;
+    use crate::types::scoll;
+    use crate::types::stype::SType;
+    use crate::types::stype_param::STypeVar;
 
     #[test]
-    fn ser_roundtrip_property() {
+    fn ser_roundtrip() {
         let mc: Expr = MethodCall::new(
-            GlobalVars::SelfBox.into(),
-            sbox::GET_REG_METHOD.clone(),
-            vec![Constant::from(0i8).into()],
+            vec![1i64, 2i64].into(),
+            scoll::INDEX_OF_METHOD
+                .clone()
+                .with_concrete_types(&[(STypeVar::t(), SType::SLong)].iter().cloned().collect()),
+            vec![2i64.into(), 0i32.into()],
         )
         .unwrap()
         .into();
diff --git a/ergotree-ir/src/serialization/serializable.rs b/ergotree-ir/src/serialization/serializable.rs
index 2c85dcc70..68ff2f870 100644
--- a/ergotree-ir/src/serialization/serializable.rs
+++ b/ergotree-ir/src/serialization/serializable.rs
@@ -2,6 +2,7 @@
 use crate::mir::expr::InvalidArgumentError;
 use crate::mir::val_def::ValId;
 use crate::types::stuple::STupleItemsOutOfBoundsError;
+use crate::types::type_unify::TypeUnificationError;
 
 use super::{
     constant_store::ConstantStore,
@@ -84,6 +85,12 @@ impl From<STupleItemsOutOfBoundsError> for SerializationError {
     }
 }
 
+impl From<TypeUnificationError> for SerializationError {
+    fn from(e: TypeUnificationError) -> Self {
+        SerializationError::Misc(format!("{:?}", e))
+    }
+}
+
 /// Consensus-critical serialization for Ergo
 pub trait SigmaSerializable: Sized {
     /// Write `self` to the given `writer`.
diff --git a/ergotree-ir/src/serialization/types.rs b/ergotree-ir/src/serialization/types.rs
index 18922203f..4836fc828 100644
--- a/ergotree-ir/src/serialization/types.rs
+++ b/ergotree-ir/src/serialization/types.rs
@@ -146,7 +146,7 @@ impl SigmaSerializable for SType {
     fn sigma_serialize<W: SigmaByteWrite>(&self, w: &mut W) -> Result<(), io::Error> {
         // for reference see http://github.com/ScorexFoundation/sigmastate-interpreter/blob/25251c1313b0131835f92099f02cef8a5d932b5e/sigmastate/src/main/scala/sigmastate/serialization/TypeSerializer.scala#L25-L25
         match self {
-            SType::SFunc(_) => todo!(),
+            SType::SFunc(_) => panic!("SFunc is not supposed to be here"),
             SType::SAny => self.type_code().sigma_serialize(w),
             SType::SBoolean => self.type_code().sigma_serialize(w),
             SType::SByte => self.type_code().sigma_serialize(w),
diff --git a/ergotree-ir/src/types.rs b/ergotree-ir/src/types.rs
index 983859b28..3964024a0 100644
--- a/ergotree-ir/src/types.rs
+++ b/ergotree-ir/src/types.rs
@@ -17,3 +17,5 @@ pub mod stuple;
 pub mod stype_companion;
 /// Type parameters for generic signatures
 pub mod stype_param;
+/// Types unification
+pub mod type_unify;
diff --git a/ergotree-ir/src/types/sbox.rs b/ergotree-ir/src/types/sbox.rs
index d21318511..416db845b 100644
--- a/ergotree-ir/src/types/sbox.rs
+++ b/ergotree-ir/src/types/sbox.rs
@@ -57,7 +57,7 @@ lazy_static! {
         name: "getReg",
         tpe: SFunc {
             t_dom: vec![SType::SBox, SType::SByte],
-            t_range: Box::new(SType::SOption(Box::new(SType::STypeVar(STypeVar::t())))),
+            t_range: SType::SOption(Box::new(STypeVar::t().into())).into(),
             tpe_params: vec![],
         },
     };
@@ -72,10 +72,11 @@ lazy_static! {
         name: "tokens",
         tpe: SFunc {
             t_dom: vec![SType::SBox],
-            t_range: Box::new(SType::SColl(Box::new(SType::STuple(STuple::pair(
-                                SType::SColl(Box::new(SType::SByte)),
-                                SType::SLong
-            ))))),
+            t_range: SType::SColl(Box::new(
+                    STuple::pair(
+                        SType::SColl(SType::SByte.into()),
+                        SType::SLong
+                    ).into())).into(),
             tpe_params: vec![],
         },
     };
diff --git a/ergotree-ir/src/types/scoll.rs b/ergotree-ir/src/types/scoll.rs
index 13dff2046..fd3aba737 100644
--- a/ergotree-ir/src/types/scoll.rs
+++ b/ergotree-ir/src/types/scoll.rs
@@ -38,7 +38,7 @@ lazy_static! {
         method_id: INDEX_OF_METHOD_ID,
         name: "indexOf",
         tpe: SFunc {
-            t_dom: vec![SType::SColl(SType::STypeVar(STypeVar::t()).into()), SType::STypeVar(STypeVar::t()), SType::SInt],
+            t_dom: vec![SType::SColl(SType::STypeVar(STypeVar::t()).into()), STypeVar::t().into(), SType::SInt],
             t_range: SType::SInt.into(),
             tpe_params: vec![],
         },
@@ -51,14 +51,13 @@ lazy_static! {
     static ref FLATMAP_METHOD_DESC: SMethodDesc = SMethodDesc {
         method_id: FLATMAP_METHOD_ID,
         name: "flatMap",
-        tpe: SFunc {
-            t_dom: vec![SType::SColl(SType::STypeVar(STypeVar::iv()).into()),
-            SType::SFunc(
-                SFunc::new(vec![SType::STypeVar(STypeVar::iv())], SType::STypeVar(STypeVar::ov()), vec![] ))
-            ],
-            t_range: SType::SColl(SType::STypeVar(STypeVar::ov()).into()).into(),
-            tpe_params: vec![],
-        },
+        tpe: SFunc::new(
+            vec![
+                SType::SColl(SType::STypeVar(STypeVar::iv()).into()),
+                SFunc::new(vec![STypeVar::iv().into()], STypeVar::ov().into()).into()
+                ],
+            SType::SColl(SType::STypeVar(STypeVar::ov()).into()),
+        ),
     };
     /// Coll.flatMap
     pub static ref FLATMAP_METHOD: SMethod = SMethod::new(&S_COLL_TYPE_COMPANION, FLATMAP_METHOD_DESC.clone());
diff --git a/ergotree-ir/src/types/sfunc.rs b/ergotree-ir/src/types/sfunc.rs
index 719a02404..f838a3304 100644
--- a/ergotree-ir/src/types/sfunc.rs
+++ b/ergotree-ir/src/types/sfunc.rs
@@ -17,11 +17,11 @@ pub struct SFunc {
 
 impl SFunc {
     /// Create new SFunc
-    pub fn new(t_dom: Vec<SType>, t_range: SType, tpe_params: Vec<STypeParam>) -> Self {
+    pub fn new(t_dom: Vec<SType>, t_range: SType) -> Self {
         Self {
             t_dom,
             t_range: t_range.into(),
-            tpe_params,
+            tpe_params: vec![],
         }
     }
 
@@ -41,4 +41,11 @@ impl SFunc {
             tpe_params: remaining_vars,
         }
     }
+
+    /// Returns function parameter types (t_dom) with added result type (t_range)
+    pub fn t_dom_plus_range(&self) -> Vec<SType> {
+        let mut res = self.t_dom.clone();
+        res.push(*self.t_range.clone());
+        res
+    }
 }
diff --git a/ergotree-ir/src/types/smethod.rs b/ergotree-ir/src/types/smethod.rs
index 5b8434a56..2da31946c 100644
--- a/ergotree-ir/src/types/smethod.rs
+++ b/ergotree-ir/src/types/smethod.rs
@@ -10,6 +10,8 @@ use super::sfunc::SFunc;
 use super::stype::SType;
 use super::stype_companion::STypeCompanion;
 use super::stype_param::STypeVar;
+use super::type_unify::unify_many;
+use super::type_unify::TypeUnificationError;
 
 /// Method id unique among the methods of the same object
 #[derive(PartialEq, Eq, Debug, Clone)]
@@ -77,6 +79,19 @@ impl SMethod {
             ..self
         }
     }
+
+    /// Specializes this instance by creating a new [`SMethod`] instance where signature
+    /// is specialized with respect to the given object and args types.
+    pub fn specialize_for(
+        self,
+        obj_tpe: SType,
+        args: Vec<SType>,
+    ) -> Result<SMethod, TypeUnificationError> {
+        let mut items2 = vec![obj_tpe];
+        let mut args = args;
+        items2.append(args.as_mut());
+        unify_many(self.tpe().t_dom.clone(), items2).map(|subst| self.with_concrete_types(&subst))
+    }
 }
 
 #[derive(PartialEq, Eq, Debug, Clone)]
diff --git a/ergotree-ir/src/types/stuple.rs b/ergotree-ir/src/types/stuple.rs
index 4b9f84e3a..53feb5a2f 100644
--- a/ergotree-ir/src/types/stuple.rs
+++ b/ergotree-ir/src/types/stuple.rs
@@ -1,3 +1,4 @@
+use std::collections::HashMap;
 use std::convert::TryFrom;
 use std::convert::TryInto;
 use std::slice::Iter;
@@ -5,6 +6,7 @@ use std::slice::Iter;
 use crate::mir::select_field::TupleFieldIndex;
 
 use super::stype::SType;
+use super::stype_param::STypeVar;
 
 /// Tuple items with bounds check (2..=255)
 #[derive(PartialEq, Eq, Debug, Clone)]
@@ -39,6 +41,12 @@ impl<T> TupleItems<T> {
     }
 }
 
+impl<T> From<TupleItems<T>> for Vec<T> {
+    fn from(t: TupleItems<T>) -> Self {
+        t.0
+    }
+}
+
 /// Out of bounds items quantity error
 #[derive(PartialEq, Eq, Debug, Clone)]
 pub struct STupleItemsOutOfBoundsError();
@@ -79,6 +87,18 @@ impl STuple {
             items: vec![t1, t2].try_into().unwrap(),
         }
     }
+
+    pub(crate) fn with_subst(self, subst: &HashMap<STypeVar, SType>) -> Self {
+        STuple {
+            items: self
+                .items
+                .iter()
+                .map(|a| a.clone().with_subst(subst))
+                .collect::<Vec<SType>>()
+                .try_into()
+                .unwrap(),
+        }
+    }
 }
 
 // pub struct STupleCompanion();
diff --git a/ergotree-ir/src/types/stype.rs b/ergotree-ir/src/types/stype.rs
index e7acc68cb..a64df73ca 100644
--- a/ergotree-ir/src/types/stype.rs
+++ b/ergotree-ir/src/types/stype.rs
@@ -95,12 +95,31 @@ impl SType {
         )
     }
 
+    /// Check if type is primitive
+    pub fn is_prim(&self) -> bool {
+        matches!(
+            self,
+            SType::SByte
+                | SType::SShort
+                | SType::SInt
+                | SType::SLong
+                | SType::SBigInt
+                | SType::SAny
+                | SType::SGroupElement
+                | SType::SSigmaProp
+                | SType::SBox
+                | SType::SAvlTree
+                | SType::SContext
+                | SType::SBoolean
+        )
+    }
+
     pub(crate) fn with_subst(self, subst: &HashMap<STypeVar, SType>) -> Self {
         match self {
             SType::STypeVar(ref tpe_var) => subst.get(&tpe_var).cloned().unwrap_or(self),
             SType::SOption(tpe) => SType::SOption(tpe.with_subst(subst).into()),
             SType::SColl(tpe) => SType::SColl(tpe.with_subst(subst).into()),
-            SType::STuple(_) => todo!("type substitution in STuple is not yet implemented"),
+            SType::STuple(stup) => SType::STuple(stup.with_subst(subst)),
             SType::SFunc(sfunc) => SType::SFunc(sfunc.with_subst(subst)),
             _ => self,
         }
@@ -113,6 +132,18 @@ impl From<STuple> for SType {
     }
 }
 
+impl From<STypeVar> for SType {
+    fn from(v: STypeVar) -> Self {
+        SType::STypeVar(v)
+    }
+}
+
+impl From<SFunc> for SType {
+    fn from(v: SFunc) -> Self {
+        SType::SFunc(v)
+    }
+}
+
 /// Conversion to SType
 pub trait LiftIntoSType {
     /// get SType
@@ -213,11 +244,11 @@ impl LiftIntoSType for Tuple {
 
 #[cfg(test)]
 #[cfg(feature = "arbitrary")]
-mod tests {
+pub(crate) mod tests {
     use super::*;
     use proptest::prelude::*;
 
-    fn primitive_type() -> BoxedStrategy<SType> {
+    pub(crate) fn primitive_type() -> BoxedStrategy<SType> {
         prop_oneof![
             Just(SType::SAny),
             Just(SType::SBoolean),
@@ -231,7 +262,6 @@ mod tests {
             Just(SType::SBox),
             Just(SType::SAvlTree),
             Just(SType::SContext),
-            Just(SType::STypeVar(STypeVar::t())),
         ]
         .boxed()
     }
@@ -241,7 +271,7 @@ mod tests {
         type Strategy = BoxedStrategy<Self>;
 
         fn arbitrary_with(_args: Self::Parameters) -> Self::Strategy {
-            primitive_type()
+            prop_oneof![primitive_type(), Just(SType::STypeVar(STypeVar::t())),]
                 .prop_recursive(
                     4,  // no more than this branches deep
                     64, // total elements target
diff --git a/ergotree-ir/src/types/type_unify.rs b/ergotree-ir/src/types/type_unify.rs
new file mode 100644
index 000000000..61b1f41e1
--- /dev/null
+++ b/ergotree-ir/src/types/type_unify.rs
@@ -0,0 +1,330 @@
+use std::collections::HashMap;
+
+use super::stype::SType;
+use super::stype_param::STypeVar;
+use SType::*;
+
+#[allow(clippy::unnecessary_wraps)]
+fn unified_without_subst() -> Result<HashMap<STypeVar, SType>, TypeUnificationError> {
+    Ok(HashMap::new())
+}
+
+/// Performs pairwise type unification making sure each type variable is equally
+/// substituted in all items.
+pub fn unify_many(
+    items1: Vec<SType>,
+    items2: Vec<SType>,
+) -> Result<HashMap<STypeVar, SType>, TypeUnificationError> {
+    if items1.len() != items2.len() {
+        return Err(TypeUnificationError(format!(
+            "items lists are different sizes {:?} vs. {:?}",
+            items1, items2
+        )));
+    }
+    let list_of_substitutions: Result<Vec<HashMap<STypeVar, SType>>, _> = items1
+        .iter()
+        .zip(items2)
+        .map(|(t1, t2)| unify_one(t1, &t2))
+        .collect();
+    let mut res = HashMap::new();
+    for substitutions in list_of_substitutions? {
+        for (type_var, tpe) in substitutions.iter() {
+            match res.insert(type_var.clone(), tpe.clone()) {
+                Some(previous_val) if previous_val != *tpe => {
+                    return Err(TypeUnificationError(format!(
+                        "cannot merge new substitution {:?} for {:?} already exist substitution {:?}",
+                        tpe, type_var, previous_val
+                    )))
+                }
+                _ => (),
+            };
+        }
+    }
+    Ok(res)
+}
+
+/// Error on type unification
+#[derive(PartialEq, Eq, Debug, Clone)]
+pub struct TypeUnificationError(pub String);
+
+/// Finds a substitution `subst` of type variables
+/// such that unify_types(t1.with_subst(subst), t2) == Ok(emptySubst)
+pub fn unify_one(t1: &SType, t2: &SType) -> Result<HashMap<STypeVar, SType>, TypeUnificationError> {
+    match (t1, t2) {
+        (STypeVar(tv1), STypeVar(tv2)) if tv1 == tv2 => unified_without_subst(),
+        (STypeVar(id1), t2) if !matches!(t2, STypeVar(_)) => {
+            Ok([(id1.clone(), t2.clone())].iter().cloned().collect())
+        }
+        (t1, t2) if t1.is_prim() && t2.is_prim() && t1 == t2 => unified_without_subst(),
+        (SColl(elem_type1), SColl(elem_type2)) => unify_one(elem_type1, elem_type2),
+        (SColl(elem_type1), STuple(_)) => unify_one(elem_type1, &SAny),
+        (STuple(tuple1), STuple(tuple2)) if tuple1.items.len() == tuple2.items.len() => {
+            unify_many(tuple1.items.clone().into(), tuple2.items.clone().into())
+        }
+        (SOption(elem_type1), SOption(elem_type2)) => unify_one(elem_type1, elem_type2),
+        (SFunc(sfunc1), SFunc(sfunc2)) => {
+            unify_many(sfunc1.t_dom_plus_range(), sfunc2.t_dom_plus_range())
+        }
+        (SAny, _) => unified_without_subst(),
+        // it is necessary for implicit conversion in Coll(bool, prop, bool)
+        (SBoolean, SSigmaProp) => unified_without_subst(),
+        (t1, t2) => Err(TypeUnificationError(format!(
+            "Cannot unify {:?} and {:?}",
+            t1, t2
+        ))),
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::super::stype::tests::primitive_type;
+    use super::*;
+    use crate::types::sfunc::SFunc;
+    use crate::types::stuple::STuple;
+    use proptest::prelude::*;
+
+    proptest! {
+
+        #[test]
+        fn prim_types(t in primitive_type()) {
+            prop_assert_eq!(unify_one(&t, &t), unified_without_subst());
+            prop_assert_eq!(unify_one(&SAny, &t), unified_without_subst());
+            prop_assert_eq!(unify_one(&SAny, &SColl(t.clone().into())), unified_without_subst());
+            prop_assert_eq!(unify_one(&SColl(SAny.into()), &SColl(t.clone().into())), unified_without_subst());
+            prop_assert_eq!(unify_one(
+                &SColl(SAny.into()),
+                &STuple(STuple::pair(t.clone(), t.clone()))), unified_without_subst()
+            );
+            prop_assert_eq!(unify_one(
+                &SColl(SAny.into()),
+                &STuple(STuple::pair(t.clone(), STuple(STuple::pair(t.clone(), t))))), unified_without_subst()
+            );
+        }
+
+    }
+
+    fn check_error(t1: SType, t2: SType) {
+        assert!(
+            unify_one(&t1, &t2).is_err(),
+            "unification of {:?} and {:?} should fail",
+            t1,
+            t2
+        );
+    }
+
+    fn check_subst_map(t1: SType, t2: SType, expect: HashMap<STypeVar, SType>) {
+        assert_eq!(unify_one(&t1, &t2).unwrap(), expect);
+        assert_eq!(
+            unify_one(&t1.with_subst(&expect), &t2),
+            unified_without_subst()
+        )
+    }
+
+    fn check_empty_subst(t1: SType, t2: SType) {
+        assert_eq!(
+            unify_one(&t1, &t2).unwrap(),
+            unified_without_subst().unwrap()
+        );
+    }
+
+    fn check_subst(t1: SType, t2: SType, subst: (STypeVar, SType)) {
+        check_subst_map(t1, t2, [subst].iter().cloned().collect())
+    }
+
+    fn check_subst_many(t1: SType, t2: SType, subst: &[(STypeVar, SType)]) {
+        check_subst_map(t1, t2, subst.iter().cloned().collect())
+    }
+
+    #[test]
+    fn unify_empty_subst() {
+        check_empty_subst(SInt, SInt);
+        check_empty_subst(
+            STuple::pair(SInt, SInt).into(),
+            STuple::pair(SInt, SInt).into(),
+        );
+
+        // tuple as array
+        check_empty_subst(SColl(SAny.into()), STuple::pair(SInt, SInt).into());
+
+        check_empty_subst(
+            SColl(SColl(SInt.into()).into()),
+            SColl(SColl(SInt.into()).into()),
+        );
+
+        check_empty_subst(SOption(SInt.into()), SOption(SInt.into()));
+
+        check_empty_subst(
+            SFunc::new(vec![SBox], SLong).into(),
+            SFunc::new(vec![SBox], SLong).into(),
+        );
+
+        check_empty_subst(STypeVar::t().into(), STypeVar::t().into());
+        check_empty_subst(
+            STuple::pair(SBoolean, STypeVar::t().into()).into(),
+            STuple::pair(SBoolean, STypeVar::t().into()).into(),
+        );
+
+        check_empty_subst(
+            SFunc::new(vec![SBoolean], SInt).into(),
+            SFunc::new(vec![SBoolean], SInt).into(),
+        );
+
+        check_empty_subst(SBoolean, SSigmaProp);
+    }
+
+    #[test]
+    fn unify_with_subst() {
+        check_subst(STypeVar::t().into(), SInt, (STypeVar::t(), SInt));
+
+        // Coll
+        check_subst(
+            STypeVar::t().into(),
+            SColl(SInt.into()),
+            (STypeVar::t(), SColl(SInt.into())),
+        );
+        check_subst(
+            SColl(Box::new(STypeVar::t().into())),
+            SColl(SInt.into()),
+            (STypeVar::t(), SInt),
+        );
+        check_subst(
+            SColl(Box::new(STypeVar::t().into())),
+            SColl(Box::new(STuple::pair(SInt, SBoolean).into())),
+            (STypeVar::t(), STuple::pair(SInt, SBoolean).into()),
+        );
+        check_subst(
+            SColl(Box::new(
+                STuple::pair(STypeVar::t().into(), SBoolean).into(),
+            )),
+            SColl(Box::new(STuple::pair(SInt, SBoolean).into())),
+            (STypeVar::t(), SInt),
+        );
+
+        // Option
+        check_subst(
+            STypeVar::t().into(),
+            SOption(SInt.into()),
+            (STypeVar::t(), SOption(SInt.into())),
+        );
+        check_subst(
+            SOption(Box::new(STypeVar::t().into())),
+            SOption(SInt.into()),
+            (STypeVar::t(), SInt),
+        );
+        check_subst(
+            SOption(Box::new(STypeVar::t().into())),
+            SOption(Box::new(STuple::pair(SInt, SBoolean).into())),
+            (STypeVar::t(), STuple::pair(SInt, SBoolean).into()),
+        );
+        check_subst(
+            SOption(Box::new(
+                STuple::pair(STypeVar::t().into(), SBoolean).into(),
+            )),
+            SOption(Box::new(STuple::pair(SInt, SBoolean).into())),
+            (STypeVar::t(), SInt),
+        );
+
+        // SFunc
+        check_subst(
+            SFunc::new(vec![STypeVar::t().into()], SInt).into(),
+            SFunc::new(vec![SBoolean], SInt).into(),
+            (STypeVar::t(), SBoolean),
+        );
+        check_subst(
+            SFunc::new(vec![SInt], STypeVar::t().into()).into(),
+            SFunc::new(vec![SInt], SBoolean).into(),
+            (STypeVar::t(), SBoolean),
+        );
+        check_subst_many(
+            SFunc::new(
+                vec![STuple::pair(SInt, STypeVar::iv().into()).into()],
+                STypeVar::t().into(),
+            )
+            .into(),
+            SFunc::new(vec![STuple::pair(SInt, SBoolean).into()], SBox).into(),
+            &[(STypeVar::t(), SBox), (STypeVar::iv(), SBoolean)],
+        );
+        check_subst(
+            SFunc::new(
+                vec![STuple::pair(SInt, STypeVar::t().into()).into()],
+                STypeVar::t().into(),
+            )
+            .into(),
+            SFunc::new(vec![STuple::pair(SInt, SBox).into()], SBox).into(),
+            (STypeVar::t(), SBox),
+        );
+        check_subst_many(
+            SFunc::new(
+                vec![
+                    SColl(STypeVar(STypeVar::iv()).into()),
+                    SFunc::new(vec![STypeVar::iv().into()], STypeVar::ov().into()).into(),
+                ],
+                SColl(STypeVar(STypeVar::ov()).into()),
+            )
+            .into(),
+            SFunc::new(
+                vec![SColl(SBox.into()), SFunc::new(vec![SBox], SLong).into()],
+                SColl(SLong.into()),
+            )
+            .into(),
+            &[(STypeVar::iv(), SBox), (STypeVar::ov(), SLong)],
+        )
+    }
+
+    #[test]
+    fn unify_negative() {
+        check_error(SInt, SLong);
+
+        // Tuple
+        check_error(SInt, STuple::pair(SInt, SBoolean).into());
+        check_error(
+            STuple::pair(SBoolean, SInt).into(),
+            STuple::pair(SBoolean, SBoolean).into(),
+        );
+        check_error(STuple::pair(SInt, STypeVar::t().into()).into(), SInt);
+        check_error(
+            STuple::pair(STypeVar::t().into(), SInt).into(),
+            STuple::pair(SBoolean, STypeVar::iv().into()).into(),
+        );
+
+        // Coll
+        check_error(SColl(SColl(SInt.into()).into()), SColl(SInt.into()));
+        check_error(
+            SColl(Box::new(STypeVar::t().into())),
+            SColl(Box::new(STypeVar::iv().into())),
+        );
+
+        // Option
+        check_error(SOption(SBoolean.into()), SOption(SInt.into()));
+        check_error(SOption(SBoolean.into()), SColl(SInt.into()));
+
+        // SFunc
+        check_error(
+            SFunc::new(vec![SBox], SLong).into(),
+            SFunc::new(vec![SBox], SInt).into(),
+        );
+        check_error(
+            SFunc::new(vec![STypeVar::t().into()], SInt).into(),
+            SFunc::new(vec![SInt], SBoolean).into(),
+        );
+        check_error(
+            SFunc::new(vec![SInt], STypeVar::t().into()).into(),
+            SFunc::new(vec![SBoolean], SInt).into(),
+        );
+        check_error(
+            SFunc::new(
+                vec![STuple::pair(SInt, STypeVar::t().into()).into()],
+                STypeVar::t().into(),
+            )
+            .into(),
+            SFunc::new(vec![STuple::pair(SInt, SBoolean).into()], SBox).into(),
+        );
+
+        check_error(SSigmaProp, SBoolean);
+    }
+
+    #[test]
+    fn unify_diff_size() {
+        assert!(unify_many(vec![SInt, SLong], vec![SLong]).is_err());
+    }
+}


Test patch: