Search

An effective model for protein structures is important for the study of protein geometry, which, to a large extent, determine the functions of proteins. There are a number of approaches for modelling; one might focus on the conformation of the backbone or H-bonds, and the model may be based on the geometry or the topology of the structure in focus. We focus on the topology of H-bonds in proteins, and explore the link between the topology and the geometry of protein structures. More specifically, we take inspiration from CASP Evaluation of Model Accuracy and investigate the extent to which structural similarities, via GDT_TS, can be estimated from the topology of H-bonds. We report on two experiments; one where we attempt to mimic the computation of GDT_TS based solely on the topology of H-bonds, and the other where we perform linear regression where the independent variables are various scores computed from the topology of H-bonds. We achieved an average $\Delta\text{GDT}$ of 6.45 with 54.5% of predictions inside 2 $\Delta\mathrm{GDT}$ for the first method, and an average $\Delta\mathrm{GDT}$ of 4.41 with 72.7% of predictions inside 2 $\Delta\mathrm{GDT}$ for the second method., Comment: 11 pages, 11 figures

H-bonds are known to play an important role in the folding of proteins into three-dimensional structures, which in turn determine their diverse functions. The conformations around H-bonds are important, in that they can be non-local along the backbone and are therefore not captured by the methods such as Ramachandran plots. We study the relationship between the geometry of H-bonds in proteins, expressed as a spatial rotation between the two bonded peptide units, and their topology, expressed as a subgraph of the protein fatgraph. We describe two experiments to predict H-bond rotations from their corresponding subgraphs. The first method is based on sequence alignment between sequences of the signed lengths of H-bonds measured along the backbone. The second method is based on finding an exact match between the descriptions of subgraphs around H-bonds. We find that 88.14% of the predictions lie inside the ball, centred around the true rotation, occupying just 1% of the volume of the rotation space SO(3)., Comment: 24 pages, 15 figures

We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call $\lambda^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised $\lambda^T_\square$ representation, we obtain code in two functional smart contract languages (Liquidity and CameLIGO), the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages., Comment: 57 pages; Coq development: https://github.com/AU-COBRA/ConCert/tree/journal-2021. arXiv admin note: substantial text overlap with arXiv:2012.09138

We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, an escrow contract, an implementation of a Decentralized Finance (DeFi) contract which includes a custom token standard (Tezos FA2), and more. In total, this gives us a way to write dependent programs in Coq, test them semi-automatically, verify, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages., Comment: Coq implementation: https://github.com/AU-COBRA/ConCert/tree/artifact-2020 Update: fixed the "author running" list, fixed a mistake in an evaluation rule for lambda-box (Section 3.1, item 2)

We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq's functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular we develop a Congress contract in this style. This contract -- a simplified version of the infamous DAO -- is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress's behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.

We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we develop an embedding of a core smart contract language into Coq and verify several important properties of a crowdfunding contract based on a previous formalisation of smart contract execution in blockchains., Comment: Extended the related work section. Significantly extended sections on translation and semantics. Added more examples and details about the formalisation. Commented of unquote and the trusted computing base. Commented on adequacy