Conversation
septract
force-pushed
the
cn-types
branch
2 times, most recently
from
February 11, 2026 20:38
a41d645 to
960af97
Compare
…bligations (42/46) C1: ctypeToBaseType now delegates to ctypeInnerToBaseType, mapping C integer types to Bits(sign, width) instead of unbounded Integer (matching CN's Memory.bt_of_sct). C5: PEwrapI maps each Iop to the correct BinOp instead of always returning add. C7: PEundef generates requireConstraint(false) unreachability obligation, matching CN's provable(LC.T(bool_ false)) check. H6 (partial): PEif now tracks path conditions (CN's path_cs) so obligations in branches have the branch condition in their assumptions. Guard patterns (ite(check, value, undef)) are stripped matching CN's core_to_mucore.ml. Also adds full CN audit report (docs/2026-02-08_CN_AUDIT_REPORT.md). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace flat Int pointer encoding with CN's proper algebraic datatype: - declare-datatype pointer ((NULL) (AiA alloc_id addr)) - 5 helper functions: ptr_shift, copy_alloc_id, alloc_id_of, bits_to_ptr, addr_of - Raw string preamble emitted to solver before every query - Thread TypeEnv through SmtLib translation for struct layout info - Implement memberShift, offsetOf, copyAllocId, hasAllocId - Update arrayShift to use ptr_shift, aligned to use addr_of+bvurem - Update cast operations for loc<->bits, loc->allocId - Pointer comparisons use bvult/bvule on addr_of - Update audit report: C2 FIXED Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- C3: Unit type uses cn_tuple_0 empty tuple datatype matching CN solver.ml:405 - Pointer arithmetic: ptr + int in specs now elaborates to arrayShift (matching CN compile.ml:447-463 mk_binop). Fixes test 022. - H9: Verified allocId as Int matches CN's VIP mode default (not a bug) - ResolveContext carries paramCTypes for pointee type lookup - Remaining failures: 023/045 (struct), 044 (SeqRMW) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…esolution (43/46) - Struct SMT declarations matching CN's CN_Structs (solver.ml:1035-1067) - Struct term translation: construction, member access, update - Struct resource unpacking matching CN's unpack_owned (pack.ml:104-140) - Struct resource repacking matching CN's packing_ft (pack.ml:42-92) - Recursive unpacking for nested structs (do_unfold_resources) - addResourceWithUnfold replaces addR everywhere (H8 partial fix) - Struct tag ID resolution in Resolve.lean (CN parser tags have id=0) - ptrMemberShift memop implementation in Expr.lean - Union types explicitly rejected (CN does not support unions) - Antipattern fixes: no .getD defaults, no silent catch-alls, explicit errors Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… checking, parser multi-requires fix (43→44/46) - H4: Replace fall-through defaults with explicit failures (union constructor, constrained values, ctorToSym catch-all, integer literal with non-Bits type) - H1: Infer structMember field types from tagDefs (CN wellTyped.ml:695-706) - C6: Extended-precision overflow check matching CN check.ml:986-1033 (Bits(Signed, 2*width+4), cast, compute, check representability) - Fix SMT sign_extend for signed bitvector widening (was zero_extend) - Fix parser bug: support multiple requires/ensures blocks (optional→many) - Update tests with overflow bounds required by C6 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…e expansion, add CN tests to CI (44→45/46) - M2: Generate representable constraint for ALL store types matching CN check.ml:1863-1877 (not just integers). SmtLib value_check handles Void/Byte/Pointer as true, Integer as range check (indexTerms.ml:959-1010). - M2: Add aligned assumption for creates with uintptr_bt cast matching CN check.ml:1799-1800 (cast_ Memory.uintptr_bt arg loc). - H7: Implement isSymLhsEquality (logicalConstraints.ml:61-67), add symEqs field to TypingState (typing.ml:14), extract sym_eqs in addC (typing.ml:410) and addLValue (typing.ml:352-354). Equality constraints propagated to SMT. - Add test-cn and test-cn-unit to CI Makefile targets. - Update audit report: M2/H4/H7 status, test classification, executive summary. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…d custom Sources: - CN test suite (tmp/cn/tests/cn/): bitwise ops, mod, implies, loops, enums, shifts - cn-tutorial working examples: add, unsigned, negation, conditional, swap, struct, write - cn-tutorial should-fail examples: wrong return, overflow, resource leak/conjure - Custom tests: unsigned arithmetic, multiple returns, nested struct, cast, false ensures Results: 66/82 pass (including expected failures), 16 fail exposing gaps: - Parser: bitwise operators (|, ^, &, ~, <<) in spec expressions - Parser: RW(...) without explicit type parameter (needs RW<type>(...)) - Parser: separate /*@ @*/ annotation blocks per function - SMT: bvsrem vs bvsmod mismatch for modulo - Missing: inline assert, ptr_eq builtin, nested struct resource matching - Existing: SeqRMW (044), shift type mismatch (071) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…x (78/82 tests) Parser: bitwise ops (&|^<<>>), implies keyword, optional Owned(p) syntax, NULL constant, % changed to Rem (bvsrem) matching CN, CN precedence table. Type checker: Core bitwise constructors (ivOR/ivXOR/ivAND/ivCOMPL with ctype), CN builtins (ptr_eq/addr_eq/is_null), resource type inference from pointer. Architecture: ResourceName.owned now Option Ctype for deferred inference. Test runner: unannotated files trivially pass, matching CN behavior. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add --nolibc and --libc-only flags to test_cn.sh matching test_interp.sh interface. Cerberus with --nolibc generates 3.6MB JSON in 0.2s vs 348MB in 5s, giving ~24x speedup per test. Rename stdlib-dependent tests to *.libc.fail.c (010, 011, 012, 014). Add make targets: test-cn (runs both), test-cn-nolibc, test-cn-libc. Add sandbox restriction to CLAUDE.md. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…erp patterns - PASS/FAIL/CERB_SKIP status per test with [N/TOTAL] prefix - Extract error reasons from test_cn output for FAIL lines - Handle expect-fail in shell (not via --expect-fail flag) - Use array for CERBERUS_FLAGS, capture exit codes via || pattern - Add require_cerberus, mutually exclusive flag guard, colored summary Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Lift TypingM from pure to IO, spawn Z3 as inline solver process. Solver operations: push/pop scoping, assume constraints, provable queries. Context operations (addA/addL/addC) now mirror to solver via solverAssume. Branch checking (pure_, tryBranch) uses push/pop for solver state scoping. PEif uses CN's four-way pattern (check.ml:1034-1056): provable(c) × provable(¬c) → proved/proved returns default (inconsistent), proved/_ prunes else, _/proved prunes then, _/_ checks both with path conds. No backing obligations for pruned branches (CN trusts the solver here). Review fixes: remove dead setState in pure_ error path, add struct preamble to solver initialization, document PEundef divergence (obligation vs immediate failure) and cross-propagation enhancement. solverAssume skips Forall constraints matching CN's solver.ml:1352. Baseline maintained: 74 pass / 4 fail (same pre-existing failures). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ations cvc5 (unlike Z3) requires explicit variable declarations before use. The inline solver in Params.lean built parameter context via Context.addA (which doesn't call solverDeclare) before the solver was created, so parameter symbols were never declared. Added explicit declaration loop after solver initialization. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…entions tryRepackStruct called predicateRequestScan (flat scan only) instead of predicateRequest (scan + recursive repack). This meant nested structs couldn't be repacked from their field resources, failing test 087. Fix: change tryRepackStruct to call predicateRequest for each field, enabling recursive repacking. Wrap tryRepackStruct and predicateRequest in a mutual block since they are now mutually recursive. Also adds DIVERGES-FROM-CN and FIXME comment conventions to CLAUDE.md and tags 4 known divergences in Inference.lean (padding handling, lookupTag failure mode). CN test results: 75/78 (was 74/78, test 087 now passes). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…a-renaming Wave 1 of comprehensive CN audit (see docs/2026-02-18_CN_AUDIT_PLAN.md): SmtLib.lean (WP-A): - Fix *NoSMT operations as uninterpreted functions (was actual arithmetic) - Add full ADT preamble: cn_tuple (0-15), cn_list, cn_option, mem_byte - Fix MemByte encoding (structured ADT instead of Int) - Add CType encoding (Int), EachI unrolling (conjunction) - Add tuple/list/option/map/set/min/max SMT term encodings Simplify.lean (WP-B, new file): - Constraint simplification matching CN simplify.ml - Constant folding, boolean/equality simplification, accessor reduction - Map simplification, ITE simplification, struct eta-reduction DerivedConstraints.lean (WP-C, new file): - Separation logic pointer_facts matching CN resource.ml:24-71 - derivedLc1: hasAllocId, address range no-overflow per resource - derivedLc2: non-overlap constraint for pairs of Owned resources - Integrated into Monad.lean:addR Term.lean + Constraint.lean (WP-D): - Fix alpha-renaming in LogicalConstraint.subst for forall-bound vars - Add freeVarIds, suitablyAlphaRename matching CN indexTerms.ml - Fix all binding forms: eachI, mapDef, let_, match_ Tests (WP-E): 12 new CN test files (090-100) Monad.lean integration: - provable() calls simplifyConstraint before SMT query - addR() derives pointer_facts constraints (separation logic) Test results: 80/90 pass (88%), 0 regressions on existing tests. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Wave 2 of CN audit (docs/2026-02-18_CN_AUDIT_PLAN.md): Expr.lean (WP-G): - Implement ptrEq/ptrNe with hasAllocId obligations (check.ml:1527-1595) - Implement intFromPtr with representability obligation (check.ml:1646-1672) - DIVERGES-FROM-CN: simplified provenance handling, post-hoc obligations Pexpr.lean (WP-H): - Add nil/cons list constructors (check.ml:554-583) - Add ctype_width function call handler (check.ml:851-858) Spine.lean (WP-J): - Implement ghost argument handling with separate gargs list - Type-check ghost args and substitute into rest of AT (check.ml:1174-1176) - Add error cases for ghost arg count mismatches Test results: 83/90 pass (92%), +3 newly passing (066, 094, 095). Remaining 7 failures: SeqRMW (2), arrays (1), parser gaps (4). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
SeqRMW (sequential read-modify-write) for pre/post-increment was stubbed out with an error. CN itself doesn't support SeqRMW (assert_error in core_to_mucore.ml), but our Core IR preserves it for i++ operations. Changes: - Action.lean: Implement SeqRMW as load+compute+store with param slot detection. For parameter stack slots, read/update param value map instead of consuming Owned resources. For non-param pointers, use normal resource-based load/store. - Action.lean: Add param slot fallback to handleStore and handleKill. When no Owned resource is found AND the pointer is a param stack slot, update the param value (store) or silently succeed (kill) instead of failing. This correctly handles value-parameter mutations (++i) without affecting pointer-parameter dereferences (*p = x) which find their Owned resources normally. - Monad.lean: Add alias resolution to lookupParamValue. When an alias entry holds a stale symbolic reference to a primary param, follow the reference to get the current value. Needed for correct return values after param mutation. Test results: 84/90 (93%), up from 83/90. Test 070 (increments with pointer dereference) now passes via SeqRMW. Test 044 inc_post passes (SeqRMW on value param). Test 044 inc_pre still fails (needs Loaded value pattern matching in lazy muCore). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Implement ghost statement processing for CN inline annotations (cn_have, cn_assert, split_case, etc.) with full symbol resolution and store value substitution, matching CN's compile.ml translation pipeline. Key changes: - Parse cerb::magic attributes from Core annotations (Annot.lean, Parser.lean) - Parse ghost statement text (cn_have(expr), etc.) in CN/Parser.lean - Detect ghost statements in Esseq handler: unit-pattern + Epure(Vunit) + cerb::magic attributes (Expr.lean), matching core_to_mucore.ml:535-593 - Resolve placeholder symbols (id=0) against typing context via new resolveContextFromTypingContext (Resolve.lean), matching compile.ml:689-705 - Substitute stored values for stack slot references, following the value chain pattern_var -> .sym ptrSym -> store[ptrSym.id] (Resolve.lean) - Ghost statement handlers: have, assert, split_case, print, with explicit failure for predicate-dependent statements (GhostStatement.lean) - Fix SMT preamble: emit solverBasicsPreamble (tuples, lists, options, mem_byte, pointers) instead of only pointerPreamble (SmtSolver.lean) - Array resource unpacking/repacking + QPredicate request (Inference.lean) Test 096-ghost-have now passes. Pass rate: 84/90 (93%), no regressions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…y matching Implement four new CN features bringing pass rate from 84/90 to 88/90 (97%): - Loop invariants (098): Parse loop_attributes from JSON, build label types with computational args + Owned resources + invariant constraints - Global accesses (099): accesses clause symbol resolution, implicit Owned resource generation in pre/postcondition, global address in context - Ghost parameters (100): cn_ghost parsing, fresh symbols in resolver, ghost entries in caller FT, call-site annotation parsing and resolution - Array resource matching (091): cross-type integer comparison (z vs bits), cast handling in termSyntacticEq Also fixes Action.lean Kill/Store regression from early-return param check. Remaining: 044 (Loaded value pattern matching), 097 (QPredicate/focus). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…lification (90/90) - Implement handleExtract for focus/extract ghost statements with QPredicate element extraction, permission guard update, and P resource absorption - Add alpha-renaming in qpredicateRequest so precondition/postcondition each clauses with different fresh quantifier variable IDs match correctly - Add tryExtractQPIndex for structural pointer template unification - Add mapGet base type resolution (extract value type from Map(K,V)) - Add each resource parsing, map subscript parsing, array_shift resolution - Add QPredicate quantifier variable scoping in resolveQPredicate - Add Q constant arithmetic, Rem/Mod<=n-1 simplification, negate(Q) - Fix pointer type compatibility check in predicateRequestScan Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…0/90) WP-5A: Implement ordered pointer comparisons (PtrLt, PtrGt, PtrLe, PtrGe) - checkBothEqAlloc helper for same-provenance requirement - CN: gtPointer(a,b) = ltPointer(b,a), gePointer(a,b) = lePointer(b,a) WP-5B: Implement remaining pointer memops - Ptrdiff: (addr(p1) - addr(p2)) / sizeof(elem_type) - PtrFromInt: fresh pointer, constrain null or hasAllocId+addr match - CopyAllocId: combine address and allocation ID from different pointers WP-5C: SMT term completeness - CLZ/CTZ via recursive binary decomposition (solver.ml:572-613) - FFS = (x==0)?0:(ctz(x)+1), FLS = (x==0)?0:(width-clz(x)) - Exp constant folding for integer exponents - Default values as cn_val(cn_none(sort)) - Record terms encoded as tuples WP-5D: Representable/good improvements - good(ct, val) implemented (same as representable, pointer alignment TODO) - Floating point representable returns true Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Wave 6 (WP-6C): Fix capture-avoiding substitution in LAT.subst, AT.subst, and LRT.subst — alpha-rename bound variables that conflict with substitution, matching CN's suitably_alpha_rename calls. Make freshSymFor public for reuse across modules. Wave 7 (WP-7A+7B): Port 13 CN tests (6 error + 7 passing) covering pointer relop/diff errors, int-to-ptr, unconstrained ptr_eq, array shift mismatch, division/mod sign errors, bitwise ops, block type, and integer constant bounds. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
… (103/103) WP-A (SmtLib): WrapI bv_cast, Rem mod->rem, mapConst CVC5 workaround, record member/update, struct terms proper AST, struct decl reporting WP-B (Resolve): ltPointer for Loc, array_shift fail, mapGet fail, resolveAnnotTerm verify, global fail, addr_eq extract addr, substStoreValues exhaustive traversal WP-C (Parser): each step type fail, remove <</>>, binopPrec fail, char signedness documented WP-D (Expr/Pexpr/Action): Fence fail, Eunseq always tuple, conv_int non-Bits fail, ghost stmt/arg parse error reporting, quality fixes WP-E (Types/Simplify): Clause.subst in resources, QPredicate/ReturnType alpha-rename, freeVarIds pattern vars, BaseType.beq, cast identity, WrapI folding, struct identity, predicateRequestScan iterate, removeA Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…, splitCase cleanup - Simplify.lean: add SimCtxt with symEqs + typeEnv, thread through all recursive calls. Implements GAP-16 (symbol value substitution), GAP-17 (WrapI constant folding), GAP-18 (Cast identity elimination via BaseType.beq), GAP-20 (SizeOf evaluation via sizeof_). - Inference.lean: add nothing_more_needed permission coverage check after QPredicate matching (GAP-7). Uses forall(q, req(q) => matched(q)). - Monad.lean: build SimCtxt in provable() from typing state symEqs and tagDefs. Add optional freshCounter param to TypingState.empty/withContext. - Params.lean + File.lean + CN.lean: compute file-wide maxSymId to initialize fresh counters, avoiding collisions with parsed symbols (QUALITY-4). - GhostStatement.lean: add provable/refuted checks to splitCase (cases 1-2 from CN check.ml:2262-2283). Case 3 (neither provable) honestly marked DIVERGES-FROM-CN — CN forks the entire continuation, requiring CPS. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…/103) Replace dbg_trace + silent continue with proper error propagation: - Params: invariant parse/resolve errors, missing loop C types, unknown accesses globals - Params/Check: solver startup failure now fails instead of proceeding without SMT - Simplify: sizeOf failure panics instead of returning unsimplified term - SmtLib: struct preamble generation propagates unsupported field type errors - Expr: case branch errors accumulated and reported in failure message Also fixes loop invariant resolve context to include loop variables (was missing, causing all invariant constraints to silently fail resolution). 098-loop-invariant now fails with SMT serialization error -- the test was previously passing only because invariants were silently dropped. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…s (103/103) Loop invariant constraints referenced pointer symbols (Loc type) instead of loaded value symbols (e.g. bits signed 32), causing SMT sort mismatches. buildLoopLabelType now pre-computes output symbols and uses them in both the resolve context and resource bindings, matching CN's make_label_args spine. Also adds mkIndexedApp1/mkAsLiteral/mkIsTester helpers in SmtLib.lean to centralize the literalT workaround for SMT-LIB2 indexed identifiers (lean-smt's appToList flattens mkApp nodes, breaking indexed id application). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Snapshot taken 2026-07-29 during a pre-wipe backup audit of ~/Projects. Compile and proof state NOT verified — this commit exists to preserve bytes, not to represent a working checkpoint. 13 modified files (CN/Parser, CN/TypeChecking/*, CN/Types/*, CN/Verification/SmtLib) plus a new docs/2026-02-26_CN_AUDIT_REPORT.md. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.