Skip to content

Instantly share code, notes, and snippets.

View thealmarty's full-sized avatar

Marty Stumpf thealmarty

View GitHub Profile
@thealmarty
thealmarty / libcLog.txt
Last active June 25, 2024 18:57
libc debug
11:28:52 ~/code/lita/issue/fresh/llvm-valida$ cd build-libc/
11:29:22 ~/code/lita/issue/fresh/llvm-valida/build-libc$ cmake ../llvm -G Ninja -DLLVM_ENABLE_PROJECTS="clang;libc;lld;compiler-rt" -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/home/marty/code/lita/issue/new/llvm-valida/build/bin/clang -DCMAKE_CXX_COMPILER=/home/marty/code/lita/issue/new/llvm-valida/build/bin/clang++ -DLLVM_LIBC_FULL_BUILD=ON -DLLVM_LIBC_INCLUDE_SCUDO=OFF -DCOMPILER_RT_BUILD_GWP_ASAN=OFF -DCOMPILER_RT_SCUDO_STANDALONE_BUILD_SHARED=OFF -DCLANG_DEFAULT_LINKER=/home/marty/code/lita/issue/new/llvm-valida/build/bin/ld.lld -DCLANG_DEFAULT_RTLIB=compiler-rt -DDEFAULT_SYSROOT=/usr -DCMAKE_INSTALL_PREFIX=/usr -DLIBC_TARGET_TRIPLE=delendum-unknown-baremetal-gnu -DLLVM_INCLUDE_TESTS=OFF -DCMAKE_BUILD_WITH_INSTALL_RPATH=true -DCMAKE_C_FLAGS="${CMAKE_C_FLAGS} -target delendum" -DCMAKE_CXX_FLAGS="${CMAKE_CXX_FLAGS} -target delendum" -DCMAKE_EXE_LINKER_FLAGS="${CMAKE_EXE_LINKER_FLAGS} -target delendum" -DCMAKE_SHARED_LINKER_FLAGS="${CMAKE_SHARED
@thealmarty
thealmarty / insertion_sort.cpp
Created February 13, 2021 18:46
Insertion sort in C++
#include <iostream>
#include <vector>
void insertion_sort(std::vector<int> & v) {
// invariant: the first i elements of v are sorted
for(size_t i = 1; i < v.size(); ++i) {
int value = v[i];
size_t j = i-1;
// invariant: elements of v from j+1 to i inclusive are sorted and >= value
for(; j >= 0 && v[j] > value; --j) {
@thealmarty
thealmarty / insertion_sort.c
Created February 13, 2021 18:28
Insertion sort in C
#include <stdio.h>
void insertion(int v[], int size) {
// invariant: the elements of v before index i are sorted
for(int i = 1; i < size; ++i) {
int value = v[i];
int j = i;
// invariant: the elements of v between j and i are sorted and > value
for(;j > 0 && v[j-1] > value; --j) {
v[j] = v[j-1];
@thealmarty
thealmarty / Markdium-idris.idr
Created December 31, 2020 17:47
Markdium-Dependent types: formal definition and examples
onePlusOne : 1+1=2
onePlusOne = Refl
@thealmarty
thealmarty / UnificationImplementationPlan.md
Last active September 30, 2020 20:09
Unification implementation plan.

MVP unification implementation plan

The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.

Stage 1: Type checker enhancement

At the time of writing, the first stage of the totality checker MVP is finished. But the second and third stages, namely type checking data type and function declarations are required before unification can be implemented.

At the end of this stage, conversion/type checking for constructors is implemented.

@thealmarty
thealmarty / PatternMatchingCompilerAlgorithm.md
Last active September 22, 2020 19:58
Efficient compilation of function definitions with pattern-matching using case-expressions.

Efficient compilation of function definitions with pattern-matching

Function definitions with pattern-matching can be compiled into case-expressions for more efficient evaluation using the pattern matching compiler algorithm. The algorithm translates function definitions into case-expressions and avoids repeated examination of patterns.

I summarize the pattern matching compiler algorithm here as in chapter 5 of The implementation of functional programming languages.

The algorithm

A function definition of the form

@thealmarty
thealmarty / idris2unification.md
Last active September 14, 2020 16:38
Unification in Idris 2

Unification in Idris 2

Unification concerns type/conversion checking with the presence of meta-variables. Meta-variables are variables with unknown values but type checking/elaboration progress could generate constraints that these variables have to satisfy and thus find the solutions to these variables. Implicits (and implicit arguments) are inferred by unification.

Conversion checking (of terms and closures) determines whether the two inputs are equivalent. Similarly, unification determines whether the two inputs are equivalent with the presence of meta-variables. Naturally, unification is implemented as an extension to conversion checking.

@thealmarty
thealmarty / idris2notes.md
Last active August 4, 2021 21:34
Lessons from Idris 2
@thealmarty
thealmarty / PLDI2020report.md
Last active August 20, 2020 15:55
PLDI 2020 report

Potential Juvix features enabled by graph neural networks and machine learning

The rapid development of machine learning (ML) enables practical applications including in smart contract development. As a superior smart contract language, Juvix can provide extra support using ML in the following fronts:

  1. Generate correctness proofs

See this paper. When combining the mechanics of Proverbot9001, CoqHammer and CoqGym, a meaningful portion (28%) of the correctness proofs of CompCert (written in Coq) was generated. Note that the difficulties of the generated proofs are evenly distributed - i.e., it is not only generating proofs that are trivial for users to write.

Juvix is built with the intent that smart contracts written in it are more secure because users can write proofs to prove important properties of a contract. However, writing proofs is a tedious and costly task. Juvix would be much more attractive if it can write a significant portion of the proof

@thealmarty
thealmarty / token.liq
Last active September 17, 2019 15:44
A simplified token contract written in Liquidity, for deployment in the Tezos ledger.
type account = {
balance : nat;
allowances : (address, nat) map;
}
type storage = {
accounts : (address, account) big_map;
version : nat;
totalSupply : nat;
name : string;