https://gitlab.com/nomadic-labs/mi-cho-coq
Revision 7a7a1aa403201894461c5ff40ae9fee67be399f3 authored by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC, committed by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC
Before this commit, set.remove uses List.remove which only computes when its decide_equality argument does. We passed it an opaque lemma so it did not compute. Moreover, it always scanned the whole list but since we only apply it on sorted lists it could stop as soon as it encounters a value larger than the one to remove. This commit redefines set.remove so that it does not depend on decidability of equality anymore and returns as soon as it can.
1 parent 6406bf3
Tip revision: 7a7a1aa403201894461c5ff40ae9fee67be399f3 authored by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC
[michocoq] Redefine set.remove so that it computes
[michocoq] Redefine set.remove so that it computes
Tip revision: 7a7a1aa
coq-mi-cho-coq.opam
version: "dev"
opam-version: "2.0"
synopsis: "A specification of Michelson in Coq to prove properties about smart contracts in Tezos"
maintainer: "raphael.cauderlier@nomadic-labs.com"
authors: [ "Raphaël Cauderlier" "Bruno Bernardo" "Julien Tesson" "Arvid Jakobsson" ]
homepage: "https://gitlab.com/nomadic-labs/mi-cho-coq/"
dev-repo: "git+https://gitlab.com/nomadic-labs/mi-cho-coq/"
bug-reports: "https://gitlab.com/nomadic-labs/mi-cho-coq/issues"
license: "MIT"
build: [
["./configure" "michocoq" "michocott"]
[make "-j%{jobs}%"]
]
install: [
make "install"
]
depends: [
"coq-list-string"
"coq-menhirlib" {>= "20190626"}
"coq-moment" {>= "1.2.0"}
"coq-ott" {>= "0.29"}
"coq" {>= "8.10" & < "8.12.0" }
"menhir"
"ocaml" {>= "4.07.1"}
"ocamlbuild"
"ott" {build & >= "0.29"}
"zarith"
]
build-test: [ make "test" ]
description: """
Michelson is a language for writing smart contracts on the Tezos blockchain.
This package provides a Coq encoding of the syntax and semantics of Michelson,
automatically generated by the Ott tool. Also included is a framework called Mi-Cho-Coq
for reasoning about Michelson programs in Coq using a weakest precondition calculus."""
tags: [
"category:Programming Languages/Formal Definitions and Theory"
"keyword:cryptocurrency"
"keyword:michelson"
"keyword:semantics"
"keyword:smart-contract"
"keyword:tezos"
"logpath:Michocoq"
"logpath:Michocott"
]
Computing file changes ...
