Cleanup

README.md

@@ -16,7 +16,7 @@ For support and discussions, please visit our [Zulip forum](https://zulip.argume
 
 # Overview
 
-Lurk is a statically scoped dialect of Lisp, influenced by Scheme and Common Lisp. A reference implementation focused on describing and developing the core language can be found in the [`lurk`](https://github.com/argumentcomputer/lurk-lisp) repo.
+Lurk is a statically scoped dialect of Lisp, influenced by Scheme and Common Lisp. A reference implementation focused on describing and developing the core language can be found in the [`lurk-lisp`](https://github.com/argumentcomputer/lurk-lisp) repo.
 
 Lurk's distinguishing feature relative to most programming languages is that correct execution of Lurk programs can be directly proved using zk-SNARKs. The resulting proofs are succinct: they are relatively small, can be verified quickly, and they reveal only the information explicitly contained in the statement to be proved.
 
@@ -29,7 +29,7 @@ Lurk's distinguishing feature relative to most zk-SNARK authoring languages is t
 Integration with backend proving systems and tooling for proof generation are both still very early. Performance and user experience still have room for significant optimization and improvement, but simple examples can be found in the [demo example directory](demo/).
 
 # Backends
-- Nova is Lurk's officially-supported IVC backend. It uses Argument Computer Corporation's Arecibo fork of the [Nova proving system](https://github.com/argumentcomputer/arecibo) and the Pasta Curves.
+- Nova is Lurk's officially-supported IVC backend. It uses Argument's Arecibo fork of the [Nova proving system](https://github.com/argumentcomputer/arecibo) and the Pasta Curves.
 - SuperNova is Lurk's in-development NIVC backend. It uses Arecibo's [SuperNova extension to the Nova proving system](https://github.com/argumentcomputer/arecibo/tree/dev/src/supernova) and the Pasta Curves.
 - Future work may target Halo2 or other proving systems.
 

benches/sha256.rs

@@ -378,7 +378,7 @@ cfg_if::cfg_if! {
             targets =
                 nivc_prove_benchmarks
                 // TODO: Add when compressed SNARK is implemented for SuperNova
-                // https://github.com/argumentcomputer/arecibo/issues/27https://github.com/argumentcomputer/arecibo/issues/27
+                // https://github.com/argumentcomputer/arecibo/issues/27
                 // nivc_prove_compressed_benchmarks
          }
     } else {
@@ -399,7 +399,7 @@ cfg_if::cfg_if! {
              targets =
                  nivc_prove_benchmarks
                  // TODO: Add when compressed SNARK is implemented for SuperNova
-                 // https://github.com/argumentcomputer/arecibo/issues/27https://github.com/argumentcomputer/arecibo/issues/27
+                 // https://github.com/argumentcomputer/arecibo/issues/27
                  // nivc_prove_compressed_benchmarks
           }
     }

notes/reduction-notes.md

@@ -3,7 +3,7 @@
 This document contains general notes about the design, rationale, and implementation of the Lurk reduction step. For a
 more normalized (but still WIP) specification, see the [Eval Spec](eval.md)
 
-The [Lurk Language Specification](https://github.com/argumentcomputer/lurk/blob/master/spec/v0-1.md) defines evaluation
+The [Lurk Language Specification](https://github.com/argumentcomputer/lurk-lisp/blob/master/spec/v0-1.md) defines evaluation
 semantics without specifying the internal data structures or computational steps which an implementation must use to
 calculate an evaluation. `lurk-rs` implements a concrete instance of the Lurk language for which proofs of correct
 evaluation can be generated. `lurk-rs` generates zk-SNARK proofs for multiple backends, and verification of these
@@ -44,7 +44,7 @@ Taking these one at a time:
 
 
 As a matter of interest, we note that the `lurk-rs` evaluator runs about 7x faster than the one implemented in [Common
-Lisp](https://github.com/argumentcomputer/lurk/blob/master/api/api.lisp). The latter's design does not target speed, and we
+Lisp](https://github.com/argumentcomputer/lurk-lisp/blob/master/api/api.lisp). The latter's design does not target speed, and we
 make this observation only to support our suggestion that the `lurk-rs` evaluator performs well relative to the cost of
 proving. It makes sense to evaluate many frames at a time before proving because doing so is cheap.
 

notes/soundness-notes.md

@@ -4,7 +4,7 @@
 This document contains general notes about the soundness of Lurk proofs.
 
 We choose a somewhat elaborate functional commitment code example (lightly modified from [A Programmer's Introduction to
-Lurk](https://blog.lurk-lang.org/posts/prog-intro/)) because it exercises many language features.
+Lurk](https://argument.xyz/blog/prog-intro/)) because it exercises many language features.
 
 ```
 > (letrec ((reduce (lambda (acc f list)