2022-05-05

F#+Fableでsource-mapがうまく読み込まれない

問題

F#+Fableで書かれたアプリケーションをデバッグしたい。しかし、source-mapがうまく読み込まれないか、マッピングはされるもののブラウザのデバッガにコンパイルされたJavascriptが元ソースであるF#の代わりに表示されてしまう。

解決策

webpackの設定で、source-map-loaderを使用するように変更する¹。指定していなければ、devtoolオプションもeval-source-mapなりsource-mapなり指定すること。

...
  devtool: "eval-source-map",
  module: {
    rules: [
+      {
+        test: /\.js$/,
+        enforce: "pre",
+        use: ["source-map-loader"],
+      },
        ...
    ],
  },
...

Felizのテンプレートではsource-map-loaderがしっかりdependecyに記述されている。だが、なぜか使われていない。↩

2021-07-11

Firestoreのセキュリティルールのユニットテストでハマったこと

Firestoreのセキュリティルールのテストを書こうとしたらいろいろハマったので殴り書き。

環境

Typescript+Jest+@firebase/rules-unit-testing

テストフレームワークとしてFirebaseのドキュメントで使われているmochaの代わりにJestを使っているが、今回の話には全く関係ない。

ハマりポイント

`@firebase/rules-unit-testing`のインポートにはワイルドカードを使う

正:

import * as firebase from "@firebase/rules-unit-testing";

誤:

import firebase from "@firebase/rules-unit-testing";

誤っているほうだと、app()やloadFirestoreRules()などテストに必要不可欠なメソッドが呼べない。しかも型エラーが出ないのでたちが悪い。

アサーションには`await`が必要

正:

it("some test", async () => {
  /* ... */
  await firebase.assertSucceeds(/* ... */);
});

誤:

it("some test", () => {
  /* ... */
  firebase.assertSucceeds(/* ... */);
});

誤っているほうだと常にテストがPASSしてしまう。

2020-11-26

開長方形はR^2の開集合であることの証明

Mathpediaの位相空間論0 命題 0.7で述べられている「境界を含まない長方形」がR²の開集合であることを証明する

証明

$U$を

U = \big\{ (x,y) \in \R^2 | a < x < b, c < y < d \big\}

と定める。

ここで、

\forall x \in U\ \exists r > 0\ \big[ B(x,r) \subset U \big]

を示す。

任意に$x=(x',y') \in U$と定める。ここで$r$を

r = \min \big\{ x'-a,b-x',y'-c,d-y' \big\}

とおく。

これを不等式で表すと、

r \le x'-a, r \le b-x', r \le y'-c, r \le d-y'

となる。変形して、

\tag{1} a \le x'-r, r+x' \le b, c \le y'-r, r+y' \le d

また、$p = (x_p,y_p) \in B(x,r)$をとると定義から

d(p,x) < r

となり、成分ごとに書くと

|x_p-x'| < r \\ |y_p-y'| < r

となる。

これを解くと、

x'-r < x_p < x'+r \\ y'-r < y_p < y'+r

$(1)$から、

a \le x'-r < x_p < x'+r \le b \\ c \le y'-r < y_p < y'+r \le d

よって

a < x_p < b \\ c < y_p < d

したがって、$p \in U$から$B(x,r) \subset U$

$\square$

2020-11-25

開球体を用いた連続性の言い換えを確認する

Mathpedia 位相空間論0の命題 0.5 (開球体を用いた連続性の言い換え) を確認する。

使う定義や命題の確認

<1> 部分集合の定義

$\forall a\in A \Big[ a\in B \Big]$であるとき$A \subset B$と書き、$A$は$B$の部分集合という。

<2> 開球体の定義（定義 0.4）

$x \in \R^n$と$r>0$に対し$\R^n$の部分集合$B(x,r)$を

B(x, r) = \{y \in \R^n | d(x,y) < r\}

と定める。$B(x,r)$を$x$を中心とした半径$r$の開球体と呼ぶ。

<3> 連続の定義（定義 0.4中で述べられているもの）

写像$f: \R^n \to \R^m $が点$a \in \R^n$において連続であるとは

\forall \varepsilon>0 \exist \delta>0 \forall x\in\R^n \Big[ d_{\R^n}(x,a) < \delta \implies d_{\R^m}(f(x),f(a)) < \varepsilon \Big]

を満たすことである。ここで任意の点$a \in \R^n$においてこれを満たすとき、写像$f: \R^n \to \R^m $は連続であると呼ぶ

<4> 開球体を用いた連続性の言い換え（命題 0.5）

写像$f: \R^n \to \R^m $が点$a \in \R^n$において連続であるとは

\forall \varepsilon>0 \exist \delta>0 \Big[ f(B_{\R^n}(a, \delta) \subset B_{\R^m}(f(a), \varepsilon)) \Big]

を満たすことである。

実際に確認する

<3>$ \implies $<4>

$ f(b) \in f(B_{\R^n}(a, \delta)) $をとる。 $B_{\R^n}(a, \delta)$の定義から$b$は

d_{\R^n}(b,a) < \delta

を満たす。また、<3>から

d_{\R^m}(f(b),f(a)) < \varepsilon

である。

したがって$B_{\R^m}(f(a), \varepsilon)$の定義から$f(b) \in B_{\R^m}(f(a), \varepsilon)$が導かれ、

\forall f(b) \in f(B\_{\R^n}(a, \delta)) \Big[ f(b) \in B\_{\R^m}(f(a), \varepsilon) \Big]

となる。

□

<4>$ \implies $<3>

$ f(b) \in f(B_{\R^n}(a, \delta)) $をとる。 <4>から、$f(b) \in B_{\R^m}(f(a), \varepsilon)$である。

$B_{\R^m}(f(a), \varepsilon)$の定義から、

d_{\R^m}(f(b),f(a)) < \varepsilon

□

2020-11-18

Isabelle prog-proveのExercise 2.4の解答

ハマったのでメモ

問題

Exercise 2.4 Define a recursive function snoc :: 'a list => 'a => 'a list that appends an element to the end of a list. With the help of snoc define a recursive function reverse :: 'a list => 'a list that reverses a list. Prove reverse (reverse xs) = xs

reverse関数をappend無しで定義しよう、という問題。

snocの定義

ハマりどころその1。snoc xs aをx1 # x2 # ... # xn # [a]に展開していくイメージで書く。

fun snoc :: "'a list => 'a => 'a list" where
"snoc [] a = [a]" |
"snoc (x # xs) a = x # (snoc xs a)"

reverseの定義

こちらは簡単。

fun reverse :: "'a list => 'a list" where
"reverse [] = []" |
"reverse (x # xs) = snoc (reverse xs) x"

`reverse (reverse xs) = xs`の証明

2つ目のハマりどころにして一番難しいところ。素直にinductionからのautoのコンボを使ってみる:

theorem rev_rev: "reverse (reverse xs) = xs"
  apply(induction xs)
  apply(auto)
done

これは数学的帰納法の2つ目の証明が失敗してしまう。という訳でここに補題を付け加えるわけだが、それを見つけるのが難しい。

以下のような補題を上の証明の前に入れる:

lemma snoc_rev_sim [simp]: "reverse (snoc xs x) = x # (reverse xs)"
  apply(induction xs)
  apply(auto)
done

この命題はConsとsnocの対称性を表している。 Consを#、snocを*と書いてみると分かりやすい:

reverse (x # xs) = (reverse xs) * x （reverseの定義）
reverse (xs * x) = x # (reverse xs) （さっき証明した補題）

こうしてみるとConsとsnocは項の順番を置き換えることで交換できることがわかる。

2020-10-29

SQLインジェクション: Natas 14 Writeup

リンク: OverTheWire Natas14

TL;DR

簡単なSQLインジェクションの問題

問題の確認

OverTheWireのWeb系問題集であるNatasの第14問。phpで記述されていて、下のView Sourceというリンクからphpのソースコードを見ることができる。

f:id:Asakaze:20201029191428j:plain

IDとパスワードのテキストボックスが並ぶ典型的なログイン画面。入力後にボタンを押すとログイン可否が表示される。

Exploit

ソースコードからこの問題を解くにあたって大事なところを抜粋する：

$query = "SELECT * from users where username=\"".$_REQUEST["username"]."\" and password=\"".$_REQUEST["password"]."\"";

このコードから、ユーザーの認証に使うクエリを文字列の結合で生成していることがわかる。よって、SQLインジェクションを使うことができる。

例えば、IDに以下の通り書けばよい（パスワードは適当でOK）。

" OR 1=1;#

このように書くと、生成されるクエリは以下のようになる。

SELECT * from users where username="" OR 1=1;# and password="pass";

1=1は常に成立するため、このクエリはすべてのアカウントにひっかかる。1つでもクエリからアカウントが出た場合ログインできる仕様のため、これでめでたくログインしflagを獲得できる。

問題

解決策

環境