Compiler and Checker Demonstration
This page gives a demonstration about how the compiler and the checker works, using the example trust schema. Please refer to Implementation Details for implementation details.
LVS schema input and parsing
We assume the following LVS schema:
#KEY: "KEY"/_/_/_
#site: "lvs-test"
#article: #site/"article"/author/post/_version & {_version: $eq_type("v=0")} <= #author
#author: #site/"author"/author/"KEY"/_/admin/_ <= #admin
#admin: #site/"admin"/admin/#KEY <= #root
#root: #site/#KEY
We ignore the parsing details since this is handled by Lark.
Sorting rules
The original schema has the following dependencies among the rules:
(1) #KEY: "KEY"/_/_/_
(2) #site: "lvs-test"
(3) #article: #site/"article"/author/post/_version & {_version: $eq_type("v=0")} <= #author
--> (2) (4)
(4) #author: #site/"author"/author/"KEY"/_/admin/_ <= #admin
--> (2) (5)
(5) #admin: #site/"admin"/admin/#KEY <= #root
--> (1) (2) (6)
(6) #root: #site/#KEY
--> (1) (2)
Topological sorting gives us:
(3) #article: #site/"article"/author/post/_version & {_version: $eq_type("v=0")} <= #author
--> (2) (4)
(4) #author: #site/"author"/author/"KEY"/_/admin/_ <= #admin
--> (2) (5)
(5) #admin: #site/"admin"/admin/#KEY <= #root
--> (1) (2) (6)
(6) #root: #site/#KEY
--> (1) (2)
(1) #KEY: "KEY"/_/_/_
(2) #site: "lvs-test"
Generating pattern ID
#site/”article”/1/2/-1 & {-1: $eq_type(“v=0”)} <= #author #author: #site/”author”/1/”KEY”/-2/3/-3 <= #admin #admin: #site/”admin”/3/#KEY <= #root #root: #site/#KEY #KEY: “KEY”/-4/-5/-6 #site: “lvs-test”
Replicating rules
In this schema, we don’t have have multiple constraint sets like /a/b & {a: "a"} | {b: "b"}
.
Therefore, no rule replication is needed.
Generating tree
Each node is a name prefix, and edge becoming the condition to
Fixing signing constraints
After constructing the tree, the compilier fill in the symbol table for non-temporary symbols:
1: author
2: post
3: admin
and model the name pattern tree into a TLV encodable model.
Checker
In order to check a name /lvs-test/article/alice/post1/v=2
can be signed by
name /lvs-test/author/alice/KEY/%BDA%D6%DE%EA%09%3C%E0/admin/v=1647807153833
,
Checker first matches /lvs-test/article/alice/post1/v=2
against the name
pattern tree, which gives the uppermost branch of the pattern tree.
Along the matching, checker fills the symbols with author = "alice"
and post = "post1"
.
The end of this branch indicates the node identifier (e.g., x
) for this branch.
Then the checker matches the /lvs-test/author/alice/KEY/...
against the name pattern tree, which gives the second branch from the top.
When matching along this branch, checker uses “alice” for 1
’s value.
The end of this branch has the same node identifier x
, thereby the checking succeeds.