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.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:a12a567850b0ff1d5ad8792438131b5edb1742e0
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.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 main.
Require Import util.
Require Import utils.
Require Import fa12_interface.
Require fa12_dexter_string.

Module annot.

  Import String.

  Notation mintOrBurn := "%mintOrBurn".

End annot.

(** Parameter type definitions. *)
Definition parameter_ep_mintOrBurn_ty
  := pair int address.

(** FA1.2 types implementation *)
Module fa12TypesImpl.

  Definition parameter_ty :=
    or (or (or parameter_ep_approve_ty (Some annot.approve)
               parameter_ep_getAllowance_ty (Some annot.getAllowance)) None
           (or parameter_ep_getBalance_ty (Some annot.getBalance)
               parameter_ep_getTotalSupply_ty (Some annot.getTotalSupply)) None) None
       (or parameter_ep_mintOrBurn_ty (Some annot.mintOrBurn)
           parameter_ep_transfer_ty (Some annot.transfer)) None.

  Definition ledger_ty : type := big_map address nat.

  Definition allowances_ty : type := big_map (Cpair address address) nat.

  Definition storage_ty : type :=
    pair ledger_ty (pair allowances_ty (pair address nat)).

End fa12TypesImpl.

(** FA1.2 data implementation *)
Module FA12DataImpl (C : ContractContext).

  Module semantics := Semantics C.
  Import semantics.

  Import fa12TypesImpl.

  Definition extract_fa12_ep (p : data parameter_ty) : data (option fa12_parameter_ty) :=
    match p with
      | inl (inl (inl q)) => Some (inl (inr q))
      | inl (inl (inr q)) => Some (inr (inl q))
      | inl (inr (inl q)) => Some (inr (inr (inl q)))
      | inl (inr (inr q)) => Some (inr (inr (inr q)))
      | inr (inl _) => None
      | inr (inr q) => Some (inl (inl q))
    end.

  Definition getBalanceOpt (sto : data storage_ty) (owner : data address) : data (option nat) :=
    let '(ledger, _) := sto
    in cmap_get address owner ledger.

  Definition setBalance (sto : data storage_ty) (owner : data address) (balance' : data nat) : data storage_ty :=
    let '(ledger, (allowances, (admin, supply))) := sto in
    let balanceOpt := if (compare_equal balance' 0%N) then None else (Some balance') in
    let ledger' := cmap_update address owner balanceOpt ledger in
    (ledger', (allowances, (admin, supply))).

  Definition getAllowanceOpt (sto : data storage_ty) (owner spender : data address) : data (option nat) :=
    let '(_, (allowances, _)) := sto in
    cmap_get (Cpair address address) (owner, spender) allowances.

  Definition setAllowance (sto : data storage_ty) (owner spender : data address) (allowance' : data nat) : data storage_ty :=
    let '(ledger, (allowances, (admin, supply))) := sto in
    let allowanceOpt := if (compare_equal allowance' 0%N) then None else (Some allowance') in
    let allowances' := cmap_update (Cpair address address) (owner, spender) allowanceOpt allowances in
    (ledger, (allowances', (admin, supply))).

  Definition getAdmin (sto : data storage_ty) : data address :=
    let '(_, (_, (admin, _))) := sto in admin.

  Definition getTotalSupply (sto : data storage_ty) : data nat :=
    let '(_, (_, (_, supply))) := sto in supply.

  Definition setTotalSupply (sto : data storage_ty) (supply' : data nat) : data storage_ty :=
    let '(ledger, (allowances, (admin, _))) := sto in
    (ledger, (allowances, (admin, supply'))).

  Definition getOwners (sto : data storage_ty) : set.set (data address) (compare address).
  Proof.
    destruct sto as [ledger _]; cbn.
    exists (List.map fst (map.to_list _ _ _ ledger)).
    apply Sorted.Sorted_StronglySorted.
    1: exact (lt_trans address).
    destruct ledger as [ | k v l]; cbn.
    - auto.
    - induction l as [ | k k' v' H_k_k' l IHl]; cbn.
      all: constructor; auto.
  Defined.

End FA12DataImpl.

Module FA12AxiomsImpl (C : ContractContext).

  Import fa12TypesImpl.

  Module fa12DataImpl := FA12DataImpl C.
  Import fa12DataImpl.

  Import semantics.

  Module fa12Notations := FA12Notations C fa12TypesImpl fa12DataImpl.
  Import fa12Notations.

  Lemma ep_transfer_required (q : data parameter_ep_transfer_ty) :
    exists p, extract_fa12_ep p = Some (inl (inl q)).
  Proof.
    split with (inr (inr q)); auto.
  Qed.

  Lemma ep_approve_required (q : data parameter_ep_approve_ty) :
    exists p, extract_fa12_ep p = Some (inl (inr q)).
  Proof.
    split with (inl (inl (inl q))); auto.
  Qed.

  Lemma ep_getAllowance_required (q : data parameter_ep_getAllowance_ty) :
    exists p, extract_fa12_ep p = Some (inr (inl q)).
  Proof.
    split with (inl (inl (inr q))); auto.
  Qed.

  Lemma ep_getBalance_required (q : data parameter_ep_getBalance_ty) :
    exists p, extract_fa12_ep p = Some (inr (inr (inl q))).
  Proof.
    split with (inl (inr (inl q))); auto.
  Qed.

  Lemma ep_getTotalSupply_required (q : data parameter_ep_getTotalSupply_ty) :
    exists p, extract_fa12_ep p = Some (inr (inr (inr q))).
  Proof.
    split with (inl (inr (inr q))); auto.
  Qed.

  Opaque compare.

  Lemma getBalance_setBalance_eq sto owner amount :
    getBalance (setBalance sto owner amount) owner = amount.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z eqn:eq.
    all: rewrite map_get_update_eq; auto.
    rewrite eqb_eq in eq; subst; auto.
  Qed.

  Lemma getBalance_setBalance_neq sto owner owner' amount :
    owner <> owner' ->
    getBalance (setBalance sto owner amount) owner' =
    getBalance sto owner'.
  Proof.
    intro H.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z.
    all: rewrite map_get_update_neq; auto.
  Qed.

  Lemma getAllowance_setAllowance_eq sto owner spender amount :
    getAllowance (setAllowance sto owner spender amount) owner spender = amount.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z eqn:eq.
    all: rewrite map_get_update_eq; auto.
    rewrite eqb_eq in eq; subst; auto.
  Qed.

  Lemma getAllowance_setAllowance_neq sto owner owner' spender spender' amount :
    owner <> owner' \/ spender <> spender' ->
    getAllowance (setAllowance sto owner spender amount) owner' spender' =
    getAllowance sto owner' spender'.
  Proof.
    intro H.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z.
    all: rewrite map_get_update_neq; auto.
    all: intro H'; injection H'; intuition.
  Qed.

  Lemma getAllowance_setBalance sto owner sender spender amount :
    getAllowance (setBalance sto owner amount) sender spender =
    getAllowance sto sender spender.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn; auto.
  Qed.

  Lemma getBalance_setAllowance sto owner sender spender amount :
    getBalance (setAllowance sto sender spender amount) owner =
    getBalance sto owner.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn; auto.
  Qed.

  Lemma getOwners_mem sto owner :
    cset_mem owner (getOwners sto) = isOwner sto owner.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct ledger as [ | k v ledger]; cbn.
    - auto.
    - revert v.
      induction ledger as [ | k k' v' H_k_k' l IHl]; cbn.
      all: intro v.
      + destruct compare; auto.
      + destruct compare eqn:H_owner_k at 1 3; cbn.
        all: auto; apply IHl.
  Qed.

End FA12AxiomsImpl.

Import fa12TypesImpl.

Module self := Self fa12TypesImpl.
Import self.

Definition contract
  := Eval cbv in extract (contract_file_M fa12_dexter_string.contract 500) I.

Definition main :
  instruction self_type false
              (pair parameter_ty storage_ty ::: nil)
              (pair (list operation) storage_ty ::: nil) :=
  Instruction_seq (contract_file_code contract).
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