aterga

(define-fun e8s ((x Int)) Int (* x 100000000))

; Example values based on parameterf from here:
; https://nns.ic0.app/proposal/?u=qoctq-giaaa-aaaaa-aaaea-cai&proposal=131075
(define-const minimum_participants Int 50)
(define-const minimum_direct_participation_icp Int (e8s 50000))
(define-const maximum_direct_participation_icp Int (e8s 250000))
(define-const minimum_participant_icp Int (e8s 10))
(define-const maximum_participant_icp Int (e8s 50000))

aterga

A Taste of Verification-Assisted Development in Motoko

In this post, we demonstrate how Internet Computer developers can leverage automatic verification to build bug-free, Web3 applications in Motoko. We start by explaining why this is tricky. We then demonstrate an example smart contract (a.k.a. canister in Motoko), showing how to formally specify and (automatically) verify it. We conclude with a discussion of our experience and observations gathered while working on this (very experimental) verification technique.

We wrote this post because we wanted to make more of DFINITY's formal verification know-how available to developers outside the Foundation. While DFINITY employs verification experts to formally specify and verify some of our smart contracts, we believe that formal verification is beneficial to all Web3 projects, especially in high-stake applicatio

aterga

\newcommand*{\singleton}{%
\tikz[x=1em, y=1em, baseline=(peacesymbol.base), line width=0.098em]{%
  \node (peacesymbol) {\quad}; 
  \begin{scope}[shift={(0,-0.25)}]
    \draw (0.5,0.5) circle (0.5);
    \draw (0.5,0) -- (0.5,1);
    \draw (0.15,0.15) -- (0.5,0.50);
    \draw (0.85,0.15) -- (0.5,0.50);
  \end{scope}
}}

aterga

console.log(process.env);  // Encapsulation Vulnerability

aterga

%%% This file defines the command \boldfrak{STRING} that maps regular Latin characters to bold Fraktur. 
%%% Should work in XeLaTeX with any font that supports Frakturs; if the \mathfrak command works then this 
%%%  \boldfrak should work as well. I tested this only in math mode. 

\newcommand{\boldfraksymb}[1]{%
  \ifthenelse{\equal{#1}{a}}{𝖆}{%
  \ifthenelse{\equal{#1}{b}}{𝖇}{%
  \ifthenelse{\equal{#1}{c}}{𝖈}{%
  \ifthenelse{\equal{#1}{d}}{𝖉}{%
  \ifthenelse{\equal{#1}{e}}{𝖊}{%

aterga

# Simple commands for collecting basic SMT statistics

# Get file names
for f in $(for file in group_*/*.smt2; do ls $file | xargs -n 1 basename;  done); do printf ",$f"; done > stat.csv
echo >> stat.csv

# Get the logic
for f in $(for file in group_*/*.smt2; do cat $file | grep -oP "(?<=\(set-logic )(.*)(?=\))";  done); do printf ",$f"; done >> stat.csv
echo >> stat.csv

aterga

(* 
  Ported from Dafny. 
  Original version: https://github.com/dafny-lang/dafny/blob/master/Test/tutorial/maximum.dfy 
*)

module Maximum

open FStar.List
include FStar.List.Tot

aterga

%Insert your settings above
%Insert your text below

aterga

#!/bin/bash

projdir=$1
workdir=$(pwd)

git clone https://github.com/vprover/vampire.git
cd $workdir/vampire
git checkout 76d525d7ebed8fae9a1dc3aa4c9b6a8ddbe655bd
ln -s $projdir/z3/bin include 
make vampire_z3_rel

aterga

docker build -t IMAGE_NAME
docker run -it -d --name INSTANCE_NAME IMAGE_NAME
docker exec -it INSTANCE_NAME /bin/bash