The engine chosen by MicroPython is vulnerable to catastrophic backtracking and switching to the Pike VM implementation would fix that. Instead of backtracking in the text when the pattern doesn't match, the Pike VM iterates each char in the text only once, visiting the states valid for that position in lock step. Consequently, it allocates a list of “thread”s, proportional in length to the number of states in the pattern (though usually patterns have relatively few states). Many security issues have resulted from regexp denials of service, so this slight memory tradeoff might be worthwhile.

Since recursiveloop.c has been changed by MicroPython, those changes would need to be ported to pike.c. The fixes are small and none of the extra features exploit the backtracking, so this should be easy.

[0]: https://github.com/micropython/micropython/tree/master/lib/r...

[1]: https://github.com/pfalcon/re1.5/tree/v0.8.2

[2]: https://swtch.com/~rsc/regexp/regexp2.html

[0]: https://github.com/thaliaarchi/ws-challenges

[1]: https://github.com/thaliaarchi/wsjq

> Excel 2.0 was released a month before Windows 2.0, and the installed base of Windows was so low at that point in 1987 that Microsoft had to bundle a runtime version of Windows 1.0 with Excel 2.0.

[0]: https://en.wikipedia.org/wiki/Microsoft_Excel

> I made a prototype and, lo and behold, it was in fact slow, as predicted. (I’m smart.)

And in another article[0], describing an inefficient collision algorithm:

> Mojang’s decision never crossed my mind. I guess I’m not a real programmer.

[0]: https://purplesyringa.moe/blog/ru/minecraft-compares-arrays-...

    #!/usr/bin/env bash
    set -eEuo pipefail

    # `git commit`, using the latest file modification time as the commit and author
    # dates, when GIT_AUTHOR_DATE or GIT_COMMITTER_DATE, respectively, is not set.

    # Use fractional seconds when available to display the newest file more
    # accurately, even though Git only uses seconds.
    if which gstat >/dev/null; then
      stat=(gstat --format='%.Y %n') # Detected aliased GNU coreutils
    elif stat --version 2>/dev/null | grep -q 'GNU coreutils'; then
      stat=(stat --format='%.Y %n') # Detected GNU coreutils
    else
      stat=(stat -f '%m %N') # Fallback to BSD-style, which only reports seconds
    fi

    # Select the latest modified time of all staged files, excluding deletions.
    modified="$(
      cd "$(git rev-parse --show-toplevel)" &&
      git diff --staged --diff-filter=d --name-only -z |
        xargs -0 "${stat[@]}" |
        sort -rn |
        head -1
    )"

    modified_seconds=
    if [[ -n $modified ]]; then
      modified_seconds="${modified%% *}"
      modified_file="${modified#* }"
      modified_date="$(date -r "${modified_seconds%.*}" +'%Y-%m-%d %H:%M:%S %z')"
      echo "Modify date: $modified_date ($modified_file)"
    fi
    author_seconds="$modified_seconds"
    committer_seconds="$modified_seconds"
    if [[ -n ${GIT_AUTHOR_DATE+.} ]]; then
      echo "Author date: ${GIT_AUTHOR_DATE:-now}"
    fi
    if [[ -n ${GIT_COMMITTER_DATE+.} ]]; then
      echo "Commit date: ${GIT_COMMITTER_DATE:-now}"
    else
      last_commit_seconds="$(git show -s --format=%at HEAD 2>/dev/null || echo 0)"
      if [[ $modified_seconds < $last_commit_seconds ]]; then
        committer_seconds=
        echo "Commit date: now (last commit: $(git show -s --format=%ai HEAD 2>/dev/null))"
      fi
    fi

    GIT_AUTHOR_DATE="${GIT_AUTHOR_DATE-"$author_seconds"}" \
    GIT_COMMITTER_DATE="${GIT_COMMITTER_DATE-"$committer_seconds"}" \
    exec git commit "$@"

It's interesting to read this early use of “bit”, before the term became commonplace. The first publication to use “bit”, also by Shannon, was only a year prior[0].

[0]: https://en.wikipedia.org/wiki/Bit#History

Comments URL: https://news.ycombinator.com/item?id=40409997

Points: 3

# Comments: 2

The process is: Compile mrustc with a C++ compiler. Compile rustc sources with untrusted rustc binary and compile rustc sourcs with mrustc (these have identical behavior, but different codegen). Compile rustc sources with rustc-by-rustc and compile rustc sources with rustc-by-mrustc (these will have identical behavior and codegen). Those will match. If you compile once more, they will match. Since mrustc is never compiled by rustc, such a backdoor would have to also exist in gcc/clang and propagate with exactly identical behavior in mrustc. The process could be repeated for gcc/clang.

Since we don't have a verified rustc (a la CompCert [0]), I wonder if an approach like the translation validation of seL4 [1] would work. They prove that the artifact (ARM machine code) produced by an existing compiler (gcc) for a chosen program (seL4) matches the source semantics (C). Thus you could circumvent trusting rustc, but it only works to verify a specific output of a chosen program. If the chosen program was coq-of-rust, I don't think this would be easier than the approach I detailed above. The seL4 kernel is 9,500 lines of C, while their Isabel/HOL specification is over 200,000 lines, so the technique doesn't seem to scale to a large chosen source like rustc.

Isn't bootstrapping fun?

[0]: Xavier Leroy. 2008. “Formal verification of a realistic compiler”. https://xavierleroy.org/publi/compcert-CACM.pdf

[1]: Thomas Sewell, Magnus Myreen, and Gerwin Klein. PLDI 2013. “Translation Validation for a Verified OS Kernel”. https://sci-hub.st/10.1145/2491956.2462183

Automatic translation like this shifts the trust to the tool. coq-of-rust itself is written in Rust, not in Coq. The recursive nature is somewhat boggling, but I think a proof of its correctness is possible in a similar process to David A. Wheeler's “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] (which circumvents Ken Thompson's Trusting Trusting attack by using a second compiler), but with a mix of a CompCert approach.

To verify it, you'd use coq-of-rust to convert the coq-of-rust translator from Rust to Coq. That translation is not trusted, because it was performed in Rust, but it doesn't matter. Once in Coq, you prove the desired correctness properties—crucially, that it preserves the semantics of the Rust program when it translates a program to Coq.

As in the article, it is likely easier to work with more functional definitions in proofs instead of generated ones, so you'd undertake the same process as they do with the stdlib of proving equivalence between definitions. Since the current line count for the coq-of-rust translator (specifically, lib/ [1]) is 6350 lines of Rust, it even seems feasible to write a full translator in Coq and prove its equivalence to the generated one.

Then, you execute the proven-correct Coq coq-of-rust translator on the Rust source of the coq-of-rust translator. The Coq definitions it outputs should match the output of the Rust coq-of-rust translator that you started with.

As an aside, it's nice to see industry funding for work like this. I'm often cynical of cryptocurrency, but its correctness constraints really push for improvements in areas I like (Rust, Coq, funding for masters students I know, etc.).

[0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf

[1]: https://github.com/formal-land/coq-of-rust/tree/main/lib