Project-declaredLean 4.31.0 · null

Default lit wf

Cedar.Thm.default_lit_wf

authorization program verification semantics decoder

Plain-language statement

Decoder.defaultLit is well-formed if given sufficiently well-formed eidOf and ty.

Exact Lean statement

public theorem default_lit_wf
  {εs : SymEntities}
  {eidOf : EntityType → String} {ty : TermType}
  (hwf_ty : ty.WellFormed εs)
  (hwf_eidOf : ∀ ety, εs.isValidEntityType ety → εs.isValidEntityUID { ty := ety, eid := eidOf ety }) :
  (Decoder.defaultLit eidOf ty).WellFormed εs

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

public theorem default_lit_wf  {εs : SymEntities}  {eidOf : EntityType → String} {ty : TermType}  (hwf_ty : ty.WellFormed εs)  (hwf_eidOf : ∀ ety, εs.isValidEntityType ety → εs.isValidEntityUID { ty := ety, eid := eidOf ety }) :  (Decoder.defaultLit eidOf ty).WellFormed εs:= by  cases ty with  | prim p =>    simp only [Decoder.defaultLit]    constructor    cases p with    | bool | bitvec | string =>      simp only [Decoder.defaultPrim]      constructor    | entity uid =>      simp only [Decoder.defaultPrim]      constructor      apply hwf_eidOf      cases hwf_ty      assumption    | ext e =>      cases e      all_goals        simp only [Decoder.defaultPrim, Decoder.defaultExt]        constructor  | option ty' =>    simp only [Decoder.defaultLit]    constructor    cases hwf_ty ; assumption  | set ty' =>    simp only [Decoder.defaultLit]    constructor    · intros t ht      exfalso      exact Set.not_mem_empty _ ht    · intros t ht      exfalso      exact Set.not_mem_empty _ ht    · cases hwf_ty ; assumption    · exact Set.empty_wf  | record rty =>    cases rty with | mk attrs =>    cases hwf_ty with | record_wf hwf_rty hwf_rty_map =>    simp only [Decoder.defaultLit]    simp only [Map.mapOnValues₂_eq_mapOnValues]    constructor    · intros attr t hmem_attr_t      replace hmem_attr_t := Map.mem_toList_find? (Map.mapOnValues_wf.mp hwf_rty_map) hmem_attr_t      replace ⟨attr_ty, hmem_attr_t, _⟩ := Map.find?_mapOnValues_some' _ hmem_attr_t      subst t      have := Map.sizeOf_lt_of_find? hmem_attr_t      apply default_lit_wf _ hwf_eidOf      apply hwf_rty attr      exact hmem_attr_t    · exact Map.mapOnValues_wf.mp hwf_rty_map

Project: Cedar Specification
License: Apache-2.0
Commit: 3f093947b8ae
Source: cedar-lean/Cedar/Thm/SymCC/Decoder.lean:41-96

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.31.0

Find? ext

Cedar.Data.Map.find?_ext

Plain-language statement

Two well-formed maps are equal if they have the same find? for every key.

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Find? notmem keys

Cedar.Data.Map.find?_notmem_keys

Plain-language statement

Inverse of find?_mem_toList, except that this requires wf

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Find? some iff in values

Cedar.Data.Map.find?_some_iff_in_values

Plain-language statement

The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record