fix: env::get validates UTF-8 (defect-queue item 2) + ordered known-d… #22
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
| name: CI | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| workflow_dispatch: | |
| schedule: | |
| # Weekly clean-checkout proof replay (see the proof-replay job below). | |
| # The regular jobs also run, giving a weekly full-CI signal. | |
| - cron: "17 4 * * 1" | |
| # Nightly differential fuzz campaign with a rotating (date-derived) seed | |
| # (see the fuzz-campaign job below). Fixed CI seeds re-test the same | |
| # programs forever; every fuzzer-found bug came from a fresh seed. | |
| - cron: "23 3 * * *" | |
| jobs: | |
| grammar: | |
| name: LL(1) grammar check | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Workflow-YAML gate (every workflow file parses) | |
| run: | | |
| python3 -m pip install --quiet pyyaml || true | |
| bash scripts/tests/check_workflow_yaml.sh | |
| - name: Gate-hygiene gate (every gate is pipe-safe and fails loudly) | |
| run: bash scripts/tests/check_gate_hygiene.sh | |
| - name: Constructor-coverage gate (every walker handles every constructor) | |
| run: bash scripts/tests/check_constructor_coverage.sh | |
| - name: Run Python LL(1) checker | |
| run: python3 scripts/check_ll1.py grammar/concrete.ebnf | |
| - name: Run C LL(1) checker | |
| run: | | |
| cc -Wall -Wextra -Werror -O2 -o /tmp/check_ll1 scripts/check_ll1.c | |
| /tmp/check_ll1 grammar/concrete.ebnf | |
| - name: Run Rust LL(1) checker | |
| run: | | |
| rustc -O -o /tmp/check_ll1_rs scripts/check_ll1.rs | |
| /tmp/check_ll1_rs grammar/concrete.ebnf | |
| build: | |
| name: Build | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Check for build warnings | |
| run: | | |
| OUTPUT=$(lake build 2>&1) | |
| if echo "$OUTPUT" | grep -i "warning"; then | |
| echo "::error::Build produced warnings" | |
| echo "$OUTPUT" | |
| exit 1 | |
| fi | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| main-tests: | |
| name: Main test suite | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Run main test suite | |
| run: | | |
| for attempt in 1 2 3; do | |
| if SKIP_FLAKY_TCP_TEST=1 ./scripts/tests/run_tests.sh; then | |
| exit 0 | |
| fi | |
| echo "::warning file=run_tests::Main test suite failed on attempt $attempt of 3" | |
| done | |
| exit 1 | |
| - name: Run golden tests (--emit-core / --emit-ssa / --fmt baselines) | |
| run: bash ./scripts/tests/test_golden.sh | |
| macos: | |
| name: Build + main tests (macOS) | |
| runs-on: macos-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Run main test suite | |
| run: | | |
| for attempt in 1 2 3; do | |
| if SKIP_FLAKY_TCP_TEST=1 ./scripts/tests/run_tests.sh; then | |
| exit 0 | |
| fi | |
| echo "::warning file=run_tests::Main test suite failed on attempt $attempt of 3 (macOS)" | |
| done | |
| exit 1 | |
| proof-replay: | |
| name: Weekly clean-checkout proof replay | |
| # Fresh checkout with no build caches: rebuild everything and re-run the | |
| # proof/theorem gates so a stale cache can never produce a false green. | |
| # Guarded to the WEEKLY cron so the nightly fuzz cron does not trigger it. | |
| # Crons run ONLY on the canonical public repo (lambdaclass/concrete) — | |
| # the working repo mirrors the tree, doubling nightly compute for nothing. | |
| if: ((github.event_name == 'schedule' && github.event.schedule == '17 4 * * 1') && github.repository == 'lambdaclass/concrete') || github.event_name == 'workflow_dispatch' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action, caches disabled) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| use-github-cache: false | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Run proof evidence gate (Lean kernel theorem checking) | |
| run: bash scripts/ci/proof_gate.sh | |
| - name: Lean-replay gate (SMT -> kernel upgrade artifact) | |
| run: bash scripts/tests/check_smt_replay.sh | |
| - name: Proof-patterns corpus gate | |
| run: bash scripts/tests/check_proof_patterns.sh | |
| - name: Axiom-inventory gate (docs/AXIOMS.md stays honest) | |
| run: bash scripts/tests/check_axiom_inventory.sh | |
| fuzz-campaign: | |
| name: Nightly differential fuzz (rotating seed) | |
| if: ((github.event_name == 'schedule' && github.event.schedule == '23 3 * * *') && github.repository == 'lambdaclass/concrete') || github.event_name == 'workflow_dispatch' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Fuzz campaign (date-derived seed, depth 3 + depth 4) | |
| run: | | |
| SEED=$(date -u +%Y%m%d) | |
| echo "seed: $SEED" | |
| python3 scripts/tests/fuzz_differential.py --n 2000 --seed "$SEED" --depth 3 | |
| python3 scripts/tests/fuzz_differential.py --n 500 --seed "$SEED" --depth 4 | |
| - name: Linearity fuzz campaign (ground-truth conservation oracle, rotating seed) | |
| run: | | |
| SEED=$(date -u +%Y%m%d) | |
| python3 scripts/tests/fuzz_linearity.py --n 400 --seed "$SEED" | |
| - name: Gate mutation coverage (Phase 6C #5 — heavy; rebuilds per mutation) | |
| run: bash scripts/tests/check_gate_mutation_coverage.sh | |
| - name: Upload failing case (if any) | |
| if: failure() | |
| uses: actions/upload-artifact@v4 | |
| with: | |
| name: fuzz-fail-${{ github.run_id }} | |
| path: fuzz_fail.con | |
| if-no-files-found: ignore | |
| ssa-tests: | |
| name: SSA test suite | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Run SSA test suite | |
| run: SKIP_FLAKY_TCP_TEST=1 bash ./scripts/tests/test_ssa.sh | |
| trust-gate: | |
| name: Trust gate (correctness contracts) | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Run trust gate | |
| run: ./scripts/tests/run_tests.sh --trust-gate | |
| proof-gate: | |
| name: Proof evidence gate | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Run proof evidence gate | |
| run: bash scripts/ci/proof_gate.sh | |
| - name: Evidence-class corpus integrity gate | |
| run: bash scripts/tests/check_evidence_corpus.sh | |
| - name: Registry-retirement gate (examples are source-linked, no JSON) | |
| run: bash scripts/tests/check_no_example_registries.sh | |
| - name: Proof-namespace guard (example proofs stay under Examples.*) | |
| run: bash scripts/tests/check_proof_namespace.sh | |
| - name: Proof-patterns corpus gate | |
| run: bash scripts/tests/check_proof_patterns.sh | |
| - name: Contract-negatives gate (source-contract hardening) | |
| run: bash scripts/tests/check_contract_negatives.sh | |
| - name: Contract-stability gate (contract API drift) | |
| run: bash scripts/tests/check_contract_stability.sh | |
| - name: Phase 1 contracts validation artifact (umbrella + snapshots) | |
| run: bash scripts/tests/check_phase1_contracts.sh | |
| - name: VC schema v1 gate (Phase 2 foundation) | |
| run: bash scripts/tests/check_vc_schema.sh | |
| - name: ProofKit arithmetic-bridge gate (Phase 2 library) | |
| run: bash scripts/tests/check_proofkit_arith.sh | |
| - name: External-SMT path gate (Phase 2 trust boundary) | |
| run: bash scripts/tests/check_smt_path.sh | |
| - name: SMT release-policy gate (Phase 2 evidence governance) | |
| run: bash scripts/tests/check_smt_policy.sh | |
| - name: Lean-replay gate (Phase 2 SMT→kernel upgrade artifact) | |
| run: bash scripts/tests/check_smt_replay.sh | |
| - name: SMT negatives gate (Phase 2 honesty boundaries) | |
| run: bash scripts/tests/check_smt_negatives.sh | |
| - name: VC/discharge example matrix gate (Phase 2 status references) | |
| run: bash scripts/tests/check_vc_discharge_examples.sh | |
| - name: External-SMT teaching group gate (Phase 2 when-useful/when-refused) | |
| run: bash scripts/tests/check_smt_examples.sh | |
| - name: Red-team VC/SMT gate (Phase 2 adversarial) | |
| run: bash scripts/tests/check_smt_redteam.sh | |
| - name: End-of-Phase-2 VC/SMT examples gate | |
| run: bash scripts/tests/check_vc_examples.sh | |
| - name: Operational-VC-auto-discharge forcing-probe gate (Phase 9 #16a) | |
| run: bash scripts/tests/check_operational_vc_auto_discharge.sh | |
| - name: Phase 2 VC/discharge validation artifact (umbrella) | |
| run: bash scripts/tests/check_phase2_vc.sh | |
| - name: ObligationCore ledger gate (Phase 3 schema + vocabulary) | |
| run: bash scripts/tests/check_obligation_core.sh | |
| - name: Unified scoped-collector gate (Phase 3 #3 adversarial) | |
| run: bash scripts/tests/check_scoped_collector.sh | |
| - name: Call-site precondition migration gate (Phase 3 #4 parity+improvement) | |
| run: bash scripts/tests/check_call_site_migration.sh | |
| - name: Array-bounds migration gate (Phase 3 #5 parity+improvement) | |
| run: bash scripts/tests/check_bounds_migration.sh | |
| - name: Div/mod + sound-lowering migration gate (Phase 3 #6 parity+improvement) | |
| run: bash scripts/tests/check_div_migration.sh | |
| - name: Overflow migration gate (Phase 3 #7 three-route parity+trust-boundary) | |
| run: bash scripts/tests/check_overflow_migration.sh | |
| - name: Assert/assume migration gate (Phase 3 #8 ledger fact + no-laundering) | |
| run: bash scripts/tests/check_assume_migration.sh | |
| - name: Loop-obligation migration gate (Phase 3 #9 O1-O5 scoped + split status) | |
| run: bash scripts/tests/check_loop_migration.sh | |
| - name: Contract-clause migration gate (Phase 3 #10 ledger diagnostics + partial) | |
| run: bash scripts/tests/check_contract_clause_migration.sh | |
| - name: Proof-link freshness migration gate (Phase 3 #11 proof-status in the ledger) | |
| run: bash scripts/tests/check_proof_link_migration.sh | |
| - name: Obligation-expression lowering gate (Phase 3 #12 shared lowering layer) | |
| run: bash scripts/tests/check_obligation_lowering.sh | |
| - name: Backend discharge-adapter gate (Phase 3 #13 evidence-class firewall) | |
| run: bash scripts/tests/check_discharge_adapters.sh | |
| - name: Reports-as-views gate (Phase 3 #15 ledger consistency) | |
| run: bash scripts/tests/check_obligation_report_views.sh | |
| - name: Contracts↔ledger parity gate (Phase 3 #15/#18e) | |
| run: bash scripts/tests/check_contracts_ledger_parity.sh | |
| - name: No-duplicate-obligation-walkers guard (Phase 3 #18d) | |
| run: bash scripts/tests/check_no_duplicate_obligation_walkers.sh | |
| - name: Single-truth-source guard (Phase 3 #18d step 5) | |
| run: bash scripts/tests/check_obligation_single_truth_source.sh | |
| - name: Policy-as-ledger-view gate (Phase 3 #14) | |
| run: bash scripts/tests/check_obligation_policy_views.sh | |
| - name: prove-as-ledger-view gate (Phase 3 #16) | |
| run: bash scripts/tests/check_obligation_prove_views.sh | |
| - name: Phase 3 capstone — ObligationCore single truth source (umbrella) | |
| run: bash scripts/tests/check_phase3_obligation_core.sh | |
| - name: ObligationCore red-team gate (Phase 3 hardening) | |
| run: bash scripts/tests/check_obligation_redteam.sh | |
| language-gates: | |
| name: Language-surface gates (Phase 5-6) | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Module/import/visibility gate (Phase 5 #1) | |
| run: bash scripts/tests/check_module_visibility.sh | |
| - name: Project-model gate (Phase 5 #2 — Concrete.toml structure) | |
| run: bash scripts/tests/check_project_model.sh | |
| - name: "`concrete test` gate (Phase 5 #3 — project test runner)" | |
| run: bash scripts/tests/check_concrete_test.sh | |
| - name: Diagnostics-quality gate (Phase 5 #4 — span floor) | |
| run: bash scripts/tests/check_diagnostics_quality.sh | |
| - name: ByteView gate (Phase 5 #5a — owned stored zero-copy view) | |
| run: bash scripts/tests/check_byte_view.sh | |
| - name: Collections gate (Phase 5 #6 — H1-clean collection surface) | |
| run: bash scripts/tests/check_collections.sh | |
| - name: "`concrete fmt` gate (Phase 6 #1 — subcommand + semantics-preserving)" | |
| run: bash scripts/tests/check_concrete_fmt.sh | |
| - name: Loop-control gate (Phase 6 #4 — break/continue/while-expr + linear cleanup) | |
| run: bash scripts/tests/check_loop_control.sh | |
| - name: Type-alias gate (Phase 6 #3 — transparency + no-new-identity) | |
| run: bash scripts/tests/check_type_alias.sh | |
| - name: Pattern-ergonomics gate (Phase 6 #5 — range patterns) | |
| run: bash scripts/tests/check_pattern_ergonomics.sh | |
| - name: Lex-escapes gate (unknown escapes are E0001, never silently mangled) | |
| run: bash scripts/tests/check_lex_escapes.sh | |
| - name: Mixed-width binop gate (E0228 + flexible literals + interp cast normalization) | |
| run: bash scripts/tests/check_mixed_width_binops.sh | |
| - name: Type-agreement gate (Phase 6.5 #9 — Check/Elab type through one TypeJudgment) | |
| run: bash scripts/tests/check_type_agreement.sh | |
| - name: "Differential-position gate (flexible overflow / signed shift, interp == compiled)" | |
| run: bash scripts/tests/check_differential_positions.sh | |
| - name: "Copy-judgment gate (Phase 6.5 — one Copy judgment shared by Check and Core)" | |
| run: bash scripts/tests/check_copy_judgment.sh | |
| - name: "Ownership-judgment matrix (Check == Lower move/drop == interp consumption)" | |
| run: bash scripts/tests/check_ownership_judgment.sh | |
| - name: "Totality-judgment matrix (trap/divergence facts agree interp == compiled)" | |
| run: bash scripts/tests/check_totality_judgment.sh | |
| - name: "CoreCheck boundary gate (residue classes rejected before Lower)" | |
| run: bash scripts/tests/check_corecheck_boundary.sh | |
| - name: "Capability-judgment gate (Phase 6.5 — one direct-call capability decision)" | |
| run: bash scripts/tests/check_capability_judgment.sh | |
| - name: "Pipeline-refactor contract (Phase 6B capstone — behavior-preserving + fail-closed)" | |
| run: bash scripts/tests/check_pipeline_refactor_contract.sh | |
| - name: "Pipeline telemetry trace (Phase 6C #1 — stable-schema JSON, no private paths)" | |
| run: bash scripts/tests/check_pipeline_telemetry.sh | |
| - name: "SSA-verify behavior preservation (trust pass keeps its verdicts on complex CFGs)" | |
| run: bash scripts/tests/check_ssa_verify_agreement.sh | |
| - name: "Compiler complexity guard (Phase 6C #2 — no super-linear pass on scaling corpus)" | |
| run: bash scripts/tests/check_compiler_complexity.sh | |
| - name: "O(n^2) append ratchet (no new `xs ++ [x]` in hot pipeline files)" | |
| run: bash scripts/tests/check_no_quadratic_append.sh | |
| - name: "Pipeline trace (Phase 6C #3 — per-stage --trace-pipeline names the first failing phase)" | |
| run: bash scripts/tests/check_trace_pipeline.sh | |
| - name: "Counterexample reduction (Phase 6C #4 — failures reduce to a minimized fixture + replay)" | |
| run: bash scripts/tests/check_counterexample_reduction.sh | |
| - name: "Phase 6D capstone (surface simplified, semantics unweakened)" | |
| run: bash scripts/tests/check_phase6d_surface_simplification.sh | |
| - name: "CLI coherence (Phase 6E — context-free help, alias identity, legacy compat)" | |
| run: bash scripts/tests/check_cli_coherence.sh | |
| - name: "Doc snippets compile (13r — con/concrete fences compile, reject as declared, or marked pseudocode)" | |
| run: bash scripts/tests/check_doc_snippets.sh | |
| - name: "Stdlib five-fact manifest (P7 2a — complete, no blanks, signature-agreeing; 2b method-canonical)" | |
| run: bash scripts/tests/check_stdlib_manifest.sh | |
| - name: "IO Writer spine (P7 14a — fn-ptr handle; acquisition authority; no-Alloc fixed sink; one shape)" | |
| run: bash scripts/tests/check_io_writer.sh | |
| - name: "Collections Copy-only status quo (H18 — non-Copy element destruction pinned as disclosed hole)" | |
| run: bash scripts/tests/check_collections_copy_only.sh | |
| - name: "std.test oracle layer (P7 step 5 — silent/cap-free expects, Console-visible asserts, stable messages, no xUnit)" | |
| run: bash scripts/tests/check_std_test.sh | |
| - name: "Bytes/Text boundary (P7 #4 — raw bytes vs validated UTF-8; checked or named-unchecked crossings only)" | |
| run: bash scripts/tests/check_bytes_text_boundary.sh | |
| - name: "Error conventions (13t — the three buckets report-visible: E0286 / trap_sites / caps)" | |
| run: bash scripts/tests/check_error_conventions.sh | |
| - name: "Exit codes (MAIN_EXIT_MODEL stage 1 — main return = process status, clean stdout; echo only behind the harness knob)" | |
| run: bash scripts/tests/check_exit_codes.sh | |
| - name: "Stdlib hardening (P7 item 0, H1-H5 class gates + unproven-content check)" | |
| run: bash scripts/tests/check_std_hardening.sh | |
| - name: "Pure-core proofs (slice 1 — kernel-verified stdlib proof link, mutation-sensitive)" | |
| run: bash scripts/tests/check_purecore_proofs.sh | |
| - name: "Workload 3: hexdump differential vs xxd + exit codes" | |
| run: bash scripts/tests/check_hexdump_differential.sh | |
| - name: "std.cli v1: cli_tool matrix + bug-034 regression + proof-of-pull" | |
| run: bash scripts/tests/check_cli_helpers.sh | |
| - name: "Workload 4: tar_list differential vs tar -tf + exit codes" | |
| run: bash scripts/tests/check_tar_list_differential.sh | |
| - name: "Builtin semantics: interp == compiled per builtin + inventory pin" | |
| run: bash scripts/tests/check_builtin_semantics.sh | |
| - name: "Workload 5: envcfg env-override matrix + exit codes + bug-039 leg" | |
| run: bash scripts/tests/check_envcfg.sh | |
| - name: "std compiled coverage: one compiled behavioral fixture per std module (fail-closed inventory)" | |
| run: bash scripts/tests/check_std_compiled_coverage.sh | |
| - name: "Pass-output hashes (Phase 6C #6 — per-stage replay manifest; determinism + position-free vs position-bearing)" | |
| run: bash scripts/tests/check_pass_hashes.sh | |
| - name: "Incremental shadow (Phase 6C #7 — reuse/invalidate prediction + no-false-reuse over an edit corpus)" | |
| run: bash scripts/tests/check_incremental_shadow.sh | |
| - name: "Phase 6C observability capstone (#8 — telemetry, complexity, trace, reduction, mutation sample, hashes, shadow)" | |
| run: bash scripts/tests/check_phase6c_observability.sh | |
| - name: Trailing-value gate (if/match as value-block trailing values) | |
| run: bash scripts/tests/check_trailing_value_blocks.sh | |
| - name: Submodule-checking gate (KNOWN_HOLES H12 — user sub-file bodies checked; std exemption disclosed) | |
| run: bash scripts/tests/check_submodule_check_coverage.sh | |
| - name: Struct-update gate (Phase 6 #5 — S { ..base }) | |
| run: bash scripts/tests/check_struct_update.sh | |
| - name: No-tuples decision gate (Phase 6 #5 — tuple syntax stays rejected) | |
| run: bash scripts/tests/check_no_tuples.sh | |
| - name: Nested-patterns decision gate (Phase 6 #5 — one level/arm + workarounds) | |
| run: bash scripts/tests/check_nested_patterns.sh | |
| - name: Numeric-literals gate (Phase 6 #6 — out-of-range literals rejected) | |
| run: bash scripts/tests/check_numeric_literals.sh | |
| - name: defer gate (Phase 6 #7 — LIFO cleanup on every exit path) | |
| run: bash scripts/tests/check_defer.sh | |
| - name: Ignored-result gate (Phase 6 #13 — discarded Result/Option rejected unless acknowledged) | |
| run: bash scripts/tests/check_ignored_result.sh | |
| - name: Array-bounds gate (KNOWN_HOLES H8 — raw a[i] runtime-checked; OOB read/write/negative/nested/&mut trap) | |
| run: bash scripts/tests/check_array_bounds.sh | |
| - name: Error-leak gate (bug 024 — recursive/edge inputs give a clean diagnostic, not an llvm-as/ld/panic leak) | |
| run: bash scripts/tests/check_error_leaks.sh | |
| - name: Source-span gate (every pass anchors its diagnostic to the original source line) | |
| run: bash scripts/tests/check_source_spans.sh | |
| - name: Pipeline-contracts gate (Phase 6.5 #3 — each boundary violation caught at the first responsible pass, no leak) | |
| run: bash scripts/tests/check_pipeline_contracts.sh | |
| - name: Capability-facts gate (Phase 6.5 #5 — checker verdict and report rendering read one capability-fact source) | |
| run: bash scripts/tests/check_capability_facts.sh | |
| - name: Linear-discard gate (KNOWN_HOLES H6 — silent discard of a non-Copy value rejected; let _/free/consumed compile) | |
| run: bash scripts/tests/check_linear_discard.sh | |
| - name: Nested-scope linearity gate (KNOWN_HOLES H9 — branch/arm local must be consumed; move-through-let; while-true/abort exempt) | |
| run: bash scripts/tests/check_linear_nested_scope.sh | |
| - name: Linear-conservation gate (every value-flow site moves a linear value exactly once — array-lit/struct-lit/destructure/arg/return/match; no duplication) | |
| run: bash scripts/tests/check_linear_conservation.sh | |
| - name: Value-flow spec coverage gate (ROADMAP 13c — every AST constructor must have a value-flow row in docs/VALUE_FLOW_SPEC.md) | |
| run: bash scripts/tests/check_value_flow_spec.sh | |
| - name: Diagnostic-code ledger completeness (ROADMAP 13m — every emittable E-code has a --report diagnostic-codes entry) | |
| run: bash scripts/tests/check_diagnostic_codes_complete.sh | |
| - name: Linearity fuzz smoke (deterministic seed — consume-once compiles, leak/dup/shadow/param-sink reject) | |
| run: python3 scripts/tests/fuzz_linearity.py --n 40 --seed 20260706 | |
| - name: Macro-stance gate (Phase 6 #11 — no v1 macros) | |
| run: bash scripts/tests/check_no_macros.sh | |
| - name: Red-team gate (Phase 6 #35a — recovery / match / fingerprint / stale fixtures) | |
| run: bash scripts/tests/check_phase6_redteam.sh | |
| - name: Stdlib handoff gate (Phase 6 #19 — required surfaces stable/provisional, none blocked) | |
| run: bash scripts/tests/check_stdlib_handoff.sh | |
| - name: Build-profiles gate (Phase 6 #10 Stage 1 — profile mechanism + reporting, no codegen) | |
| run: bash scripts/tests/check_build_profiles.sh | |
| - name: Iteration-protocol gate (Phase 6 #17 — blessed traversal forms; no Iterator trait) | |
| run: bash scripts/tests/check_iteration_protocol.sh | |
| - name: Wrapping-arith gate (Phase 6 #10 Stage 2.1 — wrapping_* wrap correctly, integer-only) | |
| run: bash scripts/tests/check_wrapping_arith.sh | |
| - name: Saturating-arith gate (Phase 6 #10 Stage 2.2 — saturating_add/sub clamp, integer-only) | |
| run: bash scripts/tests/check_saturating_arith.sh | |
| - name: Checked-arith gate (Phase 6 #10 Stage 2.3 — ordinary + traps on overflow; wrapping_* escapes) | |
| run: bash scripts/tests/check_checked_arith.sh | |
| - name: Int-arith semantics gate (Phase 6.5 #1 — interpret == fold-then-interpret == compiled; trap preservation under folding) | |
| run: bash scripts/tests/check_int_arith_semantics.sh | |
| - name: Arithmetic red-team gate (Phase 6 #10 — overflow/neg/div-mod/shift traps + interp==compiled value agreement) | |
| run: bash scripts/tests/check_arith_redteam.sh | |
| - name: "Report-arithmetic gate (Phase 6 #10 §3.2 — per-site classification: checked/proved/wrapping/saturating)" | |
| run: bash scripts/tests/check_report_arithmetic.sh | |
| - name: Memory-model gate (Phase 6 #33 — no uninitialized reads by construction) | |
| run: bash scripts/tests/check_memory_model.sh | |
| infra-gates: | |
| name: Compiler-infra gates (ledger, diagnostics, codegen, CLI, known holes) | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: CompilerLedger gate (Phase 4 #2 — non-proof fact store) | |
| run: bash scripts/tests/check_compiler_ledger.sh | |
| - name: Docs-drift gate (Phase 4 #44 — present-tense docs reference only real artifacts) | |
| run: bash scripts/tests/check_docs_drift.sh | |
| - name: Rich-diagnostics gate (Phase 4 #4 — human/JSON from one record) | |
| run: bash scripts/tests/check_rich_diagnostics.sh | |
| - name: Partial-facts gate (Phase 4 #12a — error-tolerant diagnostics) | |
| run: bash scripts/tests/check_partial_facts.sh | |
| - name: Source-maps gate (Phase 4 #13a — spans survive AST→Core) | |
| run: bash scripts/tests/check_source_maps.sh | |
| - name: Callable-values/capability design gate (Phase 5 #24a — fn-ptr smuggling closed, HOF freeze) | |
| run: bash scripts/tests/check_capability_polymorphism_design.sh | |
| - name: Callable-values gate (Phase 5 #24 step 1 — context modes; &mut *ctx reborrow aliases) | |
| run: bash scripts/tests/check_callable_values.sh | |
| - name: Returned-ref provenance known-hole gate (aggregate-ref public API freeze) | |
| run: bash scripts/tests/check_returned_ref_provenance.sh | |
| - name: Proven-violation enforcement known-hole gate (constant OOB / div-zero) | |
| run: bash scripts/tests/check_proven_violation_enforcement.sh | |
| - name: "Checked float-cast gate (float->int NaN/inf/out-of-range abort, in-range truncates — closes H2)" | |
| run: bash scripts/tests/check_float_cast.sh | |
| - name: Mono name-collision known-hole gate (nested-generic specialization merge) | |
| run: bash scripts/tests/check_mono_name_collision.sh | |
| - name: Nested place-write regression gate (compound assignment targets) | |
| run: bash scripts/tests/check_nested_field_write.sh | |
| - name: Raw-ptr-to-local known-hole gate (&mut x does not alias local) | |
| run: bash scripts/tests/check_raw_ptr_to_local.sh | |
| - name: Struct field-layout regression gate (mixed-width store/read agree) | |
| run: bash scripts/tests/check_struct_field_layout.sh | |
| - name: Codegen execution-oracle gate (compile-run-assert value) | |
| run: bash scripts/tests/check_codegen_execution.sh | |
| - name: Codegen differential gate (interpreter vs compiled agreement) | |
| run: bash scripts/tests/check_codegen_differential.sh | |
| - name: Cast-matrix differential gate (every width pair x edge value, interp == compiled) | |
| run: bash scripts/tests/check_cast_matrix.sh | |
| - name: CLI-plumbing gate (Phase 4 #14a — shared prologue + exit-code taxonomy) | |
| run: bash scripts/tests/check_cli_plumbing.sh | |
| - name: CLI-contract gate (Phase 4 #15 — golden command behavior matrix) | |
| run: bash scripts/tests/check_cli_contract.sh | |
| - name: API-boundary gate (Phase 4 #16 — consumers use the boundary, not internals) | |
| run: bash scripts/tests/check_compiler_api_boundary.sh | |
| - name: Backend-contract gate (Phase 4 #17a — codegen guarantees, no drift) | |
| run: bash scripts/tests/check_backend_contracts.sh | |
| - name: concrete prove CLI gate | |
| run: bash scripts/tests/test_prove_cli.sh | |
| thesis-evidence: | |
| name: Thesis evidence smoke test | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Check thesis demo reports | |
| run: | | |
| BIN=".lake/build/bin/concrete" | |
| "$BIN" examples/thesis_demo/src/main.con --report effects | tee /tmp/effects.txt | |
| grep -q 'Evidence: 2 proved' /tmp/effects.txt | |
| grep -q 'evidence: proved' /tmp/effects.txt | |
| "$BIN" examples/thesis_demo/src/main.con --report proof-status | tee /tmp/proof-status.txt | |
| grep -q '2 proved' /tmp/proof-status.txt | |
| grep -q 'proof matches current body' /tmp/proof-status.txt | |
| # The thesis demo intentionally has a predictable core and an I/O entrypoint. | |
| set +e | |
| "$BIN" examples/thesis_demo/src/main.con --check predictable > /tmp/predictable.txt | |
| rc=$? | |
| set -e | |
| test "$rc" -eq 1 | |
| grep -q 'predictable profile: FAIL' /tmp/predictable.txt | |
| grep -q 'may block' /tmp/predictable.txt | |
| examples: | |
| name: Examples (manifest coverage) | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| - name: Check example coverage manifest | |
| # Every .con under examples/ must be listed in | |
| # scripts/tests/example_manifest.txt with its expected outcome | |
| # (compile / project-build / expected-error / skip). The gate fails | |
| # if a new example is added without being classified. | |
| run: EXAMPLES_OUT_DIR=/tmp/concrete_examples_out bash ./scripts/tests/check_examples.sh | |
| - name: Run compiled examples (smoke test) | |
| run: | | |
| CRASH=0 | |
| # Note: tr '/.' '__' yields single underscores (tr maps char-for-char), | |
| # so binaries are named examples_<path>_main_con. | |
| for exe in /tmp/concrete_examples_out/examples_*_main_con; do | |
| [ -f "$exe" ] || continue | |
| case "$exe" in | |
| *net*|*tcp*|*http*|*grep*|*toml*|*lox*|*project*) continue ;; | |
| esac | |
| if [ -x "$exe" ]; then | |
| timeout 5 "$exe" > /dev/null 2>&1 || rc=$? | |
| rc=${rc:-0} | |
| if [ "$rc" -eq 139 ] || [ "$rc" -eq 134 ] || [ "$rc" -eq 136 ]; then | |
| echo "CRASH (exit $rc): $exe" | |
| CRASH=$((CRASH + 1)) | |
| fi | |
| fi | |
| done | |
| echo "=== Runtime crashes: $CRASH ===" | |
| if [ "$CRASH" -gt 0 ]; then | |
| exit 1 | |
| fi | |
| extra-gates: | |
| name: Extra gates (dark-gate wiring, audit 2026-07-16) | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean (via lean-action) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| build-args: "--log-level=warning" | |
| - name: Install clang | |
| run: sudo apt-get update && sudo apt-get install -y clang | |
| # These gates had Makefile targets but zero CI coverage ("dark gates") — | |
| # test_wrong_code was already silently red (WC-0005's stale expectation) | |
| # when wired here. One job, fail-fast per step. | |
| - name: Catches (negative corpus) | |
| run: bash ./scripts/tests/check_catches.sh | |
| - name: Showcase corpus | |
| run: bash ./scripts/tests/check_showcase.sh | |
| - name: Wrong-code corpus | |
| run: bash ./scripts/tests/test_wrong_code.sh | |
| - name: Reducer smoke | |
| run: bash ./scripts/tests/test_reducer_smoke.sh | |
| - name: Release bundle | |
| run: bash ./scripts/tests/test_release_bundle.sh | |
| - name: Float-literal rounding corpus | |
| run: bash ./scripts/tests/check_float_literals.sh | |
| - name: Enum union layout | |
| run: bash ./scripts/tests/check_enum_union_layout.sh | |
| - name: string_char_at differential | |
| run: bash ./scripts/tests/check_string_char_at.sh |