Example circuits to implement in Alucard

[cwgoes]

• Simple Merkle tree proof verification
  • Can be implemented with a list initially
• Tendermint light client
  • ed25519 verification (which will suck performance-wise, we should figure out how much it sucks)
  • bls12-381 verification
  • implement light client verification algorithm, also see this function
  • we should start with a simple model, such as verifying a threshold multisignature over headers
    • circuit takes as public input a start set of keys and weights and an end set of keys and weights and some hashes (state DB Merkle roots) associated with heights
    • circuit takes as private input a list of headers and signatures
    • headers must be verified sequentially
    • each header can update the keys and weights and has a hash (state DB root) associated with the particular height
    • circuit should check
      • that all of the header transitions are valid, i.e. for each i from start to end,
      • the signatures for h_i on the signer set for h_i+1 are valid, if it changed
      • the signatures for h_i on the hash are valid
      • and that if the height is in the list of heights we want to verify the state DB root for, the root matches

rough initial sense:

type Multisig = [(PublicKey, Int)]
type Threshold = Int
type Height = Int
type Hash = Bytes32
type Header {
  multisig: Multisig
  height : Int
  dbStateRootHash: bytes32
}

valid : 
  // public
  Threshold -> 
  Multisig ->
  Header ->
  [(Height, Hash)] ->
  // private
  [(Header, [Signature])] ->
  boolean
valid threshold startingMultisig startingHeader rootsToValidate headers = 
  foldl (validateHeaderTransition rootsToValidate) startingHeader headers
  where validateHeaderTransition rootsToValidate header1 (header2, sigs) = 
                 validThresholdSig (multisig header1) (hash header2) sigs &&
                 (if (height header2) in rootsToValidate then (lookup rootsToValidate height == dbStateRootHash header2) else True)
             validThresholdSig multisig sigs = sum (filterMap ecverify (zip multisig sigs)) > threshold

if x then y else z`

(x && y || z)

if x then y else z : Int

(= 2 (if x then y else z : Int)) --> ((x && y = 2) || z == 2)

• Validity predicates for Taiga
  • check here for an idea of the inputs
  • For assets
    • Allow mint or burn under specific conditions
  • For users
    • Spending conditions (different keys for different amounts), intent conditions (private bartering)
      • e.g. key X for up to amount Y of asset Z, key X1 for up to amount Y1, etc.
      • e.g. allow spend of this note with amount X of asset Y iff. a note is minted to me with amount X1 of asset Y1