aweinstock

6 ms·

1.
by aweinstock 3y ago
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
2.
by aweinstock 5y ago
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, fortu
3.
by aweinstock 6y ago
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 co
4.
by aweinstock 6y ago
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 suit
5.
by aweinstock 6y ago
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
6.
by aweinstock 6y ago
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 w
7.
by aweinstock 6y ago
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&#
8.
by aweinstock 6y ago
It's probably worth noting that the majority of the development on that library was done on April 1st 2019.
9.
by aweinstock 6y ago
Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.
10.
by aweinstock 6y ago
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 ma
11.
by aweinstock 7y ago
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...
12.
Bypassing code protection on an Intel 8752(blog.inach.is)
2 points by aweinstock 8y ago|0 comments
13.
by aweinstock 9y ago
> 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. ru
14.
by aweinstock 9y ago
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 typ
15.
by aweinstock 10y ago
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
16.
by aweinstock 10y ago
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 u
17.
by aweinstock 10y ago
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 th
18.
by aweinstock 10y ago
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&#x2F
19.
by aweinstock 10y ago
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;
20.
by aweinstock 10y ago
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 st
21.
by aweinstock 10y ago
This is fairly readable (high-level) post on word embeddings: http://colah.github.io/posts/2014-07-NLP-RNNs-Representation...
22.
by aweinstock 11y ago
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
23.
by aweinstock 11y ago
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 b