aweinstock

The post "A Very General Method of Computing Shortest Paths" (https://r6.ca/blog/20110808T035622Z.html) shows that the Gauss-Jordan algorithm for solving matrix equations, the Floyd-Warshall algorithm for all-pairs shortest paths, and Kleene's algorithm for converting DFAs to regular expressions, are all the same algorithm on matrices of elements from a star-semiring.

I do think adding a Noita-style cellular automaton would be fairly straightforward.

Currently Veloren has water and lava, but neither will flow (e.g. if water blocks are manually placed on top of a hill, they won't flow downhill, fortunately this is rare due to worldgen). A simple way to fix this would be to have an ECS system that uses CA-style rules (e.g. a water block with an adjacent-and-below air block swaps places with that air block), though naively doing this would be expensive (iterating over all loaded terrain chunks every tick). A possible optimization would be to detect such blocks, remove them from the main terrain grid, put them in a separate entity-with-terrain-collider (the same kind we use for airships), and only iterate the (sparsely populated) AABB of fluids-that-have-recently-moved. This is similar to what Noita does with keeping track of recently-updated terrain rectangles. Once this is in place, it can be straightforwardly extended with more fluid interactions (e.g. Minecraft-style water + lava = obsidian, more Noita-inspired gases rising).

The contrast between Gauss-Jordan[0] and the Bareiss algorithm[1] is a good example of explicitly handling the length of the numbers in bits as part of the runtime.

Gauss-Jordan is O(n^3) if you consider addition and multiplication to be constant-time, but if it operates on arbitrary-precision integers, it can get exponentially slow[2].

The Bareiss algorithm avoids this worst-case behavior by choosing the pivots in a slightly more involved manner, which avoids building up large intermediate values.

[0]: https://en.wikipedia.org/wiki/Gaussian_elimination#Computati... [1]: https://en.wikipedia.org/wiki/Bareiss_algorithm [2]: https://staff.itee.uq.edu.au/havas/fh97.pdf, Section 3.1's "Construction A" is a specific matrix that exhibits the worst-case behavior.

Section 5.13 advises building a custom type-and-mode checkers (per project, seemingly).

Section 4.1 defines a specific type-and-mode system in enough detail that it seems machine-checkable (potentially with the declarations as-is, with suitable declarations of unary `+` and `-` via `op/3` for modes).

It feels like an omission that the paper doesn't recommend or even mention the existence of an implementation-agnostic, project-agnostic type-and-mode checker.

Has one been developed since the paper was published, or is this not as useful as it would seem/not done for some other reason?

LLVM calls the process of breaking a struct/object into dataflow variables "Scalar Replacement of Aggregates".

https://llvm.org/doxygen/classllvm_1_1SROA.html#details

If your source language has some construct that you want to express as state machines (e.g. async, CPS, pattern match compilation), and you want to compile the state machine as direct threaded code[0] (which involves fewer branches than a while-switch), then if you're compiling to C, you need computed gotos[1], which are non-standard.

[0]: https://en.wikipedia.org/wiki/Threaded_code#Direct_threading [1]: https://gcc.gnu.org/onlinedocs/gcc/Labels-as-Values.html

It's definitely the case that some of the ELF header fields can be repurposed to store additional data, the following articles all address that optimization:

http://www.muppetlabs.com/~breadbox/software/tiny/teensy.htm... https://www.pimzero.com/2020/04/19/golf_so.html https://rpis.ec/blog/plaidctf-golfso/

There are also a few instructions in the article that are size-suboptimal (e.g. "movl $4, %eax" is 5 bytes (b804000000), while the equivalent "xor %eax, %eax; movb $4, %al" is only 4 bytes (31c0b004)).

It's probably worth noting that the majority of the development on that library was done on April 1st 2019.

Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.

For a concrete example of how z3 differs from Coq, consider trying to prove that "for all integers x, there exists an integer y greater than x such that x divides y" (a subgoal of Euclid's theorem on there being infinitely many primes).

Here's a transcript of using the z3 python bindings to ask for a proof:

    $ python
    >>> import z3
    >>> x, y = z3.Ints('x y')
    >>> s = z3.Solver()
    >>> s.add(z3.Not(z3.ForAll([x], z3.Exists([y], z3.And(y >= x, y % x == 0)))))
    >>> s.check()
    unknown

z3 returns unknown (if it had returned "unsat", it would have been possible to extract a resolution-refutation proof), and there's not much that can be done with the unknown.

Here's a Coq interactive session that proves most of the cases (with one subproof left unsolved, it was taking me too long relative to the rest of the proof).

    $ coqtop
    Require Import NArith.
    Require Import Omega.

    Lemma x_le_fact : forall x, x <= fact x.
    induction x;.
    - simpl; omega.
    - simpl; admit. (* Proving `x <= fact x -> S x <= fact x + x * fact x` left unsolved here *)
    Admitted.

    Goal forall (x : nat), exists (y : nat), y >= x /\ Nat.modulo y x = 0.
    intros x; exists (fact x).
    split.
    - unfold ">=". apply x_le_fact.
    - induction x.
        + simpl; reflexivity.
        +
      (* goal here is `fact (S x) mod S x = 0` *)
      unfold fact; fold fact.
      (* goal here is `(S x * fact x) mod S x = 0` *)
      rewrite (Nat.mul_comm (S x) (fact x)).
      (* goal here is `(fact x * S x) mod S x = 0` *)
      apply (Nat.mod_mul (fact x) (S x)).
      discriminate.
    Qed.

Unlike z3, you need to manually tell Coq what the steps are, but it gives you feedback on which steps are correct, and what assumptions are available and what subgoals still remain at each step (I've included some of those as comments, running the proof through the interpreter shows more detail).

The Knight Capital incident lost $440m in 45 minutes to a mistake in software deployment: https://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stoc...

> not all assignment makes a function impure

That's exactly what the ST monad/STRef's are for. {new,read,write}STRef let you manipulate mutable references while keeping track of their scope in the type of the reference. runST encapsulates a chunk of code that manipulates mutable variables in an externally-pure way into a pure function. The "Lazy Functional State Threads"[1] paper on it is a pretty good read.

[1]: https://www.microsoft.com/en-us/research/wp-content/uploads/...

As an exercise in learning Coq, I've implemented a proof-carrying version of the partial-ordering relation: https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e95...

There's four different types there: POSET, POSET_PROOFS, Pord, and POSET'.

- POSET only has an underlying type t and a function "leq" that takes two elements of type t and returns a bool (but doesn't enforce semantics of that bool).

- POSET_PROOFS embeds a POSET, and carries three proofs (reflexivity, antisymmetry, and transitivity) certifying that the underlying "leq" function is actually the less-than-or-equal function of a partial ordering.

- Pord is a result type with 4 values meant to denote the exhaustive possiblities of "strictly less"/"equal"/"strictly greater"/"uncomparable".

- POSET' has a type t', a function "pcomp" that takes two elements of type t' and returns a Pord, and a proof for transitivity in the "strictly less" case.

POSET' has fewer fields to instantiate, but POSET_PROOFS allows writing proofs that are closer to traditional math.

Fortunately, the fact that it's possible to write conversions between POSET_PROOFS and POSET' (done in the code as "from" and "to" in the POSET_ISOMORPHIMS module right below) indicate that they have the same properties.

For a concrete example of what exploitation of a JS engine bug looks like, PlaidCTF2016 had a challenge that allowed people to run JS in a patched version of V8 that deliberately introduced a bug in array index checking, with the goal being to run x86 machine code.

The patch to v8: http://lpaste.net/317342

An exploit: https://gist.github.com/sroettger/d077d3907999aaa0f89d11d956...

While this bug was artificial, there were (and can still be) bugs with similar consequences in actual engines (see https://www.cvedetails.com/vulnerability-list/vendor_id-1224... or https://cve.mitre.org/cgi-bin/cvekey.cgi?keyword=spidermonke... for historical examples).

While a bug in most of the components you mention are bad by themselves, their impact is magnified by the presence of javascript, which allows an attacker to interleave calculations and interactions with the buggy components, bypassing many mitigations.

Rust's set types do implement the BitAnd and BitOr traits, which allow using the & operator for intersection, | for union (There's also a few others, like (Sub, -, set difference) and (BitXor, ^, symmetric difference)).

They use Clone to construct a new set for the result, for use with a functional style. There are also the union/intersection methods that produce lazy iterators over references to the values in the sets, for cases where cloning the set elements would be too big a runtime price, at a slight cost to ergonomics.

Clone-based operator overloading:

https://doc.rust-lang.org/std/collections/struct.HashSet.htm...

https://doc.rust-lang.org/std/collections/struct.HashSet.htm...

Lazy-iterator-based methods:

https://doc.rust-lang.org/std/collections/struct.HashSet.htm...

https://doc.rust-lang.org/std/collections/struct.HashSet.htm...

Do these qualify as reasonable set operations?

Searching the history to enforce the threefold repetition rule[1] wouldn't be efficient, but the fifty-move rule[2] could be pretty cheaply implemented (one cell of state for a counter, an increment-and-check per move, and resetting the counter to 0 on the relevant moves).

[1]: https://en.wikipedia.org/wiki/Threefold_repetition [2]: https://en.wikipedia.org/wiki/Fifty-move_rule

It's a monad in Rust too (with Some being return, and and_then[1] being >>=). Rust's generics just aren't yet[2] flexible enough to abstract over monads within the language.

[1] https://doc.rust-lang.org/std/option/enum.Option.html#method... [2] https://github.com/rust-lang/rfcs/issues/324

Attacker-controlled format strings are very convenient bugs, but they can't do everything. Consider the program:

    int main() {
        char buf[20];
        fgets(buf, sizeof buf, stdin);
        printf(buf);
        return 0;
    }

An attacker writing to the program's stdin can read at offsets to the stack (e.g. "%42$x"), read the contents of arbitrary non-null memory (e.g. "ABCD%5$s", where ABCD is a 32-bit memory address, and 5 is the positional parameter corresponding to the start of buf), and write an arbitrary value to an arbitrary address (e.g. "ABCD%38x%5$n", to write the value 42 to address 0x44434241).

A significant limitation of the vulnerability in the above program is the attacker can't, in a single execution of the program, read a value, then do computations on it locally, then write a value based on those computations. This flexibility is needed in order to bypass ASLR.

Without this patch, using an information leak to bypass ASLR would be as simple as leaking any address in libc (__libc_start_main is often convenient since it's where main returns to when the progam ends, and hence is already on the stack), subtracting the (fixed, public) offset from the leak to calculate the base address libc was loaded at, and adding the (again fixed and public) offset from libc's base to some useful function (e.g. system(3)).

With this patch, the order of symbols are randomized every boot, so the offsets that were previously fixed and public aren't.

It's probably still possible, if you have multiple adaptive memory reads, to traverse the datastructures that legitimate programs use to find the order of the symbols, but a) not all information leaks can be used to read arbitrary addresses multiple times, and b) the traversal code becomes more complicated for the attacker to {write,maintain} relative to the simple arithmetic that was previously possible.

The above analysis is for remote exploits, local privilege escalation exploits can just read libc to determine the order (since it's re-linked on boot, not per process).

This is fairly readable (high-level) post on word embeddings: http://colah.github.io/posts/2014-07-NLP-RNNs-Representation...

Higher branching factor gets you a better constant factor because the depth of the tree is the base-(branching factor) logarithm of the number of nodes. The number of pointers you need to follow to reach a leaf is equal to the depth of the tree, and pointer-dereferences are likely to cause a cache miss, which is a relatively slow operation.

You're correct that asymptotically, it's the same thing.

There's some more in-depth documentation in the repo in doc/user_guide.txt, at around line 520-ish.

It has Common Lisp style defmacro (augmented with pattern matching), and Scheme-inspired defsyntax. The documentation warns that both are unhygienic, and `grep -ri gensym` didn't find anything in the repo.