Skip to content

Instantly share code, notes, and snippets.

View yamarten's full-sized avatar

yamarten

4 followers · 1 following
View GitHub Profile
@yamarten
yamarten / overload.v
Last active March 17, 2019 06:56
Coqでアドホック多相
(* Coqでアドホック多相 *)
(* Coqで多引数の型クラスを用いた多相関数のサンプル *)
(* 型クラスに性質(定理)が書けるのもCoqらしさではあるが、その辺は他所でも紹介されているので割愛 *)
(* そういった機能については例えば: http://yosh.hateblo.jp/entry/20090904/p1 *)
(* 角括弧でのリスト記法が使いたかっただけなので、コンストラクタ直書きならImport不要 *)
Require Import List.
Import List.ListNotations.
(* 型クラス定義 ここでは関数を一つ持っているだけなので単に多相関数定義と思ってもいい *)
@yamarten
yamarten / packages.asc
Last active September 20, 2019 01:44
Atomの各種機能

逆引きAtom

逆引きAtom

新世代のemacsを目指して作られた[1]エディタAtom。「emacsは環境」という言葉もあるように多機能なemacsに対し、Atomはどんな機能があるのかまとめてみた。「こんなこともできるよ」と「これオススメだよ」と「これよく探されるよ」がごっちゃになってるので、実用性はあんまり無い。特にエディタっぽい機能を求めている場合は他を参照のこと。

1. http://careerhack.en-japan.com/report/detail/580
@yamarten
yamarten / livelits.asc
Last active December 1, 2019 12:59
livelits紹介

Livelits: Filling Typed Holes with Live GUIs

Table of Contents

研究概要

やったこと

以下の2つの研究を1つに合体した

  • GUIで値を入力できるプログラミング環境

@yamarten
yamarten / firequix.jxa
Last active August 11, 2020 05:56
MacのFirefox用ブックマークレットランチャ
/*
firequix.jxa
bookmarklet organizer for Firefox with BetterTouchTool inspired by quixapp.com
*/
'use strict'
function run(argv) {
// Please create bookmark to "javascript:%s" and set keyword.
const keyword = 'javascript'
@yamarten
yamarten / yt_time.user.js
Created June 1, 2022 01:47
YouTubeの動画投稿・配信開始日時を表示
// ==UserScript==
// @name YouTube DateTime
// @match https://www.youtube.com/watch*
// @grant none
// @version 1.0.0
// @description Replace info with absolute datetime
// @description:ja YouTubeの動画投稿・配信開始日時を表示
// ==/UserScript==
(() => {
@yamarten
yamarten / atproto_signing.asc
Created March 26, 2023 05:18
ATPの署名の話

atprotoの署名は何を保証するか

atprotoではrepositoryに対して署名を行うが、これによって何が嬉しいのかを考える。

【結論】 大事なrecordを提示する時は署名も示す文化が根付けばメリットはあるが、周知されなければ署名し損 [1]

おさらい

とりあえず以下の2つの仮定をおく。これはかなり強い仮定なのでその影響は別途検討する必要がある。

1. 当然のことを言っているだけのような気もする……
@yamarten
yamarten / plc_verify.asc
Created July 29, 2023 11:05
PLCの検証の話

did:plcは何を保証するか

did:plcの仕組みについては良い解説記事があるのでそちらを参照。より詳細な話は公式READMEへ。 これらに対する補足程度に、「なぜこのような仕組みを採っているか」についてメモしておく。

operation log

PLCサーバーはDID毎に全てのoperationを保持しており、外部に提供する。これは単に履歴が追えるとか帳簿をつけているとかいうだけの話ではなく、もっと厳密な検証ができる。

operationはrotation keyの持ち主(通常はPDS)が発行するもので、主に直前のoperationのハッシュとPLCサーバーに対する操作、およびそれに対するrotation keyによる署名が含まれている。rotation keyの公開鍵の登録や変更もoperationによって行うため、operation logを辿っていけば各署名の検証に使うべき鍵も分かる。各operationの署名を検証することでoperationの正当性を、ハッシュを検証することでoperationの連続性を確認できる。

@yamarten
yamarten / atoroto_handle.asc
Created August 15, 2023 07:31
atprotoハンドルアンチ論

ハンドルアンチの主張

ハンドルアンチを名乗っている割にあんまり具体的な話をしていなかった気がするので、ハンドルという機能が持つ課題を一旦まとめておく。正直に言えば、一時期カスタムハンドルがアカウントの検証手段として過剰に期待されていたことに対する逆張りの気持ちも大いにあるが、それは別として現状のハンドルに対する問題意識を明文化したい。

念の為書いておくと、atprotoの現状理解を整理する一貫として書いているのであって、これらの問題を解決するような仕様変更を求めるつもりはない。

PDSがハンドルを提供しないといけない

あると嬉しいし、PDS的にもあまりコストがかからないのではないかと思うが、必須にはしたくないという話。

@yamarten
yamarten / atproto_aniv.asc
Created October 18, 2023 10:20
atprotoの1年間の話

atprotoがやったこと/やっていないこと

10月18日。experimentだったADXが「Authenticated Transfer Protocol」に名を変え正式発表して早一年。特にBlueskySocialが活発に動き出してからのatprotoは色々と変わったことや分かったことがあったので、まとめてみる。

とはいっても「何ができるか」はきっと各所で解説されているので、「何ができていないか」「何をしなくなったか」にフォーカスして、一周年記念らしからぬネガティブな話をする。一年間の道程の概略は本人達がまとめているので、そちらを参照されたい。

解説というより覚書のようなものなので、ある程度プロトコルの中身を知ってる前提。ユーザ視点では「ベータ開始当初の目標は一部未達成で、まだちゃんとベータ」「来年頭に連合開始予定」くらいの認識で良いと思う。

やろうとしていたこと

@yamarten
yamarten / coq_tools.asc
Last active November 13, 2023 23:02
Coq関連プログラムリンク集
Table of Contents

目についたCoqのライブラリ/プラグイン/開発環境などの覚え書き

実用面は気にせず、研究用や無メンテも載せる

ライブラリ

Coqソースファイルのみで構成されるもの