maelys-git

maelys-git

maelys-git is a C wrapper around the git binary. Before any git command runs, it evaluates a Datalog policy to decide whether the operation is allowed. This wrapper runs before git is exec'd, so git hooks and --no-verify are irrelevant to denied operations: a denied operation never reaches git at all.

This tutorial builds the wrapper in five levels of increasing rigour.

Level 1
Minimal gate
argv → EDB → allow/deny
Level 2
Deny codes
stable identifiers
Level 3
Rich context
files, classes, state
Level 4
Per-repo policy
manifest + SHA + sig
Level 5
Receipts
audited gate

Why not git hooks

git hook (.git/hooks/)             maelys-git
──────────────────────────────────────────────────────────────
Shell scripts, not versioned       Datalog in .maelys/git/policy.dl
Bypassable via --no-verify         Enforced before git runs
One hook per event                 One policy for all operations
No audit trail                     Receipt per decision, with proof
Hard to test                       Testable with edb_add_fact
Silent conflicts                   Explicit deny rules + stratified negation

Level 1 — Minimal gate

Level 1 introduces the core pattern: turn a Git command into runtime facts, evaluate a Datalog policy, and only execute the real git binary if the policy derives allow(Op). This level deliberately keeps the domain small: operation, target ref, user, flags, and commit-message validity, with a small allowlist of known operations. It is the minimal policy gate, and it is fail-closed: anything it cannot determine with certainty is denied.

The pipeline

git pushuser commandEDBargv + envsolve_onceallow / denygitor blocked

Domain

/* Minimal domain for Level 1. Level 3 extends this with
   source_ref, changed_file, sensitive_file_staged,
   approval_present, working_tree_dirty, branch_class. */
static const maelys_datalog_predicate_def_t git_preds[] = {
  /* EDB: runtime command context */
  { "operation",        1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "target_ref",       1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "user",             1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "flag",             1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "commit_msg",       1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "valid_commit_msg", 1, MAELYS_DATALOG_PRED_KIND_EDB },
 
  /* POLICY_FACT: ruleset configuration */
  { "protected_branch", 1, MAELYS_DATALOG_PRED_KIND_POLICY_FACT },
  { "blocked_user",     1, MAELYS_DATALOG_PRED_KIND_POLICY_FACT },
  { "release_manager",  1, MAELYS_DATALOG_PRED_KIND_POLICY_FACT },
  { "known_operation",  1, MAELYS_DATALOG_PRED_KIND_POLICY_FACT },
 
  /* IDB / QUERY: decisions.
     deny/2     : query-visible for receipt/debug deny-code enumeration.
     deny_any/1 : internal collapse predicate used by allow/1.
     allow/1    : queried by the wrapper to make the decision. */
  { "deny",     2, MAELYS_DATALOG_PRED_KIND_IDB |
                    MAELYS_DATALOG_PRED_KIND_QUERY },
  { "deny_any", 1, MAELYS_DATALOG_PRED_KIND_IDB },
  { "allow",    1, MAELYS_DATALOG_PRED_KIND_IDB |
                    MAELYS_DATALOG_PRED_KIND_QUERY },
};

Policy

protected_branch("main").
protected_branch("master").
protected_branch("release").
blocked_user("ci-bot").
release_manager("alice").
release_manager("bob").
known_operation("push").
known_operation("commit").
 
/* Unknown operation: denied by default, not allowed because no deny matched. */
deny(Op, "GIT_UNKNOWN_OPERATION") :-
    operation(Op), not(known_operation(Op)).
 
/* Force covers --force, -f, --force-with-lease, --force-if-includes and a
   leading '+' in a refspec: the C side normalizes them all to flag("force"). */
deny("push", "GIT_FORCE_PUSH") :-
    operation("push"), flag("force").
 
deny("push", "GIT_PROTECTED_BRANCH") :-
    operation("push"), target_ref(B), protected_branch(B),
    user(U), not(release_manager(U)).
 
/* Delete covers --delete, -d, -D and a leading ':' in a refspec:
   the C side normalizes them all to flag("delete"). */
deny("push", "GIT_DELETE_PROTECTED") :-
    operation("push"), flag("delete"), target_ref(B), protected_branch(B).
 
deny("commit", "GIT_BLOCKED_USER") :-
    operation("commit"), user(U), blocked_user(U).
 
deny("commit", "GIT_BAD_COMMIT_PREFIX") :-
    operation("commit"), commit_msg(M), not(valid_commit_msg(M)).
 
deny_any(Op) :- deny(Op, Code).
 
/* allow requires known_operation(Op): an unlisted operation is denied,
   never allowed merely because no deny rule happened to match it. */
allow(Op) :- operation(Op), known_operation(Op), not(deny_any(Op)).
i

Allowlist, not allow-by-default. allow(Op) requires known_operation(Op). Without it, the classic trap is that any operation with no matching deny rule is allowed automatically. Here, an operation the policy does not list is denied (GIT_UNKNOWN_OPERATION). Note that merge is not listed: git merge feature merges into the current branch, which is not in argv, so Level 1 cannot determine the protected ref and denies merge as unknown. See the refspec and identity notes below.

i

The deny reason is a stable code (GIT_FORCE_PUSH, GIT_PROTECTED_BRANCH), not a human-readable string. Human messages live in a C lookup table and can change without touching the policy or breaking receipts. See Level 2.

i

Policy vocabulary vs runtime evidence. This policy uses string constants directly in the .dl source: "push", "force", "GIT_FORCE_PUSH", "main", etc. In Maelys DL, every string written in the .dl source must belong to the registered atom vocabulary before parsing. In manifest/closed-vocabulary mode (the pattern used here), this is handled by the manifest loader.

Runtime values — user name, branch name, commit message — are different: they are unknown at policy-load time and are injected separately into the EDB via edb_add_runtime_symbol_fact. They do not need to be pre-registered.

Policy source  →  "push", "GIT_FORCE_PUSH", "--force"  → atom vocabulary
Runtime EDB    →  user("alice"), target_ref("main")     → edb_add_runtime_symbol_fact

EDB from argv

Every insertion is checked. A gate cannot silently drop a fact: if operation("push") fails to insert, no deny rule can fire and allow/1 becomes derivable by default — a missing fact would turn a deny into an allow. On any failure we return the error and the caller fails closed.

static maelys_result_t
populate_edb(maelys_datalog_edb_t *edb, const git_context_t *ctx)
{
    maelys_result_t rc;
 
    /* operation is mandatory; its failure must fail the gate */
    rc = maelys_datalog_edb_add_runtime_symbol_fact(edb, "operation", ctx->operation);
    if (rc != MAELYS_OK) return rc;
 
    if (ctx->user) {
        rc = maelys_datalog_edb_add_runtime_symbol_fact(edb, "user", ctx->user);
        if (rc != MAELYS_OK) return rc;
    }
    if (ctx->target_ref) {
        rc = maelys_datalog_edb_add_runtime_symbol_fact(edb, "target_ref", ctx->target_ref);
        if (rc != MAELYS_OK) return rc;
    }
    if (ctx->has_force) {
        rc = maelys_datalog_edb_add_runtime_symbol_fact(edb, "flag", "force");
        if (rc != MAELYS_OK) return rc;
    }
    if (ctx->has_delete) {
        rc = maelys_datalog_edb_add_runtime_symbol_fact(edb, "flag", "delete");
        if (rc != MAELYS_OK) return rc;
    }
 
    if (ctx->commit_msg) {
        rc = maelys_datalog_edb_add_runtime_symbol_fact(edb, "commit_msg", ctx->commit_msg);
        if (rc != MAELYS_OK) return rc;
        static const char *ok[] = { "feat:", "fix:", "chore:", "docs:", "refactor:", NULL };
        for (int i = 0; ok[i]; i++)
            if (strncmp(ctx->commit_msg, ok[i], strlen(ok[i])) == 0) {
                rc = maelys_datalog_edb_add_runtime_symbol_fact(edb, "valid_commit_msg", ctx->commit_msg);
                if (rc != MAELYS_OK) return rc;
                break;
            }
    }
    return maelys_datalog_edb_finalize(edb);
}
!

Check every insertion in a gate. Ignoring the maelys_result_t of edb_add_runtime_symbol_fact is the most common way to break fail-closed: a dropped operation or flag fact silently weakens the policy. The deny rules depend on those facts being present.

Evaluate and exec

static int evaluate(const maelys_datalog_policy_set_t *ps,
                    const git_context_t *ctx) {
    static maelys_datalog_edb_t edb;
    static maelys_datalog_fact_t pool[256];
 
    if (maelys_datalog_edb_init(&edb, pool, 256,
            &ps->policies[0].symbols, &ps->policies[0].registry) != MAELYS_OK)
        return 1;  /* fail closed */
 
    /* Intern the operation ONCE, before solving, and keep the id.
       Reusing it for the query term avoids a second intern after solve
       (which would mutate the post-load symbol table) and guarantees the
       query uses the same id the EDB was built with. */
    maelys_datalog_symbol_id_t op_id;
    if (maelys_datalog_edb_intern_runtime_symbol(&edb, ctx->operation, &op_id) != MAELYS_OK)
        return 1;  /* fail closed */
 
    if (populate_edb(&edb, ctx) != MAELYS_OK)
        return 1;  /* fail closed */
 
    maelys_datalog_solve_result_t *result = NULL;
    if (maelys_datalog_solve_once(&ps->policies[0], &edb, &result) != MAELYS_OK)
        return 1;
 
    maelys_datalog_term_t op_term = {
        .kind = MAELYS_DATALOG_TERM_SYMBOL, .as.symbol = op_id };
 
    bool allowed = false;
    maelys_result_t rc = maelys_datalog_query_solved_ground_fact(
        result, "allow", &op_term, 1, &allowed);
    maelys_datalog_solve_result_free(result);
 
    if (rc != MAELYS_OK) return 1;          /* fail closed */
    if (!allowed) {
        fprintf(stderr, "maelys-git: '%s' denied by policy\n", ctx->operation);
        return 1;
    }
    return 0;
}
i

Intern once, query with the same id. The operation string is interned during EDB build and the returned id is reused to build the allow(Op) query term. Re-interning after solve_once would write into the symbol table the ruleset shares, mutating state that should be stable after load. For an unknown operation the intern still succeeds (a new runtime symbol), but no allow fact is derived for it, so the gate denies — fail-closed by default.

Why this is fail-closed by construction

The wrapper above is short, but three of its details are not stylistic — the engine forces them, and getting any of them wrong fails loudly rather than silently weakening the gate. They are worth calling out because they are the reason a Maelys gate is hard to write insecurely.

Lifecycle order   intern BEFORE finalize, not after
Read-only query   reuse the id, never intern post-solve
No silent loss    every insertion return is checked

Lifecycle: intern before finalize. The EDB has a state machine. Once edb_finalize runs (inside populate_edb), the EDB is immutable and any further intern or insertion returns MAELYS_ERR_INVALID_STATE. That is why the operation is interned before populate_edb is called. Inverting the two lines does not "sometimes work" — it returns a hard error, and the gate fails closed. The engine makes the unsafe ordering impossible to ship by accident.

Query is read-only. After solve_once, the result is queried by building a maelys_datalog_term_t from the id obtained earlier. The query API never mutates: it does not intern, it does not touch the symbol table. Re-interning the operation string after the solve would write into the table the ruleset shares, which is exactly the post-load mutation the engine's design forbids. Reusing the id keeps the decision path 100% read-only.

No silent capacity loss. Every edb_add_runtime_symbol_fact return is checked. If the static fact pool were exhausted (unlikely with Git arguments, but bounded and therefore possible), the insertion returns an error, the wrapper denies, and Git never runs. There is no truncated EDB that quietly solves to allow because a fact silently failed to insert.

i

This is the general shape of a Maelys integration: the engine's invariants (strict lifecycle, read-only queries, transactional capacity, zero-malloc static pools) push the caller toward a fail-closed implementation. A bug in any of the three points above surfaces as an error code, not as a silent allow. The same invariants appear in maelys-pty and document access.

!

What the engine does not protect you from. The three guarantees above are narrow: the engine makes a specific class of bug loud instead of silent — acting after finalize, mutating during a query, or a dropped insertion you chose to check. It does not make arbitrary code safe, and two limits matter.

First, the capacity guarantee only helps if you read the return value. The engine hands you an error code; it cannot force you to test it. Write edb_add_runtime_symbol_fact(edb, "user", u); and ignore the result, and a dropped fact can still turn a deny into an allow. The engine did not save you — it returned the error you threw away.

Second, and more important: the engine guarantees that if your facts are correct, the decision is correct. It guarantees nothing about whether your facts are true. Every context bug in this tutorial — binding target_ref to the remote instead of the branch, treating git push origin as unambiguous, reading identity from a spoofable $USER — produces a valid allow over a well-formed EDB. The EDB simply asserts the wrong thing about the world, and the solver faithfully reasons from it. Garbage in, valid garbage out.

So the work that actually secures the gate — parsing argv correctly, normalizing refspecs, refusing ambiguity, trusting a real identity source — lives entirely in the C that builds the EDB. The engine protects the decision; you are still responsible for the facts.

Load policy and run

Level 1 keeps the policy compiled in and loads it with load_policy_inline_with_static_domain (static predicate table + inline source in one call). Level 4 replaces this with manifest_load_ex and SHA-256 verification.

int main(int argc, char *argv[]) {
    /* Load the compiled-in policy. Any load error fails the gate closed. */
    maelys_datalog_policy_set_t ps;
    maelys_datalog_diagnostic_t diag = {0};
 
    maelys_result_t rc = maelys_datalog_load_policy_inline_with_static_domain(
        git_preds, sizeof(git_preds) / sizeof(git_preds[0]),
        "git_policy", "git_policy.l1",
        POLICY_SRC, sizeof(POLICY_SRC) - 1u,
        0, &ps, &diag);
    if (rc != MAELYS_OK) {
        fprintf(stderr, "maelys-git: policy load error: %s\n",
                diag.message[0] ? diag.message : "unknown");
        return 1;  /* fail closed */
    }
 
    git_context_t ctx;
    extract_context(argc, argv, &ctx);
    if (!ctx.operation) {
        maelys_datalog_policy_set_clear(&ps);
        return 1;
    }
 
    /* Fail-closed preconditions: make the absence (or ambiguity) of a fact
       impossible for the rules that need it. A missing user, an unreadable
       commit message, or an undeterminable push ref must never let the
       corresponding deny rule silently fail to fire. */
    if (!ctx.user || ctx.user[0] == '\0') {
        fprintf(stderr, "maelys-git: missing user identity\n");
        maelys_datalog_policy_set_clear(&ps);
        return 1;
    }
    if (strcmp(ctx.operation, "commit") == 0 &&
        (!ctx.commit_msg || ctx.commit_msg[0] == '\0')) {
        fprintf(stderr, "maelys-git: commit message not available to gate\n");
        maelys_datalog_policy_set_clear(&ps);
        return 1;
    }
    if (ctx.needs_ref && ctx.ref_ambiguous) {
        fprintf(stderr, "maelys-git: push target ref is ambiguous or missing\n");
        maelys_datalog_policy_set_clear(&ps);
        return 1;
    }
 
    int denied = evaluate(&ps, &ctx);
    maelys_datalog_policy_set_clear(&ps);
    if (denied) return 1;
 
    /* Avoid PATH loop if maelys-git shadows git in PATH:
       set MAELYS_GIT_REAL=/usr/bin/git or use an absolute path.
       Also fix argv[0] so real git sees its own name, not the wrapper's. */
    const char *real_git = getenv("MAELYS_GIT_REAL");
    if (!real_git) real_git = "/usr/bin/git";
    argv[0] = (char *)real_git;
    execv(real_git, argv);
    perror("maelys-git: execv");  /* execv only returns on error */
    return 1;
}
!

Parsing the refspec. The protected branch is the destination of the push, and it must be extracted with certainty or the gate denies. Level 1 counts positionals and requires exactly git push <remote> <refspec> (two of them): git push origin alone is the remote, not a branch, so the destination is undeterminable → deny; more than two means multiple refspecs, which Level 1 does not evaluate one by one → deny. The single refspec is then normalized — refs/heads/main, HEAD:main, main:main, +main, :main all reduce to main (with + → force, leading : → delete) — and anything that cannot be normalized with certainty (tag namespaces, a bare HEAD, exotic characters) is denied. Capturing the first positional instead would bind target_ref to the remote ("origin") and silently miss the protected branch.

!

A missing fact is a bypass. Several deny rules depend on a fact being present: GIT_PROTECTED_BRANCH needs user(U), GIT_BAD_COMMIT_PREFIX needs commit_msg(M). If the user identity is unset, or the commit message lives in an editor / -F file instead of -m, that fact never enters the EDB, the deny rule cannot fire, and allow/1 is derivable by default. The gate must establish these preconditions in C before solving, and deny when it cannot. That is why the identity and commit-message checks above run before evaluate. The same reasoning extends to force detection (--force-with-lease, a leading + in a refspec) and to refspec forms like HEAD:main or refs/heads/main that must normalize to main before the protected-branch rule can match.

i

Beyond Level 1: a fail-closed gate over all of git. This tutorial keeps a small domain to teach the pattern. A production gate must classify every subcommand (≈50+), normalize refspecs, skip git global options (git -C path …, -c key=val), honor the -- pathspec separator, and treat anything it cannot parse with certainty as deny. The reference implementation does this with a subcommand→risk-class table (readonly, local_mutate, publish, history_rewrite, ref_delete, config_mutate, submodule, plumbing, unknown) and an allowed_class(...) allowlist, so an unknown subcommand or an un-normalizable refspec injects a signal fact (context_incomplete, unparsed_token) that the policy denies. See the standalone maelys_git_gate.c.

Level 1 in action

$ maelys-git push origin main          → BLOCKED (GIT_PROTECTED_BRANCH)
$ maelys-git push --force origin feat  → BLOCKED (GIT_FORCE_PUSH)
$ maelys-git commit -m "wip"           → BLOCKED (GIT_BAD_COMMIT_PREFIX)
$ maelys-git push origin               → BLOCKED (ambiguous ref, preflight)
$ maelys-git status                    → BLOCKED (GIT_UNKNOWN_OPERATION)
$ maelys-git push origin feat/foo      → ALLOWED → execv("/usr/bin/git", argv)
i

git status is blocked because Level 1's allowlist is push and commit only — read-only commands are not listed, so they are denied as unknown. That is the strict posture; to permit reads, add them to known_operation(...), or use the risk-class gate (maelys_git_gate.c) which allows a whole readonly class at once.

i

Level 1 queries allow(Op) only. It knows the operation was denied but not which deny code fired. Retrieving the exact code (GIT_FORCE_PUSH, GIT_PROTECTED_BRANCH, etc.) requires enumerating deny/2 results or using the receipt API. Both are shown in Level 5.

Level 2 — Structured deny codes

Level 2 separates machine-stable decision codes from human-readable messages. The policy derives facts such as deny("push", "GIT_FORCE_PUSH"), while the wrapper maps GIT_FORCE_PUSH to a user-facing message. This keeps receipts stable even when wording, localization, or UI messages change.

The principle

deny("push", "GIT_FORCE_PUSH")     ← stable code in policy
    ↓
C lookup table:
  "GIT_FORCE_PUSH"        → "force-push is forbidden"
  "GIT_PROTECTED_BRANCH"  → "direct push to protected branch"
  "GIT_RELEASE_BRANCH"    → "only release managers can push to release branches"
  "GIT_BLOCKED_USER"      → "user is not allowed to commit"
  "GIT_BAD_COMMIT_PREFIX" → "commit message must start with feat: fix: ..."
  "GIT_DELETE_PROTECTED"  → "deleting a protected branch is forbidden"
  "GIT_SENSITIVE_FILE"    → "this file requires explicit approval"

Human messages can change without touching the policy. The deny code is what appears in receipts and audit logs — it is stable across policy versions.

Message table in C

static const struct { const char *code; const char *message; }
deny_messages[] = {
    { "GIT_FORCE_PUSH",        "force-push is forbidden" },
    { "GIT_PROTECTED_BRANCH",  "direct push to protected branch is forbidden" },
    { "GIT_BLOCKED_USER",      "user is not allowed to commit" },
    { "GIT_BAD_COMMIT_PREFIX", "commit message must start with feat: fix: chore: docs: refactor:" },
    { "GIT_DELETE_PROTECTED",  "deleting a protected branch is forbidden" },
    { "GIT_SENSITIVE_FILE",    "this file requires explicit approval" },
    { "GIT_RELEASE_BRANCH",   "only release managers can push to release branches" },
    { NULL, NULL }
};
 
static const char *message_for_code(const char *code) {
    for (int i = 0; deny_messages[i].code; i++)
        if (strcmp(deny_messages[i].code, code) == 0)
            return deny_messages[i].message;
    return code;  /* fallback: show code if unknown */
}

Level 3 — Rich Git context

Level 3 enriches the EDB with facts extracted from Git state: staged files, branch families, working-tree status, sensitive-file classification, and approval markers. The wrapper performs string matching and Git inspection in C; the Datalog policy only reasons over already-classified facts. This keeps the policy deterministic, bounded, and auditable.

The "no string builtins" principle

i

Maelys DL has no starts_with(), no regex(), no glob(). The wrapper extracts contextual properties into EDB facts. The policy only decides.

Instead of:     starts_with(File, "src/core/")   ← not in Datalog
Inject instead: sensitive_file_staged("src/core/policy.c")  ← EDB fact
 
Instead of:     regex(Branch, "release/.*")       ← not in Datalog
Inject instead: branch_class("release")            ← EDB fact from C

This keeps the policy bounded, deterministic, and auditable.

Extended domain

static const maelys_datalog_predicate_def_t git_preds_l3[] = {
  { "operation",            1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "target_ref",           1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "source_ref",           1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "user",                 1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "flag",                 1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "commit_msg",           1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "valid_commit_msg",     1, MAELYS_DATALOG_PRED_KIND_EDB },
 
  /* Level 3: richer context — C extracts, policy decides */
  { "changed_file",         1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "sensitive_file_staged",1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "approval_present",     1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "working_tree_dirty",   1, MAELYS_DATALOG_PRED_KIND_EDB },
  { "branch_class",         1, MAELYS_DATALOG_PRED_KIND_EDB },
 
  /* POLICY_FACT */
  { "protected_branch",     1, MAELYS_DATALOG_PRED_KIND_POLICY_FACT },
  { "blocked_user",         1, MAELYS_DATALOG_PRED_KIND_POLICY_FACT },
  { "release_manager",      1, MAELYS_DATALOG_PRED_KIND_POLICY_FACT },
  /* sensitive_path is not needed: C classifies files into sensitive_file_staged */
 
  /* IDB */
  { "deny",    2, MAELYS_DATALOG_PRED_KIND_IDB | MAELYS_DATALOG_PRED_KIND_QUERY },
  { "deny_any",1, MAELYS_DATALOG_PRED_KIND_IDB },
  { "allow",   1, MAELYS_DATALOG_PRED_KIND_IDB | MAELYS_DATALOG_PRED_KIND_QUERY },
};

Extended policy

/* Sensitive path classification is done in C.
   C injects sensitive_file_staged(F) for staged files matching sensitive paths.
   Maelys DL has no starts_with() or glob(). */
 
/* ── Force push ─────────────────────────────────────────────── */
deny("push", "GIT_FORCE_PUSH") :- operation("push"), flag("--force").
deny("push", "GIT_FORCE_PUSH") :- operation("push"), flag("-f").
 
/* ── Protected branch (non-managers only) ───────────────────── */
deny("push", "GIT_PROTECTED_BRANCH") :-
    operation("push"), target_ref(B), protected_branch(B),
    user(U), not(release_manager(U)).
 
/* ── Release branch family (C injects branch_class("release") for release/*) ── */
/* branch_class("release") covers release/v1, release/v2, etc.
   protected_branch("release") above covers only the branch named exactly "release".
   These two rules are complementary, not redundant. */
deny("push", "GIT_RELEASE_BRANCH") :-
    operation("push"),
    branch_class("release"),
    user(U),
    not(release_manager(U)).
 
/* ── Blocked user ───────────────────────────────────────────── */
deny("commit", "GIT_BLOCKED_USER") :-
    operation("commit"), user(U), blocked_user(U).
 
/* ── Commit message prefix ──────────────────────────────────── */
deny("commit", "GIT_BAD_COMMIT_PREFIX") :-
    operation("commit"), commit_msg(M), not(valid_commit_msg(M)).
 
/* ── Sensitive file requires approval ───────────────────────── */
deny("commit", "GIT_SENSITIVE_FILE") :-
    operation("commit"),
    sensitive_file_staged(F),
    not(approval_present(F)).
 
/* ── Dirty working tree cannot be pushed ───────────────────── */
deny("push", "GIT_DIRTY_TREE") :-
    operation("push"),
    working_tree_dirty("true").
 
/* ── deny_any / allow ───────────────────────────────────────── */
deny_any(Op) :- deny(Op, Code).
allow(Op)    :- operation(Op), not(deny_any(Op)).

Extended EDB population

/* C extracts contextual properties — policy never does string matching */
 
if (ctx->source_ref)
    maelys_datalog_edb_add_runtime_symbol_fact(edb, "source_ref", ctx->source_ref);
 
/* Branch family: C does prefix match, policy sees branch_class fact */
if (ctx->target_ref && strncmp(ctx->target_ref, "release/", 8) == 0)
    maelys_datalog_edb_add_runtime_symbol_fact(edb, "branch_class", "release");
 
/* Staged files from git diff --cached --name-only */
for (int i = 0; i < n_staged; i++) {
    maelys_datalog_edb_add_runtime_symbol_fact(edb, "changed_file", staged[i]);
    if (is_sensitive_path(staged[i]))   /* C prefix check */
        maelys_datalog_edb_add_runtime_symbol_fact(edb, "sensitive_file_staged", staged[i]);
    if (has_approval(staged[i]))
        maelys_datalog_edb_add_runtime_symbol_fact(edb, "approval_present", staged[i]);
}
 
/* Working tree state */
if (is_working_tree_dirty())
    maelys_datalog_edb_add_runtime_symbol_fact(edb, "working_tree_dirty", "true");

Trustworthy identity: not from the environment

Level 1 reads the user from getenv("GIT_COMMITTER_NAME") then getenv("USER"). That is fine for a demo, but environment variables are attacker-controlled: any caller can run USER=alice maelys-git push … and impersonate a release manager. A real gate must derive identity from the operating system, not from the environment it was handed.

#include <unistd.h>
#include <pwd.h>
 
/* Real identity: the uid the process runs as, resolved to a name.
   Not spoofable through the environment. */
static const char *real_user(void) {
    struct passwd *pw = getpwuid(getuid());
    return pw ? pw->pw_name : NULL;
}
!

Identity must not come from $USER. getenv("USER") / getenv("GIT_COMMITTER_NAME") are trivially overridden on the command line, so a policy that trusts them to identify release managers or blocked users is bypassable. From Level 3 on, resolve identity with getpwuid(getuid()) (or your platform's authenticated identity source) before injecting user(U) into the EDB. The Datalog rules do not change — only where the C side gets the name it trusts.

Level 4 — Per-repository policy

Level 4 moves the policy from compiled-in source to a repository-local .maelys/git/ directory. Each repository can carry its own manifest, policy file, SHA verification, and optional signature. Policy updates become normal reviewed commits or pull requests, and a tampered policy fails closed at load time.

Repository layout

.maelys/
  git/
    manifest.json      ← describes the policy: id, domain, SHA, mode
    policy.dl          ← the Datalog rules
    policy.sig         ← detached signature (optional, out of scope here)

Manifest

{
  "schema_version": 1,
  "policies": [
    {
      "id":     "git_policy.main",
      "domain": "git_policy",
      "source": "policy.dl",
      "sha256": "a3f7c291...",
      "mode":   "enforce"
    }
  ],
  "public_queries": ["allow", "deny", "deny_any"]
}

Loading at startup

static int load_repo_policy(maelys_datalog_policy_set_t *ps) {
    char root[PATH_MAX], manifest_path[PATH_MAX];
 
    if (find_repo_root(root, sizeof(root)) != 0) {
        fprintf(stderr, "maelys-git: not in a git repository\n");
        return 1;
    }
    snprintf(manifest_path, sizeof(manifest_path),
             "%s/.maelys/git/manifest.json", root);
 
    maelys_datalog_diagnostic_t diag = {0};
    if (maelys_datalog_manifest_load_ex(manifest_path, 0, ps, &diag) != MAELYS_OK) {
        fprintf(stderr, "maelys-git: policy load error: %s\n", diag.message);
        return 1;
    }
    return 0;
}

The manifest loading verifies the SHA-256 of policy.dl against the manifest entry. A tampered policy file fails to load — the gate stays closed.

Updating the policy

vim .maelys/git/policy.dl
sha256sum .maelys/git/policy.dl | awk '{print $1}'   # update sha256 in manifest
vim .maelys/git/manifest.json
git add .maelys/git/
git commit -m "policy: require approval for sensitive files"

Policy changes are PRs. The SHA-256 ties the manifest to the exact policy bytes that reviewers approved.

Level 5 — Receipts

Level 5 turns the wrapper into an audited gate. Every allow or deny decision produces a structured receipt containing the operation, user, target ref, policy identity, policy hash, deny code, and proof summary when available. The receipt makes the decision reviewable without relying on shell logs or re-running Git.

Receipt structure

{
  "tool":          "maelys-git",
  "operation":     "push",
  "target_ref":    "main",
  "user":          "alice",
  "decision":      "deny",
  "deny_code":     "GIT_PROTECTED_BRANCH",
  "deny_message":  "direct push to protected branch is forbidden",
  "policy_id":     "git_policy.main",
  "policy_sha256": "a3f7c291...",
  "timestamp":     "2025-06-15T14:32:01Z",
  "proof_summary": {
    "derived":    "deny(\"push\", \"GIT_PROTECTED_BRANCH\")",
    "facts_used": [
      "operation(\"push\")",
      "target_ref(\"main\")",
      "protected_branch(\"main\")"
    ]
  }
}

Emitting the receipt

static void emit_receipt(const git_context_t *ctx,
                          bool allowed,
                          const char *deny_code,
                          const char *policy_id,
                          const char *policy_sha256)
{
    fprintf(stderr,
        "{\n"
        "  \"tool\": \"maelys-git\",\n"
        "  \"operation\": \"%s\",\n"
        "  \"target_ref\": \"%s\",\n"
        "  \"user\": \"%s\",\n"
        "  \"decision\": \"%s\",\n"
        "  \"deny_code\": \"%s\",\n"
        "  \"deny_message\": \"%s\",\n"
        "  \"policy_id\": \"%s\",\n"
        "  \"policy_sha256\": \"%s\"\n"
        "}\n",
        ctx->operation,
        ctx->target_ref ? ctx->target_ref : "",
        ctx->user ? ctx->user : "",
        allowed ? "allow" : "deny",
        deny_code ? deny_code : "",
        deny_code ? message_for_code(deny_code) : "",
        policy_id,
        policy_sha256);
}

In this example, deny_code is assumed to come from the receipt/proof API or from an enumeration of deny(Op, Code) facts in the solve result. The minimal ground-query API (query_solved_ground_fact) only proves allow/deny — it does not bind the code value directly. The receipt API recovers the exact code.

The proof summary (which rule fired, which facts were used) is produced by the receipt and proof API when enabled. Until canonical proof serialization is complete, the minimal receipt — decision, deny code, policy identity, and selected EDB facts — is already valuable. See Receipts.

Level 5 in action

$ maelys-git push origin main
{
  "tool": "maelys-git",
  "operation": "push",
  "target_ref": "main",
  "user": "alice",
  "decision": "deny",
  "deny_code": "GIT_PROTECTED_BRANCH",
  "deny_message": "direct push to protected branch is forbidden",
  "policy_id": "git_policy.main",
  "policy_sha256": "a3f7c291..."
}
maelys-git: 'push' denied by policy

The full picture

Level 1  argv/env → EDB → solve → allow/deny → execv(real_git, argv)
Level 2  deny codes stable, human messages in C lookup table
Level 3  rich EDB: files, classes, tree state; C extracts, policy decides
Level 4  .maelys/git/manifest.json + policy.dl versioned in repo + SHA verify
Level 5  receipt per decision: deny code, policy hash, proof summary

This is the exact pattern Maelys uses for agent orchestration:

observe context → project into facts → apply deterministic policy
→ produce decision → emit receipt → execute only if allowed

What you have learned

- deny/2 uses stable codes (GIT_FORCE_PUSH), not human strings.
  Human messages live in a C table and can change without touching policy.
- Maelys DL has no string builtins. The wrapper extracts contextual
  properties (sensitive_file_staged, branch_class, working_tree_dirty("true")).
  The policy only decides. This keeps it bounded and auditable.
- working_tree_dirty uses arity 1 with value "true" — arity 0 is not used.
- deny_any/1 is needed because not(deny(Op, _)) uses _ as an unbound
  variable in a negated literal — rejected by the rule safety checker.
- valid_commit_msg(M) must carry the actual message, not "ok".
- Check every edb_add_runtime_symbol_fact return in a gate. A silently
  dropped fact (operation, flag) can turn a deny into an allow.
- Intern the operation once before solving and reuse the id for the query.
  Re-interning after solve mutates the ruleset's shared symbol table.
- For push, the gate requires exactly `git push <remote> <refspec>` and
  normalizes the refspec (refs/heads/main, HEAD:main, +main, :main -> main).
  `git push origin` alone, or multiple refspecs, are ambiguous -> deny.
- A gate must establish required facts in C before solving: user identity for
  mutating ops, and the commit message for commit. Deny when they are absent,
  or a missing fact silently turns a deny into an allow.
- A production gate classifies every subcommand into a risk class and uses an
  allowed_class allowlist, so unknown subcommands and un-normalizable refspecs
  fail closed. See the standalone maelys_git_gate.c.
- Use execv(real_git, argv) with an absolute path, not execvp("git"),
  to avoid an infinite loop if maelys-git shadows git in PATH.
- Per-repo policy (.maelys/git/) makes each repository self-contained.
  Policy changes are PRs. SHA mismatch fails the gate.
- Level 1 only knows allow/deny. The exact deny code requires Level 5
  receipts or deny/2 enumeration.
- Receipts make every decision auditable: deny code, policy identity,
  proof summary — via the receipt/proof API when enabled, without re-running the solver.

Where to go next

  • maelys-pty — the same pattern applied to an interactive shell with forkpty and seccomp/execve tracing.
  • Document access — ABAC for document ownership, sharing, and sensitivity levels.
  • Manifest loading — full reference for .maelys/git/manifest.json format, SHA verification, and signing.
  • Receipts — structured proof trees and audit receipts per decision.
  • Rulesets — full policy language reference.