1  (*
  2    argon2-checks.dats: ATS2 shadow model for Argon2id parameter validation
  3  
  4    Non-authoritative: intended for CI shadow verification only.
  5    This checks that keystore policy parameters satisfy constraints
  6    without implementing actual Argon2id (that's the SPARK core's job).
  7  
  8    Checks:
  9      - salt_bytes in [16, 32]
 10      - hash_bytes in [32, 64]
 11      - parallelism in [1, 8]
 12      - memory_kib in [65536, 1048576]
 13      - time_cost in [2, 10]
 14      - profile name is valid
 15      - upgrade only increases parameters
 16  *)
 17  
 18  #include "share/atspre_define.hats"
 19  #include "share/atspre_staload.hats"
 20  
 21  staload UN = "prelude/SATS/unsafe.sats"
 22  
 23  (* --- Constraint bounds from spec/keystore-policy.json --- *)
 24  
 25  val SALT_BYTES_MIN: int = 16
 26  val SALT_BYTES_MAX: int = 32
 27  val HASH_BYTES_MIN: int = 32
 28  val HASH_BYTES_MAX: int = 64
 29  val PARALLELISM_MIN: int = 1
 30  val PARALLELISM_MAX: int = 8
 31  val MEMORY_KIB_MIN: int = 65536
 32  val MEMORY_KIB_MAX: int = 1048576
 33  val TIME_COST_MIN: int = 2
 34  val TIME_COST_MAX: int = 10
 35  
 36  (* --- Types --- *)
 37  
 38  typedef argon2_params = @{
 39    salt_bytes = int,
 40    hash_bytes = int,
 41    parallelism = int,
 42    memory_kib = int,
 43    time_cost = int
 44  }
 45  
 46  typedef validation_result = @{
 47    valid = bool,
 48    error_msg = string
 49  }
 50  
 51  (* --- Validation functions --- *)
 52  
 53  fun
 54  validate_salt_bytes(p: int): validation_result =
 55    if p < SALT_BYTES_MIN then
 56      @{ valid = false, error_msg = "salt_bytes below minimum (16)" }
 57    else if p > SALT_BYTES_MAX then
 58      @{ valid = false, error_msg = "salt_bytes above maximum (32)" }
 59    else
 60      @{ valid = true, error_msg = "" }
 61  
 62  fun
 63  validate_hash_bytes(p: int): validation_result =
 64    if p < HASH_BYTES_MIN then
 65      @{ valid = false, error_msg = "hash_bytes below minimum (32)" }
 66    else if p > HASH_BYTES_MAX then
 67      @{ valid = false, error_msg = "hash_bytes above maximum (64)" }
 68    else
 69      @{ valid = true, error_msg = "" }
 70  
 71  fun
 72  validate_parallelism(p: int): validation_result =
 73    if p < PARALLELISM_MIN then
 74      @{ valid = false, error_msg = "parallelism below minimum (1)" }
 75    else if p > PARALLELISM_MAX then
 76      @{ valid = false, error_msg = "parallelism above maximum (8)" }
 77    else
 78      @{ valid = true, error_msg = "" }
 79  
 80  fun
 81  validate_memory_kib(m: int): validation_result =
 82    if m < MEMORY_KIB_MIN then
 83      @{ valid = false, error_msg = "memory_kib below minimum (65536)" }
 84    else if m > MEMORY_KIB_MAX then
 85      @{ valid = false, error_msg = "memory_kib above maximum (1048576)" }
 86    else
 87      @{ valid = true, error_msg = "" }
 88  
 89  fun
 90  validate_time_cost(t: int): validation_result =
 91    if t < TIME_COST_MIN then
 92      @{ valid = false, error_msg = "time_cost below minimum (2)" }
 93    else if t > TIME_COST_MAX then
 94      @{ valid = false, error_msg = "time_cost above maximum (10)" }
 95    else
 96      @{ valid = true, error_msg = "" }
 97  
 98  (* --- Full parameter validation --- *)
 99  
100  fun
101  validate_params(params: argon2_params): validation_result = let
102    val r1 = validate_salt_bytes(params.salt_bytes)
103  in
104    if ~r1.valid then r1
105    else let
106      val r2 = validate_hash_bytes(params.hash_bytes)
107    in
108      if ~r2.valid then r2
109      else let
110        val r3 = validate_parallelism(params.parallelism)
111      in
112        if ~r3.valid then r3
113        else let
114          val r4 = validate_memory_kib(params.memory_kib)
115        in
116          if ~r4.valid then r4
117          else let
118            val r5 = validate_time_cost(params.time_cost)
119          in
120            if ~r5.valid then r5
121            else @{ valid = true, error_msg = "" }
122          end
123        end
124      end
125    end
126  end
127  
128  (* --- Upgrade validation (allow_increase_only) --- *)
129  
130  fun
131  validate_upgrade(old_p: argon2_params, new_p: argon2_params): validation_result =
132    if new_p.salt_bytes < old_p.salt_bytes then
133      @{ valid = false, error_msg = "upgrade cannot decrease salt_bytes" }
134    else if new_p.hash_bytes < old_p.hash_bytes then
135      @{ valid = false, error_msg = "upgrade cannot decrease hash_bytes" }
136    else if new_p.parallelism < old_p.parallelism then
137      @{ valid = false, error_msg = "upgrade cannot decrease parallelism" }
138    else if new_p.memory_kib < old_p.memory_kib then
139      @{ valid = false, error_msg = "upgrade cannot decrease memory_kib" }
140    else if new_p.time_cost < old_p.time_cost then
141      @{ valid = false, error_msg = "upgrade cannot decrease time_cost" }
142    else
143      @{ valid = true, error_msg = "" }
144  
145  (* --- Profile validation --- *)
146  
147  datatype profile_name =
148    | Interactive
149    | Moderate
150    | High
151    | Unknown of string
152  
153  fun
154  parse_profile(s: string): profile_name =
155    if s = "interactive" then Interactive()
156    else if s = "moderate" then Moderate()
157    else if s = "high" then High()
158    else Unknown(s)
159  
160  fun
161  validate_profile_name(s: string): validation_result = let
162    val p = parse_profile(s)
163  in
164    case+ p of
165    | Unknown(name) => @{ valid = false, error_msg = "unknown profile: " + name }
166    | _ => @{ valid = true, error_msg = "" }
167  end
168  
169  (* --- Profile defaults (for shadow checking) --- *)
170  
171  fun
172  get_profile_defaults(p: profile_name): argon2_params =
173    case+ p of
174    | Interactive() => @{
175        salt_bytes = 16,
176        hash_bytes = 32,
177        parallelism = 1,
178        memory_kib = 131072,
179        time_cost = 3
180      }
181    | Moderate() => @{
182        salt_bytes = 16,
183        hash_bytes = 32,
184        parallelism = 2,
185        memory_kib = 262144,
186        time_cost = 4
187      }
188    | High() => @{
189        salt_bytes = 16,
190        hash_bytes = 32,
191        parallelism = 4,
192        memory_kib = 524288,
193        time_cost = 5
194      }
195    | Unknown(_) => @{
196        salt_bytes = 0,
197        hash_bytes = 0,
198        parallelism = 0,
199        memory_kib = 0,
200        time_cost = 0
201      }
202  
203  (* --- Invariant: argon2id MUST NOT be used for artifact hashing --- *)
204  
205  (* This is a compile-time marker. The actual enforcement is in code review
206     and CI grep checks. This type exists to document the invariant. *)
207  
208  abstype artifact_digest  (* opaque: cannot be constructed from argon2 output *)
209  abstype password_verifier  (* opaque: argon2id output, cannot be used as artifact_digest *)
210  
211  (* The type system prevents confusion at compile time if used properly.
212     This is the ATS-style way of encoding the non-goal invariants. *)
213  
214  (*
215    Usage in CI:
216  
217    1. Build this file to verify it compiles (syntax/type check)
218    2. Extract the constraint constants and compare to spec/keystore-policy.json
219    3. Run grep checks to ensure argon2 is not imported in artifact modules
220  
221    patscc -tcats argon2-checks.dats  # Type-check only
222  *)