From 06d06a80c1928b6851352ac2c903297a696f531f Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Wed, 14 Oct 2026 01:19:45 +0100 Subject: [PATCH 1/2] AGENTS.md: allow decide +kernel for certificates and test vectors Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- AGENTS.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 6019316..b90cd5b 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -229,8 +229,11 @@ globally; use `letI` or a wrapper carrier. - Do not raise `maxHeartbeats` or `maxRecDepth` to make a proof pass; a heartbeat limit is a symptom to diagnose. -- Do not use `decide` or `native_decide` in new proofs or checks. For small - test vectors, use ordinary kernel-checked equality and simplification proofs. +- Do not use `native_decide`, `bv_decide` or any native evaluation in proofs or + checks, and do not use plain `decide`, which evaluates in the elaborator. A + computation certificate or a test vector may use `decide +kernel`: the kernel + evaluates it, and it adds no axiom. Small test vectors can also use ordinary + kernel-checked equality and simplification proofs. - Do not introduce `Fintype I` or enumerate `Fin n` merely to shorten a proof. - Prefer `Nat`-indexed traces and explicit finite-support witness sets for long hybrids. Keep dependent transcript values out of instance search. From 35a42e527809fcb3b540077797cf4d723565fde7 Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Wed, 14 Oct 2026 01:28:13 +0100 Subject: [PATCH 2/2] AGENTS.md: #guard tests stay allowed Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- AGENTS.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index b90cd5b..11c4e55 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -229,11 +229,13 @@ globally; use `letI` or a wrapper carrier. - Do not raise `maxHeartbeats` or `maxRecDepth` to make a proof pass; a heartbeat limit is a symptom to diagnose. -- Do not use `native_decide`, `bv_decide` or any native evaluation in proofs or - checks, and do not use plain `decide`, which evaluates in the elaborator. A - computation certificate or a test vector may use `decide +kernel`: the kernel - evaluates it, and it adds no axiom. Small test vectors can also use ordinary - kernel-checked equality and simplification proofs. +- Do not use `native_decide`, `bv_decide` or any other native evaluation in a + proof, and do not use plain `decide`, which evaluates in the elaborator. A + computation certificate or a test vector stated as a proposition may use + `decide +kernel`: the kernel evaluates it, and it adds no axiom; small ones + can also use ordinary equality and simplification proofs. Known-answer tests + may run by evaluation with `#guard`, as the Commons tests do: they check the + code, and no proof depends on them. - Do not introduce `Fintype I` or enumerate `Fin n` merely to shorten a proof. - Prefer `Nat`-indexed traces and explicit finite-support witness sets for long hybrids. Keep dependent transcript values out of instance search.