Update

penglei · May 22, 2021 · 595e718 · 595e718
1 parent d9cd074
commit 595e718
Show file tree

Hide file tree

Showing 8 changed files with 141 additions and 16 deletions.
diff --git a/content/post/isabelle-note1/index.adoc 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来提供的。
+
+//<!--more-->
+
+== 基础
+
+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
@@ -0,0 +1,12 @@
+<div class="paragraph">
+  <p>xxxabc111</p>
+</div>
+
+<div class="paragraph">
+  <p>HUGOMORE42</p>
+</div>
+
+<div style="text-align: center">
+  <canvas style="border: 1px solid black; direction: ltr;" id="pdf-content" value="main.pdf"></canvas>
+</div>
+
diff --git a/hugo-asciidoctor-render/a2.html b/hugo-asciidoctor-render/a2.html
@@ -0,0 +1,8 @@
+<div class="paragraph">
+ <p>HUGOMORE42</p>
+</div>
+
+<div style="text-align: center">
+<canvas style="border: 1px solid black; direction: ltr;" id="pdf-content" value="main.pdf"></canvas>
+</div>
+
diff --git a/hugo-asciidoctor-render/b1.html b/hugo-asciidoctor-render/b1.html
@@ -0,0 +1,20 @@
+<div id="preamble">
+  <div class="sectionbody">
+    <div class="paragraph">
+     <p>xxxabc111</p>
+   </div>
+   <div class="paragraph">
+    <p>HUGOMORE42</p>
+   </div>
+  </div>
+</div>
+
+<div class="sect1">
+  <h2 id="_content"><a class="anchor" href="#_content"></a><a class="link" href="#_content">Content</a></h2>
+  <div class="sectionbody">
+   <div style="text-align: center">
+    <canvas style="border: 1px solid black; direction: ltr;" id="pdf-content" value="main.pdf"></canvas>
+   </div>
+  </div>
+</div>
+
diff --git a/hugo-asciidoctor-render/b2.html b/hugo-asciidoctor-render/b2.html
@@ -0,0 +1,19 @@
+<div id="preamble">
+  <div class="sectionbody">
+    <div class="paragraph">
+      <p>HUGOMORE42</p>
+    </div>
+  </div>
+</div>
+
+<div class="sect1">
+  <h2 id="_content"><a class="anchor" href="#_content"></a><a class="link" href="#_content">Content</a></h2>
+  <div class="sectionbody">
+   <div style="text-align: center">
+    <canvas style="border: 1px solid black; direction: ltr;" id="pdf-content" value="main.pdf"></canvas>
+   </div>
+  </div>
+</div>
+
+
+
diff --git a/hugo-asciidoctor-render/no-explicit-summary-with-content.html b/hugo-asciidoctor-render/no-explicit-summary-with-content.html
@@ -0,0 +1,13 @@
+<div class="paragraph">
+  <p>xxxabc111</p>
+</div>
+
+<div class="paragraph">
+  <p>HUGOMORE42</p>
+</div>
+
+<div style="text-align: center">
+  <canvas style="border: 1px solid black; direction: ltr;" id="pdf-content" value="main.pdf"></canvas>
+</div>
+
+
diff --git a/hugo-asciidoctor-render/preamble-has-content.html b/hugo-asciidoctor-render/preamble-has-content.html
@@ -0,0 +1,20 @@
+<div id="preamble">
+  <div class="sectionbody">
+    <div class="paragraph">
+     <p>xxxabc111</p>
+   </div>
+   <div class="paragraph">
+    <p>HUGOMORE42</p>
+   </div>
+  </div>
+</div>
+
+<div class="sect1">
+  <h2 id="_content"><a class="anchor" href="#_content"></a><a class="link" href="#_content">Content</a></h2>
+  <div class="sectionbody">
+   <div style="text-align: center">
+    <canvas style="border: 1px solid black; direction: ltr;" id="pdf-content" value="main.pdf"></canvas>
+   </div>
+  </div>
+</div>
+
diff --git a/post/transparent_proxy_on_macosx/index.html b/post/transparent_proxy_on_macosx/index.html
@@ -76,7 +76,7 @@
 ">
 <meta itemprop="datePublished" content="2019-02-17T00:00:00&#43;00:00" />
 <meta itemprop="dateModified" content="2019-02-17T00:00:00&#43;00:00" />
-<meta itemprop="wordCount" content="2651">
+<meta itemprop="wordCount" content="2718">
 
 
 
@@ -335,19 +335,23 @@ <h2 id="architecture"><a class="anchor" href="#architecture"></a><a class="link"
 </div>
 <div class="listingblock">
 <div class="content">
-<pre class="nowrap">..............................macOS..............................
-.                                                               .
-. +----------+                                                  .
-. |   APP    |                                                  .
-. +----------+                                                  .
-.      | eg: 1.2.3.4            pf rdr-to  +------------------+ .  +---------------+
-.      |                      +-----------&gt;| transprant proxy +---&gt;| socks5 server +---&gt;outside world
-.      v                      |            +------------------+ .  +---------------+    (eg: 1.2.3.4)
-.  +----+--+               +--+--+         127.0.0.1:12345      .
-.  |  en0  +--------------&gt;| lo0 |                              .
-.  +-------+  pf route-to  +-----+                              .
-.                                                               .
-.................................................................</pre>
+<pre class="nowrap">.........................macOS............................
+.                (userspace)                             .
+.                                 127.0.0.1:12345        .
+. +----------+                  +------------------+     .  +---------------+
+. |   APP    |                  | transprant proxy +-------&gt;| socks5 server +---&gt;outside world
+. +----------+                  +------------------+     .  +---------------+    (eg: 1.2.3.4)
+.      | eg: 1.2.3.4                      ^              .
++======|==================================|===============
+.      |        (kernel space)            |              .
+.      |                        pf rdr    |              .
+.      |                      +-----------+              .
+.      v                      |                          .
+.  +----+--+               +--+--+                       .
+.  |  en0  +--------------&gt;| lo0 |                       .
+.  +-------+  pf route-to  +-----+                       .
+.                                                        .
+..........................................................</pre>
 </div>
 </div>
 <div class="paragraph">
@@ -366,10 +370,10 @@ <h2 id="architecture"><a class="anchor" href="#architecture"></a><a class="link"
 <div class="ulist">
 <ul>
 <li>
-<p>第二条规则 <strong>route-to</strong> 表示将本地任何地址访问1.2.3.4的TCP流量路由到另一个地址；</p>
+<p>第一条规则 <strong>rdr</strong> 表示将进入lo0、协议为TCP、任何来源、目的地址是1.2.3.4的流量转发到 <code>127.0.0.01:12456</code> ；</p>
 </li>
 <li>
-<p>第一条规则 <strong>rdr-to</strong> 表示将进入lo0接口上的流量转发到另一个地址；</p>
+<p>第二条规则 <strong>route-to</strong> 表示将从本地任何地址(一台设备可能有多个IP地址)访问1.2.3.4的TCP流量路由到另一个地址(这里是lo0 127.0.0.1)；</p>
 </li>
 </ul>
 </div>