Skip to content

Instantly share code, notes, and snippets.

@gluk64

gluk64/chainweaver-share.pact

Created November 8, 2019 11:12
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save gluk64/f9726d3d4e0380e14844b7931bf7197b to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save gluk64/f9726d3d4e0380e14844b7931bf7197b to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. gluk64 created this gist Nov 8, 2019.
    48 changes: 48 additions & 0 deletions chainweaver-share.pact
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,48 @@
    ;;
    ;; "Hello, world!" smart contract/module
    ;;
    ;; To try it out, click "Load into REPL" and type into the repl:
    ;; (hello-world.set-message "universe")
    ;; (hello-world.greet)
    ;;
    ;; Check lines 21 and 34 to play with Formal Verification
    ;;

    ;; Define the module.
    (module hello-world MODULE_ADMIN
    "A smart contract to greet the world."

    ; no-op module admin for example purposes.
    ; in a real contract this could enforce a keyset, or
    ; tally votes, etc.
    (defcap MODULE_ADMIN () true)

    (defschema message-schema
    @doc "Message schema"
    @model [(invariant (!= msg ""))]

    msg:string)

    (deftable
    message:{message-schema})

    (defun set-message
    (
    m:string
    )
    "Set the message that will be used next"
    ; uncomment the following to make the model happy!
    ; (enforce (!= m "") "set-message: must not be empty")
    (write message "0" {"msg": m})
    )

    (defun greet ()
    "Do the hello-world dance"
    (with-default-read message "0" { "msg": "" } { "msg":= msg }
    (format "Hello {}!" [msg])))
    )

    (create-table message)

    (set-message "world")
    (greet)