[vishwa-raman]

No description provided.

[github-actions]

Documentation preview

The preview has been removed.

[johnnygreco]

@vishwa-raman I pushed 8cd2275 to this branch, which adds LaTeX math support to Dev Notes (MathJax, set up the way Zensical's Math guide recommends). Write inline math as \(...\) or $...$, and display math as \[...\] or $$...$$ on their own lines.

With that available, a few patterns would make the formal parts of the note easier to follow:

• Write variables as math, and use one name per concept. Policies are "A" and "B" in the intro but P₁ and P₂ in the Prover section, and line 67 also uses "A" for an agent and "B" for a job, right before the same letters mean policies. Using \(P_1\) and \(P_2\) for policies throughout (and \(a\) and \(j\) for the agent and job, or no letters at all) removes the ambiguity.
• Set named functions in italics with \mathit{}. \mathit{grants} and \mathit{allowed} keep the italic look the note already has, while making it clear these are functions and not prose.
• Give the key equation its own line. The definition of allowed(P) in terms of permit and forbid is the core idea of the Prover section and reads better as display math.
• Keep Cedar names in code formatting. permit, forbid, and NetworkConnect are Cedar syntax, so leaving them in backticks keeps them visually distinct from math.
• Use one notation throughout. Mixing LaTeX with Unicode subscripts and symbols (P₁, ⊆, ⇒) renders in two slightly different fonts, so it is worth converting all of them.

For example, the end of line 69 could read:

Mathematically, is it the case that \(P_1 \Rightarrow P_2\)? If so, taking \(\mathit{grants}\) to be a function that takes a policy and returns the set of all grants in that policy, \(\mathit{grants}(P_1) \subseteq \mathit{grants}(P_2)\).

And the set-difference item in the Prover section could put its equation on its own line. Indent the equation and the paragraph after it so they stay inside the list item, and leave a blank line before the next item:

2. **Set difference:** this is what `forbid` adds. A matching `forbid` always overrides any `permit`, so

    \[
    \mathit{allowed}(P) = \Big(\bigcup \mathit{permits}\Big) \setminus \Big(\bigcup \mathit{forbids}\Big)
    \]

    That's the formal reason "forbid always wins" and why policy order doesn't matter.

3. **Intersection**, within a single policy: ...

The three relations would follow the same pattern: \(\mathit{allowed}(P_1) \subseteq \mathit{allowed}(P_2)\) for inclusion, \(\mathit{allowed}(P_1) = \mathit{allowed}(P_2)\) for equivalence, and \(\mathit{allowed}(P_1) \cap \mathit{allowed}(P_2) = \emptyset\) for disjointness.

[vishwa-raman]

@johnnygreco - Addressed all comments. Please take a look.

[johnnygreco]

Great post, thanks @vishwa-raman!!

[vishwa-raman]

Addressed the footnote order which was the last thing remaining. Will merge once everything passes.