Namada SE 2 Patch 3 TLDR; There was a bug that returned non-determinstically ordered validator set updates. v0.31.5 has a bug where the state machine returns an incorrect validator set update to the consensus machine. The current network has progressed to block 42850, which halted due to the aformentioned problem. In order to fix it a majority of validator voting power must upgrade to v0.31.6. In order to restart the network 2/3+1 of voting power needs to sync the chain from scratch. Steps to upgrade

Namada SE 2 Restart 1 TLDR; There was a bug that reordered ABCI messages. v0.31.2 has a bug that causes jailing operations to be applied in a non-determinstic order. This was caught uniquely due to the bug in v0.31.1, which caused a number of random jailing events. The current network progressed to block 8671 which resulted in committing a broken state. In order to fix it a majority of validator voting power must upgrade to v0.31.4 and resync. Steps to upgrade :warning:ABOVE ALL ELSE, DON'T DELETE THE KEYS OR THE VALIDATOR STATE.:warning:

There was a bug that was introduced in version v0.31.1 by accident. The bug involved a line mistakenly moved to an async section in Namada's ABCI interface code, which could have led to reordered ABCI events and explains much of the behaviour observed on the testnet. v0.31.2 has been released, which fixes the bug. You can install either from source or use the binaries build in the CI. ABOVE ALL ELSE, DON'T DELETE THE KEYS OR THE VALIDATOR STATE. I would suggest the following steps to upgrade: Stop the validator node Move your <chain_dir> directory out of the <base_dir> by moving it somewhere else.

an autonomous ecologist's guide to namada & anoma _{^{Christopher Goes Autonomous Ecologies 2}} Alternative titles wtf are these crazy people doing? why are there so many names? will they ever ship?

In the Zero Knowledge sphere, there exists a plethora of Zero Knowledge Systems and languages. From zk-SNARK languages like Zokrates, Leo, and Vamp-IR; to STARK machines like Triton VM, Miden VM, and RISC Zero. It is difficult in the current landscape to make an informed decision about which system fits their use case best. This benchmarking endeavor seeks to alleviate these issues by readily making performance numbers between the various systems be known and provide an easy way to compare the same program across languages and systems. Currently, the amount of backends and programs that are compared is limited. However, community contributions should amplify the value provided by the benchmarking project. In particular, the benchmarking results and programs will be most useful to five kinds of individuals: Users who are building an application with a Zero Knowledge System. Compiler writers who wish to target a Zero Knowledge System. Users who have a choice of the Zero Knowledge System in their application. Zero Knowledge System implementers who wish to know optimization points.

The Berlin Pipeline was originally an architecture proposal for a compiler project written in the ML style. Which is to say the compiler is written as a series of passes and layers from the frontend language all the way down to the backend. With that said, The Berlin Pipeline should be of interest to compiler writers regardless of backgrounds and can be applied to any compiler that: Has complex pipelining

[toc] Installation The easiest way to install Alucard at the moment is through ros. Install ros Set sbcl as the default ros install sbcl-bin Update asdf ros install asdf run git clone https://github.com/anoma/juvix-circuits.git cd into the cloned directory cd juvix-circuits

Summary "Geb" (the name is an homage to Hofstadter's Gödel, Escher, Bach; despite being an acronym, it's pronounced as a single syllable and written with only an initial capital letter) is a small programming language which supports: Metaprogramming Effects Dependent types Programming languages and mathematical logics as built-in types Composition of languages and logics, with individual components defined as universal constructions Embeddable within other languages, using its effects to call out of the embedded Geb code to a host language Alternative syntaxes -- there is a precise specification of which functions an interpreter must support, but no constraint on what syntax a given interpreter should provide, and between any two valid syntaxes, there is a single correct mechanical translation (an isomorphism)

Welcome to the Alucard Reference Manual. The reference manual is laid out via sections on specific topics. Each topic contains various functions related to the topic along with documentation and example usage of each feature. For example, a section like Definition Facilities has subtopics like: defcircuit deftype

Before we can get onto the question, let us first talk about the interface of Alucard. The following concepts of Alucard are had Function application Function Creation a binder creator through def structs through deftype arrays with length and type determining the type Prolog style constraints

This document lays out the specification and documentation for the various items found in the Alucard(Alu) programming language. This document also serves as a companion piece to: A detailed Syntax Guide. This piece gives an interactive tutorial to the langugage, meaning that every piece of code in the tutorial can be run in the Alucard REPL.

This document outlines the BNF for the Alucard syntax specificaiton ;; Top Level defcircuit ::= (defcircuit <symbol> (<field>* <return>?) <expression>*) deftype ::= (deftype <symbol> () <type-field>*) field ::= (<privacy> <symbol> <type>)

Rough thoughts. We have two concepts: Module Package Modules are modules we all know and love. Namely it acts like the UNIX filesystem. Packages describe your project state, what projects we import etc.

storage space on Anoma comes at a premium, thus having small binaries is important. A typical rust WASM binary for VP's comes out to 100KB or less. Thus if we want to be practical to the usecase of Anoma, we will have to have a small runtime. Anoma uses wasmer which [1] seems to allocate A lot of vram. Normally when we start our memory image pool, we should allocate almost infinite vram to have a stable memory pool to keep allocating to. Further for VP, the runtime is expected to be quite fast, and thus contracts are short lived. Due to these two points, we should implement the GC in such a way that when we generate out to WASM, we should replace the runtime GC functions with a naieve implementation that just mallocs to the pool without any GC triggering. We can do this by linking it against the naieve implementation rather than the real one when extracting out to VP WASM.

Preamble Currenlty the syntax of Juvix is quite large, with an over 200 line BNF. This means that trying to make any extensions to the syntax should be carefully thoughtout and considered, as any change may make another part of the syntax inconsistent. Further, due to the large size it can't be studied in terms of any small data structure, we must write a 200 line nested ADT to properly hold and traverse this structure. Thus if we have any chance of properly extending the language to be ergonomic for validity-predicates or any domain an user may want. To facilitate this, we will hold the following values in-regards to syntax. Be minimal. Be consistent. Be homoiconic. Rule 1 gives us the outline that for the syntax we chose it should be as small as possible. This helps us to do analysis over the syntax. Rule 2 gives the user a consistent interface to properly "intuit" the language, and have understanding one part of the syntax help the user undersatnd another part.

Juvix as a language is type theoretic in nature. In particular, it wishes to leverage dependent type theory to make safe and fast validity-predicates. In order to properly achieve this goal, it is important to make a high level language that is fit for the domain. Thus the following properties become of the utmost importance for Juvix. Correctness Speed Ergonomic Contract Code

This document outlines writing Alucard, every expression written here is valid alucard, feel free to type along with the document into the Alucard REPL or a file that you can send over! New concepts are introduced and iterated upon in later sections. The file is a fully loadable version of this document Comments ;; This is a comment!

The Juvix module system is one that wishes to leverage the benefit of a nested module system (rust, ocaml) while maintaining a workflow that can support working interactively or through a more static approach. In order to achieve this goal, we analyze different approaches of module management, and distill the qualities that are positive to a project and user behavior. The Haskell World View The Haskell view of modules is an interesting one in that the language's modules look nested, while continuing to be flat. An argument over the Flat World Model Consider the following example -- Compilation.hs

In this document we outline the Berlin Pipeline. The document is broken up into three core chunks along with a miscellaneous section that outlines helper structures which are integral to the smooth operation of the pipeline. These four sections are The Berlin Pipeline Step The Berlin Pipeline Proper The Berlin Pipeline Automatisierung The Berlin Pipeline Extensions The fourth section covers extensions that have made it in the codebase that may alter the shape of the first three sections that are written about.

Context Juvix as a project has decided upon the Berlin Pipeline as a means of unifying the codebase (see the writeup for motivation). The Berlin also enforces a strict structure on what is a pass. Namely, the data that gets sent between compiler passes must have the following properties: Be one consistent type that can express any form (statement, expression, declaration, etc.) that the compiler may contain. Can be easily manipulated, as to be able to write tooling ontop and operate generically over it. Be able to reason over and operate over subsets of the given form that we wish to operate upon. Be easily serializable and de-serializable to whatever structure is most convenient to work over. Only a few representations fit the bill for all four of these properties, and out of those we have chosen S-expressions as the best candidate for this. This document will outline how S-expressions interact with 4., covering prior work and what we wish to do with it.