aprender-contracts-cli 0.60.0

CLI for provable-contracts — validate, scaffold, verify, status, audit
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

metadata:
  version: "1.0.0"
  description: "Clamp kernel — saturating bound"
  references:
    - "IEEE 754-2019"

equations:
  clamp:
    formula: "y_i = min(max(x_i, lo), hi)"
    domain: "x ∈ ℝ^n, lo ≤ hi"
    codomain: "y ∈ [lo, hi]^n"
    invariants:
      - "lo ≤ y_i ≤ hi for all i"
      - "clamp(clamp(x)) = clamp(x)"
      - "x_i ≤ x_j → y_i ≤ y_j"

proof_obligations:
  - type: bound
    property: "Output in [lo, hi]"
    formal: "lo ≤ y_i ≤ hi for all i"
    applies_to: all
  - type: monotonicity
    property: "Order preservation"
    formal: "x_i ≤ x_j → y_i ≤ y_j"
    applies_to: all
  - type: idempotency
    property: "Idempotent application"
    formal: "clamp(clamp(x)) = clamp(x)"
    applies_to: all
  - type: equivalence
    property: "SIMD matches scalar"
    tolerance: 0.0
    applies_to: simd

kernel_structure:
  phases:
    - name: compare_lo
      description: "Clamp below by lo"
      invariant: "tmp_i = max(x_i, lo)"
    - name: compare_hi
      description: "Clamp above by hi"
      invariant: "y_i = min(tmp_i, hi)"
    - name: store
      description: "Write result"
      invariant: "lo ≤ y_i ≤ hi"

simd_dispatch:
  clamp:
    scalar: clamp_scalar
    avx2: clamp_avx2

falsification_tests:
  - id: FALSIFY-CL-001
    rule: "Bound"
    prediction: "lo <= clamp(x) <= hi for all x"
    if_fails: "Comparison order wrong"

kani_harnesses:
  - id: KANI-CL-001
    obligation: CL-BND-001
    property: "Output within bounds"
    bound: 16
    strategy: exhaustive

qa_gate:
  id: F-CL-001
  name: "Clamp Contract"
  checks:
    - "bound"
  pass_criteria: "All 1 falsification tests pass"