Skip to main content
  • Home
  • Development
  • Documentation
  • Donate
  • Operational login
  • Browse the archive

swh logo
SoftwareHeritage
Software
Heritage
Archive
Features
  • Search

  • Downloads

  • Save code now

  • Add forge now

  • Help

https://gitlab.com/nomadic-labs/mi-cho-coq
08 June 2021, 12:34:34 UTC
  • Code
  • Branches (270)
  • Releases (1)
  • Visits
Revision d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC, committed by kristinas on 11 May 2021, 09:41:59 UTC
Added README
1 parent f70493e
  • Files
  • Changes
    • Branches
    • Releases
    • HEAD
    • refs/heads/51-verify-dexter-2-dexter-fa1-2lqt-dexter-1-5
    • refs/heads/Julien@adding_contracts
    • refs/heads/arvid@ci-build-refactor-cache
    • refs/heads/arvid@ci-rethinking
    • refs/heads/arvid@cpmm-verification
    • refs/heads/arvid@cpmm2-verification
    • refs/heads/arvid@dexter-lemmas-and-refactorings
    • refs/heads/arvid@dexter-verification-parsing-test
    • refs/heads/arvid@dexter-verification-stringfix
    • refs/heads/arvid@dexter-verification-updates-20200928-coq8.08
    • refs/heads/arvid@dexter_fa12lqt-verification__addLiquidity
    • refs/heads/arvid@dexter_fa12lqt-verification__removeLiquidity
    • refs/heads/arvid@fragment_typer_and_ott_typing
    • refs/heads/arvid@guillaume-claret@dexter_fa12lqt-verification
    • refs/heads/arvid@guillaume-claret@dexter_fa12lqt-verification-bis
    • refs/heads/arvid@opaque-tez-experiments
    • refs/heads/arvid@rafoo@simplify-eval_precond-rebased
    • refs/heads/arvid@re-organize-contracts_coq
    • refs/heads/backport-opam-package-changes-from-upstream
    • refs/heads/bb@dexter-verification
    • refs/heads/chain-modelisation-guestbook
    • refs/heads/colin-dexter_fa12lqt-verification
    • refs/heads/contract_spend
    • refs/heads/dev
    • refs/heads/dexter-dfs-compat
    • refs/heads/dexter-fa2-verification-hackish
    • refs/heads/dexter-verification
    • refs/heads/dexter-verification-approve
    • refs/heads/dexter-verification-cleanup-lemmas
    • refs/heads/dexter-verification-rebase
    • refs/heads/dexter_fa12lqt-verification
    • refs/heads/entrypoints
    • refs/heads/guillaume-claret-add-entrypoint-to-self
    • refs/heads/guillaume-claret-full-eval-function
    • refs/heads/guillaume-claret-gadts-without-annotations
    • refs/heads/guillaume-claret-integrate-coq-of-ocaml-output
    • refs/heads/guillaume-claret-semantics-injection
    • refs/heads/guillaume-claret@dexter_fa12lqt-verification
    • refs/heads/guillaume-claret@dexter_fa12lqt-verification-benchmark-token-to-token
    • refs/heads/guillaume-claret@dexter_fa12lqt-verification-experiments
    • refs/heads/guillaume-claret@dexter_fa12lqt-verification-string-eqb
    • refs/heads/improve_multisig
    • refs/heads/internship_report
    • refs/heads/intership_presentation
    • refs/heads/julien@entrypoint_notations
    • refs/heads/julien@gasoline_inconsistent_universe
    • refs/heads/julien@mutually_calling_contracts
    • refs/heads/kristina-fa12-verification-rebase
    • refs/heads/kristina@fa12-verification-rebase
    • refs/heads/kristina@fa2
    • refs/heads/manager-contract-do-entry
    • refs/heads/master
    • refs/heads/merge-contract
    • refs/heads/merge-contract_multithreaded_simpl
    • refs/heads/merge_with_shared_storage
    • refs/heads/michelson_fragment
    • refs/heads/miguelito
    • refs/heads/old_merge_with_shared_storage
    • refs/heads/old_merge_with_shared_storage_WIP
    • refs/heads/old_merge_with_shared_storage_use
    • refs/heads/old_resiliable_contract_
    • refs/heads/proto-proposal
    • refs/heads/rafoo@concert_integration
    • refs/heads/rafoo@dexter_fa12lqt-verification
    • refs/heads/rafoo@dexter_perf_experiment
    • refs/heads/rafoo@map_extra_lemmas
    • refs/heads/rafoo@mutez_opacity
    • refs/heads/rafoo@primitives
    • refs/heads/rafoo@semantics-projections
    • refs/heads/rafoo@slides_inria_day
    • refs/heads/rafoo@talk_nl_seminar
    • refs/heads/rafoo@tpbc
    • refs/heads/rafoo@transparent_set_remove
    • refs/heads/rafoo@tzt
    • refs/heads/raphael@precond_iter
    • refs/heads/raphael@tuto
    • refs/heads/return2sender
    • refs/heads/self_in_origination
    • refs/heads/specialised-multisig
    • refs/heads/stateful
    • refs/heads/yrg@cpmm2-economic-properties
    • refs/heads/yrg@cpmm2-new-version
    • refs/heads/yrg@dexter_fa12lqt-verification-XtzToToken
    • refs/heads/yrg@dexter_fa12lqt-verification-set-manager
    • refs/heads/yrg@dexter_fa12lqt-verification-tokenToXtz
    • refs/heads/yrg@dexter_fa12lqt-verification-update-spec
    • refs/heads/yrg@make-mutez-more-readable
    • refs/heads/yrg@optimize-micheline-lexer
    • refs/heads/yrg@optimize-micheline-lexical-analysis
    • refs/heads/yrg@refactor-make-mutez-more-readable
    • refs/heads/yrg@verify-vesting
    • refs/heads/yrg@wip-cpmm2-economic-properties
    • refs/heads/zhenlei@cancellable_contract
    • refs/heads/zhenlei@internship_report
    • refs/heads/zhenlei@merge_shared_tree
    • refs/merge-requests/1/head
    • refs/merge-requests/100/head
    • refs/merge-requests/100/merge
    • refs/merge-requests/101/head
    • refs/merge-requests/102/head
    • refs/merge-requests/102/merge
    • refs/merge-requests/103/head
    • refs/merge-requests/103/merge
    • refs/merge-requests/104/head
    • refs/merge-requests/104/merge
    • refs/merge-requests/105/head
    • refs/merge-requests/105/merge
    • refs/merge-requests/106/head
    • refs/merge-requests/106/merge
    • refs/merge-requests/107/head
    • refs/merge-requests/107/merge
    • refs/merge-requests/108/head
    • refs/merge-requests/108/merge
    • refs/merge-requests/109/head
    • refs/merge-requests/109/merge
    • refs/merge-requests/11/head
    • refs/merge-requests/11/merge
    • refs/merge-requests/110/head
    • refs/merge-requests/110/merge
    • refs/merge-requests/111/head
    • refs/merge-requests/111/merge
    • refs/merge-requests/112/head
    • refs/merge-requests/112/merge
    • refs/merge-requests/113/head
    • refs/merge-requests/113/merge
    • refs/merge-requests/114/head
    • refs/merge-requests/114/merge
    • refs/merge-requests/115/head
    • refs/merge-requests/115/merge
    • refs/merge-requests/116/head
    • refs/merge-requests/116/merge
    • refs/merge-requests/117/head
    • refs/merge-requests/117/merge
    • refs/merge-requests/118/head
    • refs/merge-requests/118/merge
    • refs/merge-requests/119/head
    • refs/merge-requests/119/merge
    • refs/merge-requests/12/head
    • refs/merge-requests/120/head
    • refs/merge-requests/120/merge
    • refs/merge-requests/121/head
    • refs/merge-requests/121/merge
    • refs/merge-requests/122/head
    • refs/merge-requests/122/merge
    • refs/merge-requests/123/head
    • refs/merge-requests/123/merge
    • refs/merge-requests/124/head
    • refs/merge-requests/124/merge
    • refs/merge-requests/125/head
    • refs/merge-requests/125/merge
    • refs/merge-requests/126/head
    • refs/merge-requests/126/merge
    • refs/merge-requests/127/head
    • refs/merge-requests/127/merge
    • refs/merge-requests/128/head
    • refs/merge-requests/128/merge
    • refs/merge-requests/129/head
    • refs/merge-requests/129/merge
    • refs/merge-requests/13/head
    • refs/merge-requests/130/head
    • refs/merge-requests/130/merge
    • refs/merge-requests/131/head
    • refs/merge-requests/131/merge
    • refs/merge-requests/132/head
    • refs/merge-requests/132/merge
    • refs/merge-requests/15/head
    • refs/merge-requests/16/head
    • refs/merge-requests/17/head
    • refs/merge-requests/18/head
    • refs/merge-requests/19/head
    • refs/merge-requests/2/head
    • refs/merge-requests/21/head
    • refs/merge-requests/22/head
    • refs/merge-requests/23/head
    • refs/merge-requests/25/head
    • refs/merge-requests/26/head
    • refs/merge-requests/27/head
    • refs/merge-requests/27/merge
    • refs/merge-requests/28/head
    • refs/merge-requests/28/merge
    • refs/merge-requests/3/head
    • refs/merge-requests/32/head
    • refs/merge-requests/32/merge
    • refs/merge-requests/33/head
    • refs/merge-requests/35/head
    • refs/merge-requests/35/merge
    • refs/merge-requests/4/head
    • refs/merge-requests/40/head
    • refs/merge-requests/40/merge
    • refs/merge-requests/43/head
    • refs/merge-requests/43/merge
    • refs/merge-requests/45/head
    • refs/merge-requests/45/merge
    • refs/merge-requests/47/head
    • refs/merge-requests/47/merge
    • refs/merge-requests/49/head
    • refs/merge-requests/49/merge
    • refs/merge-requests/50/head
    • refs/merge-requests/50/merge
    • refs/merge-requests/52/head
    • refs/merge-requests/52/merge
    • refs/merge-requests/54/head
    • refs/merge-requests/54/merge
    • refs/merge-requests/55/head
    • refs/merge-requests/55/merge
    • refs/merge-requests/57/head
    • refs/merge-requests/57/merge
    • refs/merge-requests/58/head
    • refs/merge-requests/58/merge
    • refs/merge-requests/59/head
    • refs/merge-requests/59/merge
    • refs/merge-requests/6/head
    • refs/merge-requests/6/merge
    • refs/merge-requests/60/head
    • refs/merge-requests/60/merge
    • refs/merge-requests/61/head
    • refs/merge-requests/61/merge
    • refs/merge-requests/62/head
    • refs/merge-requests/62/merge
    • refs/merge-requests/63/head
    • refs/merge-requests/63/merge
    • refs/merge-requests/64/head
    • refs/merge-requests/64/merge
    • refs/merge-requests/65/head
    • refs/merge-requests/65/merge
    • refs/merge-requests/66/head
    • refs/merge-requests/66/merge
    • refs/merge-requests/67/head
    • refs/merge-requests/67/merge
    • refs/merge-requests/68/head
    • refs/merge-requests/68/merge
    • refs/merge-requests/69/head
    • refs/merge-requests/69/merge
    • refs/merge-requests/70/head
    • refs/merge-requests/70/merge
    • refs/merge-requests/71/head
    • refs/merge-requests/71/merge
    • refs/merge-requests/72/head
    • refs/merge-requests/72/merge
    • refs/merge-requests/74/head
    • refs/merge-requests/74/merge
    • refs/merge-requests/75/head
    • refs/merge-requests/75/merge
    • refs/merge-requests/78/head
    • refs/merge-requests/78/merge
    • refs/merge-requests/79/head
    • refs/merge-requests/79/merge
    • refs/merge-requests/8/head
    • refs/merge-requests/82/head
    • refs/merge-requests/82/merge
    • refs/merge-requests/9/head
    • refs/merge-requests/90/head
    • refs/merge-requests/90/merge
    • refs/merge-requests/92/head
    • refs/merge-requests/92/merge
    • refs/merge-requests/93/head
    • refs/merge-requests/93/merge
    • refs/merge-requests/94/head
    • refs/merge-requests/94/merge
    • refs/merge-requests/95/head
    • refs/merge-requests/95/merge
    • refs/merge-requests/96/head
    • refs/merge-requests/96/merge
    • refs/merge-requests/97/head
    • refs/merge-requests/97/merge
    • refs/merge-requests/98/head
    • refs/merge-requests/98/merge
    • refs/merge-requests/99/head
    • refs/merge-requests/99/merge
    • refs/tags/ISOLA2020
    • d116674d67eca4b4b15d7c08efd878a8c8aa864b
    • FMBC_2019
  • 41bf34f
  • /
  • src
  • /
  • contracts_coq
  • /
  • fa12_dexter_spec.v
Raw File Download
Take a new snapshot of a software origin

If the archived software origin currently browsed is not synchronized with its upstream version (for instance when new commits have been issued), you can explicitly request Software Heritage to take a new snapshot of it.

Use the form below to proceed. Once a request has been submitted and accepted, it will be processed as soon as possible. You can then check its processing state by visiting this dedicated page.
swh spinner

Processing "take a new snapshot" request ...

Permalinks

To reference or cite the objects present in the Software Heritage archive, permalinks based on SoftWare Hash IDentifiers (SWHIDs) must be used.
Select below a type of object currently browsed in order to display its associated SWHID and permalink.

  • revision
  • directory
  • content
  • snapshot
origin badgerevision badge
swh:1:rev:d116674d67eca4b4b15d7c08efd878a8c8aa864b
origin badgedirectory badge Iframe embedding
swh:1:dir:6daf21c967c43f4fd0e075c74bded4dc7ac5ef7d
origin badgecontent badge Iframe embedding
swh:1:cnt:ab3122e75713fa76b6b8d759e2424559ef27f3c2
origin badgesnapshot badge
swh:1:snp:2f08cb74658b563b0774f3a403ea265cf76058c6
Citations

This interface enables to generate software citations, provided that the root directory of browsed objects contains a citation.cff or codemeta.json file.
Select below a type of object currently browsed in order to generate citations for them.

  • revision
  • directory
  • content
  • snapshot
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Tip revision: d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC
Added README
Tip revision: d116674
fa12_dexter_spec.v
(* Open Source License *)
(* Copyright (c) 2021 Nomadic Labs. <contact@nomadic-labs.com> *)

(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)

(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)

(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)

Require Import NArith.
Require Import ZArith.
Require Import syntax.
Require Import semantics.
Require Import comparable.
Require Import error.
Require Import utils.
Require Import fa12_interface.
Require Import fa12_dexter.

Import List.ListNotations.

Open Scope list_scope.

Module FA12DexterSpec (C : ContractContext).

  Module fa12AxiomsImpl := FA12AxiomsImpl C.
  Import fa12AxiomsImpl.
 
  Import fa12TypesImpl fa12DataImpl fa12Notations.
  Import self semantics.

  (** Entry point specifications *)
  Section EntryPoints.

    Variable (env : @proto_env self_type).

    Notation sender := (sender env).

    (** Entry point: ep_approve *)
    Definition ep_approve
               (p : data parameter_ep_approve_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(spender, allowance') := p in
      let allowance := getAllowance sto sender spender in
      (allowance = 0%N \/ allowance' = 0%N) /\
      ret_sto = setAllowance sto sender spender allowance' /\
      ret_ops = nil.

    (** Entry point: ep_transfer *)
    Definition ep_transfer
               (p : data parameter_ep_transfer_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(from, (to, value)) := p in
      exists from_balance',
      let from_balance := getBalance sto from in
      from_balance = (from_balance' + value)%N /\
      let sto' := setBalance sto from from_balance' in
      let to_balance := getBalance sto' to in
      let sto'' := setBalance sto' to (to_balance + value)%N in
      if (compare_equal sender from)
         then ret_sto = sto'' /\ ret_ops = nil
         else exists allowance',
              let allowance := getAllowance sto from sender in
              allowance = (allowance' + value)%N /\
              ret_sto = setAllowance sto'' from sender allowance' /\
              ret_ops = nil.

    (** Entry point: ep_mintOrBurn *)
    Definition ep_mintOrBurn
               (p : data parameter_ep_mintOrBurn_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(amount, owner) := p in
      sender = getAdmin sto /\ exists balance',
      let balance := getBalance sto owner in
      Z.of_N balance' = (Z.of_N balance + amount)%Z /\
      let supply' := Z.abs_N (Z.of_N (getTotalSupply sto) + amount)%Z in
      ret_sto = setBalance (setTotalSupply sto supply') owner balance' /\
      ret_ops = nil.

    (** Entry point: ep_getTotalSupply *)
    Definition ep_getTotalSupply
               (p : data parameter_ep_getTotalSupply_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(_, contr) := p in
      let supply := getTotalSupply sto in
      let op := transfer_tokens env nat supply (0 ~Mutez) contr in
      ret_sto = sto /\ ret_ops = [op].

    (** Entry point: ep_getBalance *)
    Definition ep_getBalance
               (p : data parameter_ep_getBalance_ty)
               (sto : data storage_ty)
               (ret_ops :  data (list operation))
               (ret_sto :  data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(owner, contr) := p in
      let balance := getBalance sto owner in
      let op := transfer_tokens env nat balance (0 ~Mutez) contr in
      ret_sto = sto /\ ret_ops = [op].

    (** Entry point: ep_getAllowance *)
    Definition ep_getAllowance
               (p : data parameter_ep_getAllowance_ty)
               (sto : data storage_ty)
               (ret_ops :  data (list operation))
               (ret_sto :  data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '((owner, spender), contr) := p in
      let allowance := getAllowance sto owner spender in
      let op := transfer_tokens env nat allowance (0 ~Mutez) contr in
      ret_sto = sto /\ ret_ops = [op].

  End EntryPoints.

  (** Full spec *)
  Definition spec
             (env : @proto_env self_type)
             (p : data parameter_ty)
             (sto : data storage_ty)
             (ret_ops : data (list operation))
             (ret_sto : data storage_ty) :=
    match p with
      | inl (inl (inl q)) => ep_approve env q sto ret_ops ret_sto
      | inl (inl (inr q)) => ep_getAllowance env q sto ret_ops ret_sto
      | inl (inr (inl q)) => ep_getBalance env q sto ret_ops ret_sto
      | inl (inr (inr q)) => ep_getTotalSupply env q sto ret_ops ret_sto
      | inr (inl q) => ep_mintOrBurn env q sto ret_ops ret_sto
      | inr (inr q) => ep_transfer env q sto ret_ops ret_sto
    end.

End FA12DexterSpec.
The diff you're trying to view is too large. Only the first 1000 changed files have been loaded.
Showing with 0 additions and 0 deletions (0 / 0 diffs computed)
swh spinner

Computing file changes ...

back to top

Software Heritage — Copyright (C) 2015–2025, The Software Heritage developers. License: GNU AGPLv3+.
The source code of Software Heritage itself is available on our development forge.
The source code files archived by Software Heritage are available under their own copyright and licenses.
Terms of use: Archive access, API— Contact— JavaScript license information— Web API