From 595e71800dc7677a4c21ad8573f3c794cf22afe2 Mon Sep 17 00:00:00 2001 From: penglei Date: Sat, 22 May 2021 16:50:55 +0800 Subject: [PATCH] Update --- content/post/isabelle-note1/index.adoc | 29 +++++++++++++++ hugo-asciidoctor-render/a1.html | 12 +++++++ hugo-asciidoctor-render/a2.html | 8 +++++ hugo-asciidoctor-render/b1.html | 20 +++++++++++ hugo-asciidoctor-render/b2.html | 19 ++++++++++ .../no-explicit-summary-with-content.html | 13 +++++++ .../preamble-has-content.html | 20 +++++++++++ post/transparent_proxy_on_macosx/index.html | 36 ++++++++++--------- 8 files changed, 141 insertions(+), 16 deletions(-) create mode 100644 content/post/isabelle-note1/index.adoc create mode 100644 hugo-asciidoctor-render/a1.html create mode 100644 hugo-asciidoctor-render/a2.html create mode 100644 hugo-asciidoctor-render/b1.html create mode 100644 hugo-asciidoctor-render/b2.html create mode 100644 hugo-asciidoctor-render/no-explicit-summary-with-content.html create mode 100644 hugo-asciidoctor-render/preamble-has-content.html diff --git a/content/post/isabelle-note1/index.adoc b/content/post/isabelle-note1/index.adoc new file mode 100644 index 0000000..ea5142b --- /dev/null +++ b/content/post/isabelle-note1/index.adoc @@ -0,0 +1,29 @@ +//// +title: Isabelle笔记（一） +date: 2021-04-30T09:00:00+08:00 + +draft: true +categories: [Formal] +tags: [Isabelle, Proof Assistant] +//// + += Isabelle笔记（一） +// Disable wrapping in listing and literal blocks. +:prewrap!: +:toc: +:sectanchors: +:sectlinks: +:icons: font + +Isabelle是一个实现形式逻辑的通用系统，其中Isabelle/HOL是Isabelle处理高阶逻辑的特化系统。 +HOL 是 `Higher-Order Logic` 的简写。 具体地，在Isabelle中，HOL是通过组合 Function Programming和Logic来提供的。 + +// + +== 基础 + +Isabelle底层使用ML语言实现，其语法也受到ML的影响。Isabelle/Isar是Isabelle的一个扩展，几乎隐藏了所有底层实现语言的细节。 +因此，Isabelle/HOL的完整简写应该是 Isabelle/Isar/HOL。 + +使用Isabelle是以理论(`theory`)为中心， `theory` 由具名的 `type` 、 `function` 、 `theorem` 列表构成。 + diff --git a/hugo-asciidoctor-render/a1.html b/hugo-asciidoctor-render/a1.html new file mode 100644 index 0000000..d11cd27 --- /dev/null +++ b/hugo-asciidoctor-render/a1.html @@ -0,0 +1,12 @@ +
+

xxxabc111

+
+ +
+

HUGOMORE42

+
+ +
+ +
+ diff --git a/hugo-asciidoctor-render/a2.html b/hugo-asciidoctor-render/a2.html new file mode 100644 index 0000000..e2e4fcf --- /dev/null +++ b/hugo-asciidoctor-render/a2.html @@ -0,0 +1,8 @@ +
+

HUGOMORE42

+
+ +
+ +
+ diff --git a/hugo-asciidoctor-render/b1.html b/hugo-asciidoctor-render/b1.html new file mode 100644 index 0000000..6718a30 --- /dev/null +++ b/hugo-asciidoctor-render/b1.html @@ -0,0 +1,20 @@ +
+
+
+

xxxabc111

+
+
+

HUGOMORE42

+
+
+
+ +
+

Content

+
+
+ +
+
+
+ diff --git a/hugo-asciidoctor-render/b2.html b/hugo-asciidoctor-render/b2.html new file mode 100644 index 0000000..21213a5 --- /dev/null +++ b/hugo-asciidoctor-render/b2.html @@ -0,0 +1,19 @@ +
+
+
+

HUGOMORE42

+
+
+
+ +
+

Content

+
+
+ +
+
+
+ + + diff --git a/hugo-asciidoctor-render/no-explicit-summary-with-content.html b/hugo-asciidoctor-render/no-explicit-summary-with-content.html new file mode 100644 index 0000000..9f5caf3 --- /dev/null +++ b/hugo-asciidoctor-render/no-explicit-summary-with-content.html @@ -0,0 +1,13 @@ +
+

xxxabc111

+
+ +
+

HUGOMORE42

+
+ +
+ +
+ + diff --git a/hugo-asciidoctor-render/preamble-has-content.html b/hugo-asciidoctor-render/preamble-has-content.html new file mode 100644 index 0000000..6718a30 --- /dev/null +++ b/hugo-asciidoctor-render/preamble-has-content.html @@ -0,0 +1,20 @@ +
+
+
+

xxxabc111

+
+
+

HUGOMORE42

+
+
+
+ +
+

Content

+
+
+ +
+
+
+ diff --git a/post/transparent_proxy_on_macosx/index.html b/post/transparent_proxy_on_macosx/index.html index cdde4fc..f7da952 100644 --- a/post/transparent_proxy_on_macosx/index.html +++ b/post/transparent_proxy_on_macosx/index.html @@ -76,7 +76,7 @@ "> - + @@ -335,19 +335,23 @@

-
..............................macOS..............................
-.                                                               .
-. +----------+                                                  .
-. |   APP    |                                                  .
-. +----------+                                                  .
-.      | eg: 1.2.3.4            pf rdr-to  +------------------+ .  +---------------+
-.      |                      +----------->| transprant proxy +--->| socks5 server +--->outside world
-.      v                      |            +------------------+ .  +---------------+    (eg: 1.2.3.4)
-.  +----+--+               +--+--+         127.0.0.1:12345      .
-.  |  en0  +-------------->| lo0 |                              .
-.  +-------+  pf route-to  +-----+                              .
-.                                                               .
-.................................................................
+
.........................macOS............................
+.                (userspace)                             .
+.                                 127.0.0.1:12345        .
+. +----------+                  +------------------+     .  +---------------+
+. |   APP    |                  | transprant proxy +------->| socks5 server +--->outside world
+. +----------+                  +------------------+     .  +---------------+    (eg: 1.2.3.4)
+.      | eg: 1.2.3.4                      ^              .
++======|==================================|===============
+.      |        (kernel space)            |              .
+.      |                        pf rdr    |              .
+.      |                      +-----------+              .
+.      v                      |                          .
+.  +----+--+               +--+--+                       .
+.  |  en0  +-------------->| lo0 |                       .
+.  +-------+  pf route-to  +-----+                       .
+.                                                        .
+..........................................................
@@ -366,10 +370,10 @@

  • -

    第二条规则 route-to 表示将本地任何地址访问1.2.3.4的TCP流量路由到另一个地址；

    +

    第一条规则 rdr 表示将进入lo0、协议为TCP、任何来源、目的地址是1.2.3.4的流量转发到 127.0.0.01:12456 ；

  • -

    第一条规则 rdr-to 表示将进入lo0接口上的流量转发到另一个地址；

    +

    第二条规则 route-to 表示将从本地任何地址(一台设备可能有多个IP地址)访问1.2.3.4的TCP流量路由到另一个地址(这里是lo0 127.0.0.1)；