Technical Report 2021/08/31

MELD

We build MELD on top of the Cardano blockchain, so improving the platform is one of our priorities. This technical report gives some insights into our contribution to the Cardano ecosystem and the progress of our internal projects.

Plutus

Documentation

We have been spending a good amount of effort to help update Plutus documentation, which is usually outdated due to lightning development progress. One can never get enough good documentation. The whole community needs this!

We continued to work on some documentation:

This includes restructuring the new section 5 – Goguen: Cardano Ledger for Smart Contracts in the EUTXO specs, porting more content from the Alonzo changes doc, and prepare more original content. We’ve got the Phase-2 scripts section down, ready to get more into the concept of language and new protocol parameters next. We’ve also decided to write more on context preparation and script validation in general.

The redeemerHash-not-in-InputInfo story has also inspired a new issue on Github. It’s about the ability to read other inputs’ redeemer from an input’s validator script through the script context. We used to be able to do that earlier this year but couldn’t anymore after the new Alonzo changes. We did have a few workarounds like adding extra fields to Datums, or supportive output types, etc. But after reaching a certain level of complexity, we finally want to press this to simplify contract designs for various situations, especially for third-party contract integrations where we don’t have control over any data type or validation rule. Working solely with Datum without Redeemer usually leads to more complexity and corner cases to reason about. Checking for a specific Redeemer, on the other hand, eliminates many logics in other redeemer types. If this gets approved, we suspect a minimal change is required, as txInfo already has a tx with redeemers in its witnesses. Hopefully, the removal wasn’t due to security risks, or a critical saving in memory usage.

More references:

Ledger Specs

During our dependency pumping and breaking changes fixing routine, we found an interesting one from Cardano Base that propagates to many components. The main idea is to use a fixed number of packed bytes to represent hashes instead of using a size-agnostic representation like ShortByteString hence ByteArray. This should reduce some overhead for better performance!

We spent a few hours trying to propagate this work to Ledger Specs and study the code base along the way.

Summary:

  • Hash has extended the fixed ShortByteString representation to a type HashRep h :: Type in HashAlgorithm.
  • This leads to the need to add many HashAlgorithm constraints to related functions and instances.
  • Also requires removing the UNPACK pragmas on Hash.
  • Also requires more Cardano.Ledger.Crypto.Crypto constraints.
  • Also leads to Cardano.Ledger.Crypto.HASH crypto ~ Blake2b_256 at some places related to the “rigid” type Nonce.

We stopped after cardano-ledger-core & shelley-spec-ledger to scout for more and was informed that a less invasive solution was being worked on! We don’t regret any effort, though, as this run helped us get a lot more familiar with the code base of both Cardano Base and Ledger Specs. Especially when we’re planning to analyze the low-level work in Cardano Base for the Bounty program and doing deeper ledger work in general.

If the HashAlgorithm route ends up staying, we’re happy to complete this task for all relevant repositories for the IOHK team to focus on the more awesome stuff!

Haskell ecosystem

GHC

Errors as (structured) values

This is an instrumental body of work. We want to join hands because there are newcomer-friendly tasks for us to get familiar with GHC work. We can then help integrate this new diagnostic infrastructure to HLS, and hopefully HLint & Hachi Lint too!

Our first GHC MR that converts diagnostics in GHC.Tc.Validity to proper TcRnMessage:

As the MR had gotten quite big already, we’ve focused on refining it to a mergeable state to continue the remaining cases in upcoming MRs.

Summary:

  • TcRnBadAssociatedType: replace type synonyms with inline comments. The key is to avoid pre-mature type synonyms.
  • Add examples to:
    • TcRnTupleConstraintInst, also add a Class for more information!
    • TcRnAbstractClassInst, also promote Name to Class for more information.
    • TcRnNoClassInstHead, also use the more specific pprType function for presentation.
    • TcRnConstraintInKind.
    • TcRnUnboxedTupleTypeFuncArg.
    • TcRnLinearFuncInKind.
    • TcRnForAllEscapeError.
    • TcRnVDQInTermType.
    • TcRnIllegalEqualConstraints.
    • TcRnBadQuantPredHead, also add a missing test case for T16474!
    • TcRnIllegalTupleConstraint.
    • TcRnNoneTypeVarArgInConstraint.
    • TcRnIllegalImplicitParam.
    • TcRnIllegalConstraintSynonymOfKind.
    • TcRnIllegalClassInst.
    • TcRnOversaturatedVisibleKindArg.
    • TcRnBadAssociatedType, also add a missing test case for T12387a. This one is rather intresting since the error message only happens in Template Haskell. It also requires updating the original snippet to the new Template Haskell API, which seems to come from a fellow Vietnamese engineer!
  • Remove TcRnIllegalPredConstraint and its outdated validity check.
  • Remove TcRnDuplicateConstraints and its original check, which redundant-constraints has subsumed.
  • List test cases in TcRnMessage in a more consistent style.
  • Rename GHC.Tc.Types.Validity to GHC.Tc.Types.Rank.
  • Other typo fixes, formatting, comments, renames here and there.

More references:

HLint

We continue to study and contribute to HLint, which is critical to the development of Hachi Lint, and valuable to the whole ecosystem in general.

We continued to refine existing PRs and got the first one merged!

The college students we’ve been training are now investigating the following issues:

Hopefully, they’ll get up to speed soon to deliver faster! Then they can graduate to Hachi Lint, HLS, Cabal, GHC, and Cardano work while helping newcomers get into Haskell and HLint.

We’re working with our past teachers and the best universities in Vietnam to filter the best crops to train!

Hachi

MELD Announces Hachi!

Hachi is our effort to develop a suite of security analysis tools for Plutus smart contracts. This project will be open-sourced to the public eventually. For now, we focus on research and experiments on Cardano to better understand how to have the best approach for each problem.

Here is a quick summary of what we have done lately:

  • Continue smart contract security research in general.
  • Continue to study Cardano architectures, Plutus interpreters, etc.
  • Refine and write more proposals & documentation in general. Go to greater lengths to plan the ambitious future of Hachi!
  • Write and review more contracts with vulnerabilities on Cardano.
  • Continue to work on the initial cases for Hachi Lint. We expect to release the first minimal alpha this September.
  • More static analysis work on Plutus, like transforming Plutus Core AST to XML tree to query with XPath.
  • Start working on instrumentation for Plutus Core!
  • Start detecting common constructs in Plutus Core like Church-encoded Bool and Z combinators.
  • Continue to port Plutus grammar & built-in functions for symbolic execution.
  • Continue work on Plutus Core fuzzers.
  • Start planning work for the Cardano Bounty program. We’ve been attracting more gunpowder for this critical program.

Even though most work is still highly experimental, we hope to start demoing things soon. For now, here is a quick look at our transpiling/interpreting flow:

  • (Optional) Write the validator script in Haskell:
type MyValidatorType = Integer -> Integer -> Integer -> Bool

example :: MyValidatorType
example x _ _ = if x > 0 then x + 1337 == 0xDEADBEEF else 4027431613 * x == 0xF00DBABE - x * x
  • (Optional) Compile it down to Plutus Core:
exampleCode :: PlutusTx.CompiledCode MyValidatorType
exampleCode = $$(PlutusTx.compile [||example||])

writeFile "example.plc" (pretty (PlutusTx.getPlc exampleCode))
  • Transpile Plutus Core to Racket:
cat example.plc | hc

With hc being our transpiler.

  • Embed the transpiled Racket code to a Racket template for analysis!
...
(define main
  "transpiled code goes here"
  )
(define (m datum redeemer context)
  ((force (((main datum) redeemer) context)) 0))

(define-symbolic x integer?)

;; This function solves for x (angelic execution)
(solve
 (begin
   (assume (not (= x 3735927222)))
   (assert (= 0 (m x 1 1)))
   ))

While this example simply solves (finds) an integer Datum that bypasses the validator script, it demonstrates a working Racket transpiler and custom interpreter. We hope to show the interpreter with some instrumentation and fuzzing soon. The tools’ UX should get better with time too.

We’re also formalizing a lot of our internal documentation for publishing. Hachi and its major projects will have their own papers. Please stay tuned for more!

ADAmatic

MELD and VENT Present ADAmatic!

We continue to focus on the specifications of the bridge, as well as onboarding more partners to both build with us and run the ADAmatic nodes to decentralize power. Cross-chain contract integration is still being studied (especially the RenVM study case), but the initial focus is still on the wrapping/MELDing assets functionality.

This includes an vital V2 [Ka 架] that marks decentralization.

ADAmatic v2

We need to balance speed and complexity so we won’t go full sharding & shuffling community nodes at launch. A saner choice is diverse node operators with different backgrounds cross-signing and checking each other. Limiting the scope early on also helps reduce diverse use cases and security risks that come with them. We can’t wait to announce the credible partners that are joining. Please stay tuned for more!

MELD

MELD.com

Smart Contracts

  • Continue to study Ledger and Plutus documentation and codebase.
  • Continue to study more DeFi projects.
  • More standards for DApp development.
  • Continue hardcore specifications and documentation work. Especially on Smart Contract design.
  • Write many more test cases to complete the first test suite for mFiat.
  • Continue work to improve the liquidation system.
  • Continue work to delegate collateralized ADA.
  • Go for a brand new lending design that simplifies validation rules and improves liquidity and accountability.
  • Continue to optimize minting policies for different “currencies”.
  • Continue to track open Cardano issues that might affect contract design going forward.

For different reasons (mainly competition), we’re still refraining from showing too much core work at the moment. That said, we’re also formalizing internal documentation to publish a White Paper for each core component. We do hope to publish mFiat’s this September. Please stay tuned!

For now, here is a low-key diagram of the closing CDP process! mFiat v0 Close

Tokenomics & Economics

  • Continue to study more DeFi projects.
  • More economics and tokenomics model research, especially on AMMs and their dynamic curves.
  • Collect more data to analyze.
  • More in-depth market research.
  • Forecast protocol usage and traffic to estimate treasury release schedule, protocol fees, insurance solvency, staking APY, and more.
  • Complete a new token circulating supply forecast.
  • Complete a new DEX market forecast and revenue forecast with different scenarios.
  • Complete a new token evaluation model.

Our biggest problem at the moment is the lack of data to analyze. Especially on Cardano, where on-chain contract fees and liquidity/trading volumes haven’t been captured. The focus now is to complete the economics model frame, build a solid simulator then hardcore data collection and analysis. Then just keep iterating to improve the model. This front should gradually get better come the Alonzo testnet and mainnet. Can’t wait!

We’re also speeding up recruitment for more awesome Quants. We’ll have separate economics reports and articles when things get stable enough, and hopefully many economics Yellow Papers too!

MELDApp

We’ve been making good progress with the MELDApp in general. The plan is to do beta testing this September and release the first production version next quarter. We’re going to start demoing comes September too. The current demo pipeline includes minting mFiat like mUSD and mEUR, then lending and borrowing them, then the liquidation system. Many more will come with time to. Stay tuned!