website: fix urls and a typo

Author: Philipp15b

README.md

@@ -12,9 +12,9 @@ Do not hesitate to open an issue or send an email to [email protected] wi
 I am also happy to discuss anything via Zoom as well!
 
 **The documentation is available at [www.caesarverifier.org](https://www.caesarverifier.org).**
-Start at with the [introduction](https://www.caesarverifier.org), then walk through the [quick start guide](https://www.caesarverifier.org/quickstart.html).
+Start at with the [introduction](https://www.caesarverifier.org/docs/), then walk through the [getting started guide](https://www.caesarverifier.org/docs/getting-started/).
 
 We have an OOPSLA 2023 paper on Caesar and its theory: [_A Deductive Verification Infrastructure for Probabilistic Programs_](https://doi.org/10.1145/3622870).
 You can [find the preprint on arxiv](https://arxiv.org/abs/2309.07781).
 
-There is also a [development guide](https://www.caesarverifier.org/devguide.html) if you want to work on Caesar itself.
+There is also a [development guide](https://www.caesarverifier.org/docs/devguide) if you want to work on Caesar itself.

website/docs/proof-rules/unrolling.md

@@ -37,13 +37,13 @@ This means we know that if verification of an upper bound *fails*, then it canno
 On the other hand, if verification succeeds, then we know nothing!
 
 ```heyvl
-coproc geo1_bmc(init_c: UInt) -> (c: UInt)
+coproc geo1_unroll(init_c: UInt) -> (c: UInt)
     pre init_c + 0.99
     post c
 {
     c = init_c
     var cont: Bool = true
-    @bmc(12, 0) // k = 12, terminator = 0
+    @unroll(12, 0) // k = 12, terminator = 0
     while cont {
         var prob_choice: Bool = flip(0.5)
         if prob_choice { cont = false } else { c = c + 1 }
@@ -64,7 +64,7 @@ if cont {
 }
 ```
 
-Trying to verify `geo1_bmc` will yield a counter-example to verification.
+Trying to verify `geo1_unroll` will yield a counter-example to verification.
 Because this is loop unrolling, it is a *true counter-example* to `init_c + 0.99` being an upper bound.
 On the other hand, if you change `k = 11`, then the program verifies.
 But this tells you nothing about the actual program semantics.

website/docusaurus.config.js

@@ -11,7 +11,7 @@ const config = {
   favicon: 'img/laurel.svg',
 
   // Set the production url of your site here
-  url: 'https://caesarverifier.org',
+  url: 'https://www.caesarverifier.org',
   // Set the /<baseUrl>/ pathname under which your site is served
   // For GitHub pages deployment, it is often '/<projectName>/'
   baseUrl: '/',